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.reference;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
015: import de.uka.ilkd.key.java.visitor.Visitor;
016: import de.uka.ilkd.key.util.ExtList;
017:
018: /**
019: * A reference to the current object.
020: * "this" can be prefixed by a type reference (to resolve ambiguities
021: * with inner classes).
022: */
023:
024: public class ThisReference extends JavaNonTerminalProgramElement
025: implements Reference, Expression, ReferencePrefix,
026: ReferenceSuffix, TypeReferenceContainer {
027:
028: /**
029: * Prefix.
030: */
031: private final ReferencePrefix prefix;
032:
033: /**
034: * This reference.
035: */
036: public ThisReference() {
037: prefix = null;
038: }
039:
040: /**
041: * This reference.
042: * @param outer a type reference.
043: */
044: public ThisReference(TypeReference outer) {
045: prefix = outer;
046: }
047:
048: /**
049: * Constructor for the transformation of COMPOST ASTs to KeY.
050: * @param children the children of this AST element as KeY classes.
051: * May contain:
052: * a TypeReference (as reference for the ThisReference)
053: * Comments
054: */
055: public ThisReference(ExtList children) {
056: super (children);
057: prefix = (TypeReference) children.get(TypeReference.class);
058: }
059:
060: public SourceElement getFirstElement() {
061: return (prefix == null) ? this : prefix.getFirstElement();
062: }
063:
064: /**
065: * Returns the number of children of this node.
066: * @return an int giving the number of children of this node
067: */
068: public int getChildCount() {
069: int count = 0;
070: if (prefix != null)
071: count++;
072: return count;
073: }
074:
075: /**
076: * Returns the child at the specified index in this node's "virtual"
077: * child array
078: * @param index an index into this node's "virtual" child array
079: * @return the program element at the given position
080: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
081: * of bounds
082: */
083: public ProgramElement getChildAt(int index) {
084: if (prefix != null) {
085: if (index == 0)
086: return prefix;
087: index--;
088: }
089: throw new ArrayIndexOutOfBoundsException();
090: }
091:
092: /**
093: * Get reference prefix.
094: * @return the reference prefix.
095: */
096: public ReferencePrefix getReferencePrefix() {
097: return prefix;
098: }
099:
100: /**
101: * Get the number of type references in this container.
102: * @return the number of type references.
103: */
104: public int getTypeReferenceCount() {
105: return (prefix != null) ? 1 : 0;
106: }
107:
108: /*
109: Return the type reference at the specified index in this node's
110: "virtual" type reference array.
111: @param index an index for a type reference.
112: @return the type reference with the given index.
113: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
114: of bounds.
115: */
116:
117: public TypeReference getTypeReferenceAt(int index) {
118: if (prefix instanceof TypeReference && index == 0) {
119: return (TypeReference) prefix;
120: }
121: throw new ArrayIndexOutOfBoundsException();
122: }
123:
124: /** calls the corresponding method of a visitor in order to
125: * perform some action/transformation on this element
126: * @param v the Visitor
127: */
128: public void visit(Visitor v) {
129: v.performActionOnThisReference(this );
130: }
131:
132: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
133: p.printThisReference(this );
134: }
135:
136: public ReferencePrefix setReferencePrefix(ReferencePrefix r) {
137: return this ;
138: }
139:
140: public KeYJavaType getKeYJavaType(Services javaServ,
141: ExecutionContext ec) {
142: return ec.getTypeReference().getKeYJavaType();
143: }
144:
145: }
|