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.ProgramElement;
016: import de.uka.ilkd.key.java.SourceElement;
017: import de.uka.ilkd.key.java.reference.TypeReference;
018: import de.uka.ilkd.key.java.visitor.Visitor;
019: import de.uka.ilkd.key.util.ExtList;
020:
021: /**
022: * Instanceof.
023: * @author <TT>AutoDoc</TT>
024: */
025:
026: public class ExactInstanceof extends TypeOperator {
027:
028: /**
029: * Instanceof.
030: * @param children an ExtList with all children of this node
031: * the first children in list will be the expression on the left
032: * side, the second the one on the right side a type reference.
033: */
034:
035: public ExactInstanceof(ExtList children) {
036: super (children);
037: }
038:
039: public ExactInstanceof(Expression unaryChild, TypeReference typeref) {
040: super (unaryChild, typeref);
041: }
042:
043: /**
044: * Returns the number of children of this node.
045: * @return an int giving the number of children of this node
046: */
047:
048: public int getChildCount() {
049: int result = 0;
050: if (children != null)
051: result += children.size();
052: if (typeReference != null)
053: result++;
054: return result;
055: }
056:
057: public SourceElement getLastElement() {
058: return typeReference;
059: }
060:
061: /**
062: * Returns the child at the specified index in this node's "virtual"
063: * child array
064: * @param index an index into this node's "virtual" child array
065: * @return the program element at the given position
066: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
067: * of bounds
068: */
069:
070: public ProgramElement getChildAt(int index) {
071: int len;
072: if (children != null) {
073: len = children.size();
074: if (len > index) {
075: return children.getExpression(index);
076: }
077: index -= len;
078: }
079: if (typeReference != null) {
080: if (index == 0)
081: return typeReference;
082: index--;
083: }
084: throw new ArrayIndexOutOfBoundsException();
085: }
086:
087: /**
088: * Get arity.
089: * @return the int value.
090: */
091:
092: public int getArity() {
093: return 1;
094: }
095:
096: /**
097: * Get precedence.
098: * @return the int value.
099: */
100:
101: public int getPrecedence() {
102: return 5;
103: }
104:
105: /**
106: * Get notation.
107: * @return the int value.
108: */
109:
110: public int getNotation() {
111: return POSTFIX;
112: }
113:
114: /** calls the corresponding method of a visitor in order to
115: * perform some action/transformation on this element
116: * @param v the Visitor
117: */
118: public void visit(Visitor v) {
119: v.performActionOnExactInstanceof(this );
120: }
121:
122: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
123: p.printExactInstanceof(this);
124: }
125: }
|