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.PositionInfo;
015: import de.uka.ilkd.key.java.PrettyPrinter;
016: import de.uka.ilkd.key.java.ProgramElement;
017: import de.uka.ilkd.key.java.SourceElement;
018: import de.uka.ilkd.key.java.declaration.ClassDeclaration;
019: import de.uka.ilkd.key.java.declaration.TypeDeclaration;
020: import de.uka.ilkd.key.java.declaration.TypeDeclarationContainer;
021: import de.uka.ilkd.key.java.expression.ExpressionStatement;
022: import de.uka.ilkd.key.java.reference.ConstructorReference;
023: import de.uka.ilkd.key.java.reference.ReferencePrefix;
024: import de.uka.ilkd.key.java.reference.ReferenceSuffix;
025: import de.uka.ilkd.key.java.reference.TypeReference;
026: import de.uka.ilkd.key.java.visitor.Visitor;
027: import de.uka.ilkd.key.util.ExtList;
028:
029: /**
030: * The object allocation operator.
031: * There are two variants for New:
032: * <OL>
033: * <LI>Class constructor call
034: * <BR><tt>new XYZ(a<sub>1</sub>, ..., a<sub>n</sub>)</tt>
035: * <BR>if getType() instanceof UserType
036: * <LI>Anonymous Inner Class definition and construction
037: * <BR><tt>new XYZ(a<sub>1</sub>, ..., a<sub>n</sub>)
038: * { m<sub>1</sub>, ..., m<sub>k</sub> }</tt>
039: * <BR>if getType() instanceof UserType && getClassDeclaration() != <tt>null</tt>
040: * </OL>
041: * The access path is <tt>null</tt> in most cases, except when an inner class
042: * constructor is invoked from an outer instance.
043: */
044:
045: public class New extends TypeOperator implements ConstructorReference,
046: ExpressionStatement, ReferencePrefix, ReferenceSuffix,
047: TypeDeclarationContainer {
048:
049: /**
050: * Anonymous class.
051: */
052: protected final ClassDeclaration anonymousClass;
053:
054: /**
055: * Access path.
056: */
057: protected final ReferencePrefix accessPath;
058:
059: /**
060: * Constructor for the transformation of COMPOST ASTs to KeY.
061: * @param children the children of this AST element as KeY classes.
062: * a ClassDeclaration (in case of an anonymous class decl)
063: * a TypeReference (the referred type)
064: * 2 of Expression (the first Expression as left hand
065: * side, the second as right hand side),
066: * Comments;
067: * does NOT contain: a ReferencePrefix for the constructor
068: * as it might be mixed up with the TypeReference
069: * @param rp a ReferencePrefix as access path for the constructor
070: */
071: public New(ExtList children, ReferencePrefix rp) {
072: super (children);
073: anonymousClass = (ClassDeclaration) children
074: .get(ClassDeclaration.class);
075: accessPath = rp;
076: }
077:
078: /**
079: * Constructor for the transformation of COMPOST ASTs to KeY.
080: * @param children the children of this AST element as KeY classes.
081: * a ClassDeclaration (in case of an anonymous class decl)
082: * a TypeReference (the referred type)
083: * 2 of Expression (the first Expression as left hand
084: * side, the second as right hand side),
085: * Comments;
086: * does NOT contain: a ReferencePrefix for the constructor
087: * as it might be mixed up with the TypeReference
088: * @param rp a ReferencePrefix as access path for the constructor
089: */
090: public New(ExtList children, ReferencePrefix rp, PositionInfo pi) {
091: super (children, pi);
092: anonymousClass = (ClassDeclaration) children
093: .get(ClassDeclaration.class);
094: accessPath = rp;
095: }
096:
097: /**
098: * Constructor for the transformation of COMPOST ASTs to KeY.
099: * @param type a TypeReference (the referred type)
100: * @param rp a ReferencePrefix as access path for the constructor
101: */
102: public New(Expression[] arguments, TypeReference type,
103: ReferencePrefix rp) {
104: super (arguments, type);
105: anonymousClass = null;
106: accessPath = rp;
107: }
108:
109: public SourceElement getFirstElement() {
110: return (accessPath != null) ? accessPath.getFirstElement()
111: : this ;
112: }
113:
114: public SourceElement getLastElement() {
115: return getChildAt(getChildCount() - 1).getLastElement();
116: }
117:
118: /**
119: * Get arity.
120: * @return the int value.
121: */
122: public int getArity() {
123: return 0;
124: }
125:
126: /**
127: * Get precedence.
128: * @return the int value.
129: */
130: public int getPrecedence() {
131: return 0;
132: }
133:
134: /**
135: * Get notation.
136: * @return the int value.
137: */
138: public int getNotation() {
139: return PREFIX;
140: }
141:
142: /**
143: * Get class declaration.
144: * @return the class declaration.
145: */
146: public ClassDeclaration getClassDeclaration() {
147: return anonymousClass;
148: }
149:
150: /**
151: * Get the number of type declarations in this container.
152: * @return the number of type declarations.
153: */
154: public int getTypeDeclarationCount() {
155: return (anonymousClass != null) ? 1 : 0;
156: }
157:
158: /*
159: Return the type declaration at the specified index in this node's
160: "virtual" type declaration array.
161: @param index an index for a type declaration.
162: @return the type declaration with the given index.
163: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
164: of bounds.
165: */
166: public TypeDeclaration getTypeDeclarationAt(int index) {
167: if (anonymousClass != null && index == 0) {
168: return anonymousClass;
169: }
170: throw new ArrayIndexOutOfBoundsException();
171: }
172:
173: /**
174: * Returns the number of children of this node.
175: * @return an int giving the number of children of this node
176: */
177: public int getChildCount() {
178: int result = 0;
179: if (accessPath != null)
180: result++;
181: if (typeReference != null)
182: result++;
183: if (children != null)
184: result += children.size();
185: if (anonymousClass != null)
186: result++;
187: return result;
188: }
189:
190: /**
191: * Returns the child at the specified index in this node's "virtual"
192: * child array
193: * @param index an index into this node's "virtual" child array
194: * @return the program element at the given position
195: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
196: * of bounds
197: */
198: public ProgramElement getChildAt(int index) {
199: int len;
200: if (accessPath != null) {
201: if (index == 0)
202: return accessPath;
203: index--;
204: }
205: if (typeReference != null) {
206: if (index == 0)
207: return typeReference;
208: index--;
209: }
210: if (children != null) {
211: len = children.size();
212: if (len > index) {
213: return children.getExpression(index);
214: }
215: index -= len;
216: }
217: if (anonymousClass != null) {
218: if (index == 0)
219: return anonymousClass;
220: }
221: throw new ArrayIndexOutOfBoundsException();
222: }
223:
224: /**
225: * Get reference prefix.
226: * @return the reference prefix.
227: */
228: public ReferencePrefix getReferencePrefix() {
229: return accessPath;
230: }
231:
232: /** calls the corresponding method of a visitor in order to
233: * perform some action/transformation on this element
234: * @param v the Visitor
235: */
236: public void visit(Visitor v) {
237: v.performActionOnNew(this );
238: }
239:
240: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
241: p.printNew(this );
242: }
243:
244: public ReferencePrefix setReferencePrefix(ReferencePrefix r) {
245: return this;
246: }
247: }
|