01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.java.expression.operator;
12:
13: import de.uka.ilkd.key.java.Expression;
14: import de.uka.ilkd.key.java.Services;
15: import de.uka.ilkd.key.java.TypeConverter;
16: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
17: import de.uka.ilkd.key.java.expression.Operator;
18: import de.uka.ilkd.key.java.reference.ExecutionContext;
19: import de.uka.ilkd.key.util.ExtList;
20:
21: /**
22: * Operator of arity 2
23: * @author AL
24: */
25: public abstract class BinaryOperator extends Operator {
26:
27: public BinaryOperator(ExtList children) {
28: super (children);
29: }
30:
31: public BinaryOperator(Expression lhs, Expression rhs) {
32: super (lhs, rhs);
33: }
34:
35: /**
36: * Get arity.
37: * @return the int value.
38: */
39: public int getArity() {
40: return 2;
41: }
42:
43: public KeYJavaType getKeYJavaType(Services javaServ,
44: ExecutionContext ec) {
45: final TypeConverter tc = javaServ.getTypeConverter();
46: return tc.getPromotedType(tc.getKeYJavaType(
47: (Expression) getChildAt(0), ec), tc.getKeYJavaType(
48: (Expression) getChildAt(1), ec));
49: }
50:
51: }
|