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.Expression;
014: import de.uka.ilkd.key.java.PrettyPrinter;
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.java.TypeConverter;
017: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
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: /**
024: * Unsigned shift right.
025: *
026: */
027:
028: public class UnsignedShiftRight extends Operator {
029:
030: /**
031: * Unsigned shift right.
032: */
033:
034: public UnsignedShiftRight() {
035: }
036:
037: /**
038: * Unsigned shift right.
039: * @param lhs an expression.
040: * @param rhs an expression.
041: */
042:
043: public UnsignedShiftRight(Expression lhs, Expression rhs) {
044: super (lhs, rhs);
045: }
046:
047: /**
048: * Constructor for the transformation of COMPOST ASTs to KeY.
049: * The first occurrence of an Expression in the given list is taken as
050: * the left hand side
051: * of the expression, the second occurrence is taken as the right hand
052: * side of the expression.
053: * @param children the children of this AST element as KeY classes.
054: */
055: public UnsignedShiftRight(ExtList children) {
056: super (children);
057: }
058:
059: /**
060: * Get arity.
061: * @return the int value.
062: */
063:
064: public int getArity() {
065: return 2;
066: }
067:
068: /**
069: * Get precedence.
070: * @return the int value.
071: */
072:
073: public int getPrecedence() {
074: return 4;
075: }
076:
077: /**
078: * Get notation.
079: * @return the int value.
080: */
081:
082: public int getNotation() {
083: return INFIX;
084: }
085:
086: /** calls the corresponding method of a visitor in order to
087: * perform some action/transformation on this element
088: * @param v the Visitor
089: */
090: public void visit(Visitor v) {
091: v.performActionOnUnsignedShiftRight(this );
092: }
093:
094: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
095: p.printUnsignedShiftRight(this );
096: }
097:
098: public KeYJavaType getKeYJavaType(Services javaServ,
099: ExecutionContext ec) {
100: final TypeConverter tc = javaServ.getTypeConverter();
101: return tc.getPromotedType(tc.getKeYJavaType(
102: (Expression) getChildAt(0), ec));
103: }
104: }
|