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.declaration.ArrayDeclaration;
016: import de.uka.ilkd.key.java.visitor.Visitor;
017: import de.uka.ilkd.key.util.ExtList;
018:
019: /**
020: * Array reference.
021: * @author <TT>AutoDoc</TT>
022: */
023:
024: public class ArrayReference extends JavaNonTerminalProgramElement
025: implements Reference, Expression, ReferencePrefix,
026: ReferenceSuffix, ExpressionContainer, TypeReferenceContainer {
027:
028: /**
029: * Access path.
030: */
031: protected final ReferencePrefix prefix;
032:
033: /**
034: Inits.
035: */
036: protected final ArrayOfExpression inits;
037:
038: /**
039: * Array reference.
040: */
041: public ArrayReference() {
042: prefix = null;
043: this .inits = null;
044: }
045:
046: /**
047: * Array reference.
048: * @param accessPath a reference prefix.
049: * @param initializers an expression array.
050: */
051: public ArrayReference(ReferencePrefix accessPath,
052: Expression[] initializers) {
053: this .prefix = accessPath;
054: this .inits = new ArrayOfExpression(initializers);
055: }
056:
057: /**
058: * Constructor for the transformation of COMPOST ASTs to KeY.
059: * @param children the children of this AST element as KeY classes.
060: * May contain:
061: * several of Expression (as initializers of the array),
062: * Comments.
063: * MUST NOT CONTAIN: the ReferencePrefix for the accessPath because
064: * Expression and ReferencePrefix might not be disjunct.
065: * @param accessPath a ReferencePrefix of the array reference.
066: */
067: public ArrayReference(ExtList children, ReferencePrefix accessPath,
068: PositionInfo pi) {
069: super (children, pi);
070: Expression[] e = (Expression[]) children
071: .collect(Expression.class);
072: if (e.length > 1) {
073: Expression[] e1 = new Expression[e.length - 1];
074: for (int i = 0; i < e1.length; i++)
075: e1[i] = e[i];
076: this .prefix = new ArrayReference(e1, accessPath);
077: e1 = new Expression[1];
078: e1[0] = e[e.length - 1];
079: this .inits = new ArrayOfExpression(e1);
080: } else {
081: this .prefix = accessPath;
082: this .inits = new ArrayOfExpression(e);
083: }
084: }
085:
086: /**
087: * Constructor for the transformation of COMPOST ASTs to KeY.
088: * @param children the children of this AST element as KeY classes.
089: * May contain:
090: * several of Expression (as initializers of the array),
091: * Comments.
092: * MUST NOT CONTAIN: the ReferencePrefix for the accessPath because
093: * Expression and ReferencePrefix might not be disjunct.
094: * @param accessPath a ReferencePrefix of the array reference.
095: */
096: public ArrayReference(ExtList children, ReferencePrefix accessPath) {
097: this (children, accessPath, (PositionInfo) children
098: .get(PositionInfo.class));
099: }
100:
101: private ArrayReference(Expression[] e, ReferencePrefix accessPath) {
102: Expression[] e1 = new Expression[e.length - 1];
103: if (e.length > 1) {
104: for (int i = 0; i < e1.length; i++)
105: e1[i] = e[i];
106: this .prefix = new ArrayReference(e1, accessPath);
107: e1[0] = e[e.length - 1];
108: this .inits = new ArrayOfExpression(e1);
109: } else {
110: this .prefix = accessPath;
111: this .inits = new ArrayOfExpression(e);
112: }
113: }
114:
115: /**
116: * Get the number of expressions in this container.
117: * @return the number of expressions.
118: */
119: public int getExpressionCount() {
120: int c = 0;
121: if (prefix instanceof Expression)
122: c += 1;
123: if (inits != null)
124: c += inits.size();
125: return c;
126: }
127:
128: /*
129: Return the expression at the specified index in this node's
130: "virtual" expression array.
131: @param index an index for an expression.
132: @return the expression with the given index.
133: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
134: of bounds.
135: */
136:
137: public Expression getExpressionAt(int index) {
138: if (prefix instanceof Expression) {
139: if (index == 0)
140: return (Expression) prefix;
141: index--;
142: }
143: if (inits != null) {
144: return inits.getExpression(index);
145: }
146: throw new ArrayIndexOutOfBoundsException();
147: }
148:
149: /**
150: * Get the number of type references in this container.
151: * @return the number of type references.
152: */
153: public int getTypeReferenceCount() {
154: return (prefix instanceof TypeReference) ? 1 : 0;
155: }
156:
157: /*
158: Return the type reference at the specified index in this node's
159: "virtual" type reference array.
160: @param index an index for a type reference.
161: @return the type reference with the given index.
162: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
163: of bounds.
164: */
165:
166: public TypeReference getTypeReferenceAt(int index) {
167: if (prefix instanceof TypeReference && index == 0) {
168: return (TypeReference) prefix;
169: }
170: throw new ArrayIndexOutOfBoundsException();
171: }
172:
173: /**
174: * Get reference prefix.
175: * @return the reference prefix.
176: */
177:
178: public ReferencePrefix getReferencePrefix() {
179: return prefix;
180: }
181:
182: /**
183: * Returns the number of children of this node.
184: * @return an int giving the number of children of this node
185: */
186: public int getChildCount() {
187: int result = 0;
188: if (prefix != null)
189: result++;
190: if (inits != null)
191: result += inits.size();
192: return result;
193: }
194:
195: /**
196: * Returns the child at the specified index in this node's "virtual"
197: * child array
198: * @param index an index into this node's "virtual" child array
199: * @return the program element at the given position
200: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
201: * of bounds
202: */
203: public ProgramElement getChildAt(int index) {
204: if (prefix != null) {
205: if (index == 0)
206: return prefix;
207: index--;
208: }
209: if (inits != null) {
210: return inits.getExpression(index);
211: }
212: throw new ArrayIndexOutOfBoundsException();
213: }
214:
215: /**
216: * Get dimension expressions.
217: * @return the expression array wrapper.
218: */
219: public ArrayOfExpression getDimensionExpressions() {
220: return inits;
221: }
222:
223: public SourceElement getFirstElement() {
224: return (prefix == null) ? this : prefix.getFirstElement();
225: }
226:
227: /** calls the corresponding method of a visitor in order to
228: * perform some action/transformation on this element
229: * @param v the Visitor
230: */
231: public void visit(Visitor v) {
232: v.performActionOnArrayReference(this );
233: }
234:
235: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
236: p.printArrayReference(this );
237: }
238:
239: public ReferencePrefix setReferencePrefix(ReferencePrefix r) {
240: return this ;
241: }
242:
243: public KeYJavaType getKeYJavaType(Services services,
244: ExecutionContext ec) {
245: final KeYJavaType arrayType = services.getTypeConverter()
246: .getKeYJavaType((Expression) getChildAt(0), ec);
247: return ((ArrayDeclaration) arrayType.getJavaType())
248: .getBaseType().getKeYJavaType();
249: }
250: }
|