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.*;
014: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
015: import de.uka.ilkd.key.java.expression.ArrayInitializer;
016: import de.uka.ilkd.key.java.reference.ReferencePrefix;
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: * The array allocation operator.
023: * There are two variants for NewArray:
024: * <OL>
025: * <LI>Ordinary array construction
026: * <BR><tt>new XYZ[d<sub>1</sub>]...[d<sub>n</sub>]</tt>
027: * <LI>Initialized array construction
028: * <BR><tt>new XYZ[]...[] { a<sub>1</sub>, ..., a<sub>n</sub> }
029: * </OL>
030: * Contrary to an ordinary New, a NewArray is no ConstructorReference (since
031: * all ArrayType constructors are predefined) and is not used as a Statement
032: * (since there are no sideeffects in the constructor). No access path is
033: * required for new, since there is no inner class problem.
034: * <P>
035: * NewArray has either a list of dimension length expressions, or
036: * a single ArrayInitializer.
037: */
038:
039: public class NewArray extends TypeOperator implements Reference,
040: ReferencePrefix {
041:
042: /**
043: * Dimensions.
044: */
045:
046: protected final int dimensions;
047:
048: /**
049: * Array initializer.
050: */
051:
052: protected final ArrayInitializer arrayInitializer;
053:
054: /**
055: * the key java type of this array
056: */
057: private final KeYJavaType keyJavaType;
058:
059: /**
060: * New array.
061: * @param children an ExtList with the children of this node
062: * (remove the ArrayInitializer out of the list).
063: * @param init the arrayInitializer
064: * @param dimensions an int value.
065: */
066:
067: public NewArray(ExtList children, KeYJavaType keyJavaType,
068: ArrayInitializer init, int dimensions) {
069: super (children);
070: this .arrayInitializer = init;
071: this .dimensions = dimensions;
072: this .keyJavaType = keyJavaType;
073: }
074:
075: /**
076: * New array.
077: * @param arguments an array of expressions describing the
078: * dimensions
079: * @param typeRef a reference to the arraytype
080: * @param init the arrayInitializer
081: * @param dimensions an int value.
082: */
083: public NewArray(Expression[] arguments, TypeReference typeRef,
084: KeYJavaType keyJavaType, ArrayInitializer init,
085: int dimensions) {
086: super (arguments, typeRef);
087: this .arrayInitializer = init;
088: this .dimensions = dimensions;
089: this .keyJavaType = keyJavaType;
090: }
091:
092: public SourceElement getLastElement() {
093: if (arrayInitializer != null) {
094: return arrayInitializer;
095: }
096: return this ;
097: }
098:
099: /**
100: * Get arity.
101: * @return the int value.
102: */
103:
104: public int getArity() {
105: return 0;
106: }
107:
108: /**
109: * Get precedence.
110: * @return the int value.
111: */
112:
113: public int getPrecedence() {
114: return 0;
115: }
116:
117: /**
118: * Get notation.
119: * @return the int value.
120: */
121:
122: public int getNotation() {
123: return PREFIX;
124: }
125:
126: /**
127: * Get dimensions.
128: * @return the int value.
129: */
130:
131: public int getDimensions() {
132: return dimensions;
133: }
134:
135: /**
136: * Get array initializer.
137: * @return the array initializer.
138: */
139:
140: public ArrayInitializer getArrayInitializer() {
141: return arrayInitializer;
142: }
143:
144: /**
145: * Returns the number of children of this node.
146: * @return an int giving the number of children of this node
147: */
148:
149: public int getChildCount() {
150: int result = 0;
151: if (typeReference != null)
152: result++;
153: if (children != null)
154: result += children.size();
155: if (arrayInitializer != null)
156: result++;
157: return result;
158: }
159:
160: /**
161: * Returns the child at the specified index in this node's "virtual"
162: * child array
163: * @param index an index into this node's "virtual" child array
164: * @return the program element at the given position
165: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
166: * of bounds
167: */
168:
169: public ProgramElement getChildAt(int index) {
170: int len;
171: if (typeReference != null) {
172: if (index == 0)
173: return typeReference;
174: index--;
175: }
176: if (children != null) {
177: len = children.size();
178: if (len > index) {
179: return children.getExpression(index);
180: }
181: index -= len;
182: }
183: if (arrayInitializer != null) {
184: if (index == 0)
185: return arrayInitializer;
186: }
187: throw new ArrayIndexOutOfBoundsException();
188: }
189:
190: /**
191: * Get the number of expressions in this container.
192: * @return the number of expressions.
193: */
194:
195: public int getExpressionCount() {
196: int result = 0;
197: if (children != null)
198: result += children.size();
199: if (arrayInitializer != null)
200: result++;
201: return result;
202: }
203:
204: /*
205: Return the expression at the specified index in this node's
206: "virtual" expression array.
207: @param index an index for an expression.
208: @return the expression with the given index.
209: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
210: of bounds.
211: */
212:
213: public Expression getExpressionAt(int index) {
214: int len;
215: if (children != null) {
216: len = children.size();
217: if (len > index) {
218: return children.getExpression(index);
219: }
220: index -= len;
221: }
222: if (arrayInitializer != null) {
223: if (index == 0)
224: return arrayInitializer;
225: }
226: throw new ArrayIndexOutOfBoundsException();
227: }
228:
229: /** calls the corresponding method of a visitor in order to
230: * perform some action/transformation on this element
231: * @param v the Visitor
232: */
233: public void visit(Visitor v) {
234: v.performActionOnNewArray(this );
235: }
236:
237: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
238: p.printNewArray(this );
239: }
240:
241: /**
242: * We do not have a prefix, so fake it!
243: * This way we implement ReferencePrefix
244: * @author VK
245: */
246: public ReferencePrefix getReferencePrefix() {
247: return null;
248: }
249:
250: /**
251: * same as getKeYJavaType()
252: */
253: public KeYJavaType getKeYJavaType(Services javaServ) {
254: return getKeYJavaType();
255: }
256:
257: public KeYJavaType getKeYJavaType() {
258: return keyJavaType;
259: }
260:
261: }
|