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.declaration;
012:
013: import de.uka.ilkd.key.java.PrettyPrinter;
014: import de.uka.ilkd.key.java.ProgramElement;
015: import de.uka.ilkd.key.java.abstraction.*;
016: import de.uka.ilkd.key.java.expression.Literal;
017: import de.uka.ilkd.key.java.expression.literal.NullLiteral;
018: import de.uka.ilkd.key.java.reference.TypeReference;
019: import de.uka.ilkd.key.java.visitor.Visitor;
020: import de.uka.ilkd.key.logic.ProgramElementName;
021: import de.uka.ilkd.key.util.ExtList;
022:
023: /**
024: * KeY used to model arrays using only the {@link
025: * de.uka.ilkd.key.java.abstraction.ArrayType}. As the only attribute of
026: * an array has been the length attribute, it has been handled in a
027: * different way than members of usual classes. As we need some implicit
028: * fields for array creation and initialisation, the special handling of
029: * arrays is not any longer practicable.
030: * So, this class introduce a 'virtual' declaration for array types
031: * containing all required members. Please not the array fields accessed
032: * by an index are not included, so arrays of different lengths with same base
033: * type belong to the same array declaration.
034: * Attention: In contrast to the other type declaration, array
035: * declarations may be added at runtime.
036: */
037:
038: public class ArrayDeclaration extends TypeDeclaration implements
039: ArrayType {
040:
041: /**
042: * reference to the type the elements of this array must subclass
043: */
044: private final TypeReference basetype;
045:
046: /**
047: * dimension of the array
048: */
049: private final int dim;
050:
051: private final KeYJavaType super Type;
052:
053: private String altNameRepresentation;
054:
055: private ArrayDeclaration(ExtList children, TypeReference baseType,
056: ProgramElementName name, KeYJavaType super Type) {
057: super (addLength(children, super Type), name, name, false);
058: this .basetype = baseType;
059: this .dim = dimension();
060: this .super Type = super Type;
061: }
062:
063: private static ExtList addLength(ExtList children,
064: KeYJavaType super Type) {
065: children.add(((SuperArrayDeclaration) super Type.getJavaType())
066: .length());
067: return children;
068: }
069:
070: /**
071: * ArrayDeclaration
072: * @param children an ExtList with the basetype and member
073: * declarations of this type
074: */
075: public ArrayDeclaration(ExtList children, TypeReference baseType,
076: KeYJavaType super Type) {
077: this (children, baseType, createName(baseType), super Type);
078: }
079:
080: /**
081: * Returns the number of children of this node.
082: * @return an int giving the number of children of this node
083: */
084: public int getChildCount() {
085: int result = 0;
086: if (modArray != null)
087: result += modArray.size();
088: if (name != null)
089: result++;
090: if (basetype != null)
091: result++;
092: if (members != null)
093: result += members.size();
094: return result;
095: }
096:
097: public FieldDeclaration length() {
098: return ((SuperArrayDeclaration) super Type.getJavaType())
099: .length();
100: }
101:
102: /**
103: * Returns the child at the specified index in this node's "virtual"
104: * child array
105: * @param index an index into this node's "virtual" child array
106: * @return the program element at the given position
107: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
108: * of bounds
109: */
110: public ProgramElement getChildAt(int index) {
111: int len;
112: if (modArray != null) {
113: len = modArray.size();
114: if (len > index) {
115: return modArray.getModifier(index);
116: }
117: index -= len;
118: }
119: if (name != null) {
120: if (index == 0)
121: return name;
122: index--;
123: }
124: if (basetype != null) {
125: if (index == 0)
126: return basetype;
127: index--;
128: }
129: if (members != null) {
130: return members.getMemberDeclaration(index);
131: }
132: throw new ArrayIndexOutOfBoundsException();
133: }
134:
135: /**
136: * Get the element/base type.
137: * @return refernce to the base type .
138: */
139: public TypeReference getBaseType() {
140: return basetype;
141: }
142:
143: /**
144: * Arrays are never strictfp.
145: */
146: public boolean isStrictFp() {
147: return false;
148: }
149:
150: /**
151: * Arrays are never transient.
152: */
153: public boolean isTransient() {
154: return false;
155: }
156:
157: /**
158: * Arrays are never volatile.
159: */
160: public boolean isVolatile() {
161: return false;
162: }
163:
164: /**
165: * Arrays are never interfaces (but may have interface types as
166: * element types)
167: */
168: public boolean isInterface() {
169: return false;
170: }
171:
172: /**
173: * return the dimension of this array
174: */
175: public int getDimension() {
176: return dim;
177: }
178:
179: /**
180: * returns the default value of the given type
181: * according to JLS Sect. 4.5.5
182: * @return the default value of the given type
183: * according to JLS Sect. 4.5.5
184: */
185: public Literal getDefaultValue() {
186: return NullLiteral.NULL;
187: }
188:
189: /**
190: * computes the dimension of this array
191: */
192: private int dimension() {
193: Type javaType = basetype.getKeYJavaType().getJavaType();
194: if (javaType instanceof ArrayType) {
195: return 1 + ((ArrayType) javaType).getDimension();
196: } else {
197: return 1;
198: }
199: }
200:
201: public static ProgramElementName createName(TypeReference basetype) {
202:
203: Type javaBasetype = basetype.getKeYJavaType().getJavaType();
204:
205: if (javaBasetype == null) {
206: // entered only if base type is class type
207: return new ProgramElementName("[L" + basetype.getName());
208:
209: }
210: if (javaBasetype instanceof ArrayDeclaration) {
211: return new ProgramElementName("["
212: + ((ArrayType) javaBasetype).getFullName());
213: } else if (javaBasetype instanceof TypeDeclaration) {
214: return new ProgramElementName("[L"
215: + javaBasetype.getFullName());
216: } else if (javaBasetype instanceof PrimitiveType) {
217: return ((PrimitiveType) javaBasetype).getArrayElementName();
218: }
219: return null;
220: }
221:
222: public String getAlternativeNameRepresentation() {
223: if (altNameRepresentation == null) {
224: final StringBuffer alt = new StringBuffer();
225: Type baseType = basetype.getKeYJavaType().getJavaType();
226:
227: if (baseType instanceof ArrayType) {
228: alt.append(((ArrayType) baseType)
229: .getAlternativeNameRepresentation());
230: } else {
231: if (baseType instanceof ClassType) {
232: alt.append(((ClassType) baseType).getFullName());
233: } else {
234: alt.append(baseType.getName());
235: }
236: }
237: alt.append("[]");
238: altNameRepresentation = alt.toString();
239: }
240: return altNameRepresentation;
241: }
242:
243: /**
244: * returns the local declared supertypes
245: */
246: public ListOfKeYJavaType getSupertypes() {
247: return SLListOfKeYJavaType.EMPTY_LIST.append(super Type);
248: }
249:
250: /**
251: * calls the corresponding method of a visitor in order to
252: * perform some action/transformation on this element
253: * @param v the Visitor
254: */
255: public void visit(Visitor v) {
256: v.performActionOnArrayDeclaration(this );
257: }
258:
259: /**
260: * pretty prints an array declaration
261: */
262: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
263: p.printArrayDeclaration(this );
264: }
265:
266: /**
267: * toString
268: */
269: public String toString() {
270: return name.toString().intern();
271: }
272:
273: }
|