001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.java.expression.operator;
012:
013: import de.uka.ilkd.key.java.PrettyPrinter;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.TypeConverter;
016: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
017: import de.uka.ilkd.key.java.abstraction.PrimitiveType;
018: import de.uka.ilkd.key.java.expression.Operator;
019: import de.uka.ilkd.key.java.reference.ExecutionContext;
020: import de.uka.ilkd.key.java.visitor.Visitor;
021: import de.uka.ilkd.key.util.ExtList;
022:
023: /** The most weird ternary C operator ?: */
024:
025: public class Conditional extends Operator {
026:
027: /**
028: * Conditional.
029: * @param children list of children the first one is the guard expression,
030: * the second one the then expression and the last one the else expr.
031: */
032:
033: public Conditional(ExtList children) {
034: super (children);
035: }
036:
037: /**
038: * Get arity.
039: * @return the int value.
040: */
041:
042: public int getArity() {
043: return 3;
044: }
045:
046: /**
047: * Get precedence.
048: * @return the int value.
049: */
050:
051: public int getPrecedence() {
052: return 12;
053: }
054:
055: /**
056: * Get notation.
057: * @return the int value.
058: */
059:
060: public int getNotation() {
061: return INFIX;
062: }
063:
064: /**
065: * Checks if this operator is left or right associative. Conditionals
066: * are right associative.
067: * @return <CODE>true</CODE>, if the operator is left associative,
068: * <CODE>false</CODE> otherwise.
069: */
070:
071: public boolean isLeftAssociative() {
072: return false;
073: }
074:
075: /** calls the corresponding method of a visitor in order to
076: * perform some action/transformation on this element
077: * @param v the Visitor
078: */
079: public void visit(Visitor v) {
080: v.performActionOnConditional(this );
081: }
082:
083: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
084: p.printConditional(this );
085: }
086:
087: public KeYJavaType getKeYJavaType(Services javaServ,
088: ExecutionContext ec) {
089: final TypeConverter tc = javaServ.getTypeConverter();
090: final KeYJavaType type1 = tc.getKeYJavaType(getExpressionAt(1),
091: ec);
092: final KeYJavaType type2 = tc.getKeYJavaType(getExpressionAt(2),
093: ec);
094: if (tc.isIdentical(type1, type2))
095: return type1;
096:
097: // numeric types
098: if (tc.isArithmeticType(type1) && tc.isArithmeticType(type2)) {
099: if (type1.getJavaType() == PrimitiveType.JAVA_BYTE
100: && type2.getJavaType() == PrimitiveType.JAVA_SHORT
101: || type1.getJavaType() == PrimitiveType.JAVA_SHORT
102: && type2.getJavaType() == PrimitiveType.JAVA_BYTE)
103: return javaServ.getJavaInfo().getKeYJavaType(
104: PrimitiveType.JAVA_SHORT);
105: if (tc.isImplicitNarrowing(getExpressionAt(1),
106: (PrimitiveType) type2.getJavaType()))
107: return type2;
108: if (tc.isImplicitNarrowing(getExpressionAt(2),
109: (PrimitiveType) type1.getJavaType()))
110: return type1;
111: return tc.getPromotedType(type1, type2);
112: }
113:
114: // reference types
115: if (tc.isNullType(type1) && tc.isReferenceType(type2))
116: return type2;
117: if (tc.isNullType(type2) && tc.isReferenceType(type1))
118: return type1;
119: if (tc.isAssignableTo(type1, type2))
120: return type2;
121: if (tc.isAssignableTo(type2, type1))
122: return type1;
123:
124: throw new RuntimeException(
125: "Could not determine type of conditional "
126: + "expression\n" + this
127: + ". This usually means that "
128: + "the Java program is not compilable.");
129: }
130:
131: }
|