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: * Super reference.
020: *
021: */
022:
023: public class SuperReference extends JavaNonTerminalProgramElement
024: implements Reference, Expression, ReferencePrefix,
025: ReferenceSuffix, ExpressionContainer, TypeReferenceContainer {
026:
027: /**
028: * Access path.
029: */
030: private final ReferencePrefix prefix;
031:
032: /**
033: * Super reference.
034: */
035: public SuperReference() {
036: prefix = null;
037: }
038:
039: /**
040: * Super reference.
041: * @param accessPath a reference expression.
042: */
043: public SuperReference(ReferencePrefix accessPath) {
044: this .prefix = accessPath;
045: }
046:
047: /**
048: * Constructor for the transformation of COMPOST ASTs to KeY.
049: * @param children the children of this AST element as KeY classes.
050: */
051: public SuperReference(ExtList children) {
052: prefix = (ReferencePrefix) children.get(ReferencePrefix.class);
053: }
054:
055: public SourceElement getFirstElement() {
056: return (prefix == null) ? this : prefix.getFirstElement();
057: }
058:
059: /**
060: * Get reference prefix.
061: * @return the reference prefix.
062: */
063:
064: public ReferencePrefix getReferencePrefix() {
065: return prefix;
066: }
067:
068: /**
069: * Returns the number of children of this node.
070: * @return an int giving the number of children of this node
071: */
072: public int getChildCount() {
073: int count = 0;
074: if (prefix != null)
075: count++;
076: return count;
077: }
078:
079: /**
080: * Returns the child at the specified index in this node's "virtual"
081: * child array
082: * @param index an index into this node's "virtual" child array
083: * @return the program element at the given position
084: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
085: * of bounds
086: */
087: public ProgramElement getChildAt(int index) {
088: if (prefix != null) {
089: if (index == 0)
090: return prefix;
091: index--;
092: }
093: throw new ArrayIndexOutOfBoundsException();
094: }
095:
096: /**
097: * Get the number of expressions in this container.
098: * @return the number of expressions.
099: */
100:
101: public int getExpressionCount() {
102: return (prefix instanceof Expression) ? 1 : 0;
103: }
104:
105: /*
106: Return the expression at the specified index in this node's
107: "virtual" expression array.
108: @param index an index for an expression.
109: @return the expression with the given index.
110: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
111: of bounds.
112: */
113:
114: public Expression getExpressionAt(int index) {
115: if (prefix instanceof Expression && index == 0) {
116: return (Expression) prefix;
117: }
118: throw new ArrayIndexOutOfBoundsException();
119: }
120:
121: /**
122: * Get the number of type references in this container.
123: * @return the number of type references.
124: */
125: public int getTypeReferenceCount() {
126: return (prefix instanceof TypeReference) ? 1 : 0;
127: }
128:
129: /*
130: Return the type reference at the specified index in this node's
131: "virtual" type reference array.
132: @param index an index for a type reference.
133: @return the type reference with the given index.
134: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
135: of bounds.
136: */
137:
138: public TypeReference getTypeReferenceAt(int index) {
139: if ((prefix instanceof TypeReference) && index == 0) {
140: return (TypeReference) prefix;
141: }
142: throw new ArrayIndexOutOfBoundsException();
143: }
144:
145: /** calls the corresponding method of a visitor in order to
146: * perform some action/transformation on this element
147: * @param v the Visitor
148: */
149: public void visit(Visitor v) {
150: v.performActionOnSuperReference(this );
151: }
152:
153: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
154: p.printSuperReference(this );
155: }
156:
157: public ReferencePrefix setReferencePrefix(ReferencePrefix r) {
158: return this ;
159: }
160:
161: /**
162: * returns the KeYJavaType
163: */
164: public KeYJavaType getKeYJavaType(Services javaServ,
165: ExecutionContext ec) {
166: return javaServ.getJavaInfo().getSuperclass(
167: ec.getTypeReference().getKeYJavaType());
168: }
169:
170: }
|