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 java.util.LinkedList;
014:
015: import de.uka.ilkd.key.java.Comment;
016: import de.uka.ilkd.key.java.PrettyPrinter;
017: import de.uka.ilkd.key.java.ProgramElement;
018: import de.uka.ilkd.key.java.Statement;
019: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
020: import de.uka.ilkd.key.java.abstraction.SLListOfKeYJavaType;
021: import de.uka.ilkd.key.java.visitor.Visitor;
022: import de.uka.ilkd.key.jml.UsefulTools;
023: import de.uka.ilkd.key.logic.ProgramElementName;
024: import de.uka.ilkd.key.util.ExtList;
025:
026: /**
027: * There are several types of class declarations:
028: * <ul>
029: * <li>package-less outer classes
030: * <ul>
031: * <li>getClassContainer() == null
032: * <li>getStatementContainer() == null
033: * <li>getName() != null
034: * </ul>
035: * <li>ordinary outer classes
036: * <ul>
037: * <li>getClassContainer() instanceof Package
038: * <li>getStatementContainer() == null
039: * <li>getName() != null
040: * </ul>
041: * <li>member classes
042: * <ul>
043: * <li>getClassContainer() instanceof ClassDeclaration
044: * <li>getStatementContainer() == null
045: * <li>getName() != null
046: * </ul>
047: * <li>local class
048: * <ul>
049: * <li>getClassContainer() == null
050: * <li>getStatementContainer() != null
051: * <li>getName() != null
052: * </ul>
053: * <li>local anonymous class
054: * <ul>
055: * <li>getClassContainer() == null
056: * <li>getStatementContainer() instanceof expression.New
057: * <li>getName() == null
058: * </ul>
059: * </ul>
060: * Anonymous local classes have exactly one supertype and no
061: * subtypes.
062: * <BR>
063: * Binary classes may have only binary members.
064: * taken from COMPOST and changed to achieve an immutable structure
065: */
066:
067: public class ClassDeclaration extends TypeDeclaration implements
068: Statement {
069:
070: /**
071: * Extending.
072: */
073:
074: protected final Extends extending;
075:
076: /**
077: * Implementing.
078: */
079: protected final Implements implementing;
080:
081: /**
082: * Class declaration.
083: * @param mods a modifier array.
084: * @param name Identifier of the class
085: * @param members an array containing the memberdeclarations of
086: * this type
087: * @param implemented of type Implement containing the
088: * interfaces implemented by this class
089: * @param extended Extend containing the class extended by
090: * the class of this classdeclaration
091: * @param parentIsInterfaceDeclaration boolean true iff
092: * parent is an InterfaceDeclaration
093: */
094: public ClassDeclaration(Modifier[] mods, ProgramElementName name,
095: Extends extended, ProgramElementName fullName,
096: Implements implemented, MemberDeclaration[] members,
097: boolean parentIsInterfaceDeclaration, boolean isLibrary) {
098: super (mods, name, fullName, members,
099: parentIsInterfaceDeclaration, isLibrary);
100: this .extending = extended;
101: this .implementing = implemented;
102: }
103:
104: /**
105: * uses children list to create non-anonymous class
106: * @param children the ExtList with all children building up this
107: * class declaration
108: * May contain: a Extends (as pointer to a
109: * class), a Implements (as pointer to an interface)
110: * ProgramElementName (as name), several MemberDeclaration (as members of
111: * the type), a parentIsInterfaceDeclaration (indicating if parent is
112: * interface), several Modifier (as modifiers of the type decl), a Comment
113: * @param fullName the fully qualified ProgramElementName of this class
114: * @param isLibrary a boolean flag indicating if this class represents a
115: * library class (such classes have usually no method implementations but
116: * specifications)
117: */
118: public ClassDeclaration(ExtList children,
119: ProgramElementName fullName, boolean isLibrary) {
120: super (children, fullName, isLibrary);
121: extending = (Extends) children.get(Extends.class);
122: implementing = (Implements) children.get(Implements.class);
123: }
124:
125: public ClassDeclaration(ProgramElementName name,
126: ProgramElementName fullName) {
127: this (
128: new de.uka.ilkd.key.java.declaration.Modifier[] {},
129: name,
130: null,
131: fullName,
132: null,
133: new de.uka.ilkd.key.java.declaration.MemberDeclaration[] {},
134: false, false);
135: }
136:
137: /**
138: * Returns the number of children of this node.
139: * @return an int giving the number of children of this node
140: */
141:
142: public int getChildCount() {
143: int result = 0;
144: if (modArray != null)
145: result += modArray.size();
146: if (name != null)
147: result++;
148: if (extending != null)
149: result++;
150: if (implementing != null)
151: result++;
152: if (members != null)
153: result += members.size();
154: return result;
155: }
156:
157: /**
158: * Returns the child at the specified index in this node's "virtual"
159: * child array
160: * @param index an index into this node's "virtual" child array
161: * @return the program element at the given position
162: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
163: * of bounds
164: */
165:
166: public ProgramElement getChildAt(int index) {
167: int len;
168: if (modArray != null) {
169: len = modArray.size();
170: if (len > index) {
171: return modArray.getModifier(index);
172: }
173: index -= len;
174: }
175: if (name != null) {
176: if (index == 0)
177: return name;
178: index--;
179: }
180: if (extending != null) {
181: if (index == 0)
182: return extending;
183: index--;
184: }
185: if (implementing != null) {
186: if (index == 0)
187: return implementing;
188: index--;
189: }
190: if (members != null) {
191: return members.getMemberDeclaration(index);
192: }
193: throw new ArrayIndexOutOfBoundsException();
194: }
195:
196: /**
197: * Get extended types.
198: * @return the extends.
199: */
200:
201: public Extends getExtendedTypes() {
202: return extending;
203: }
204:
205: /**
206: * Get implemented types.
207: * @return the implements.
208: */
209:
210: public Implements getImplementedTypes() {
211: return implementing;
212: }
213:
214: /**
215: * Classes are never strictfp.
216: */
217:
218: public boolean isStrictFp() {
219: return false;
220: }
221:
222: /**
223: * Classes are never transient.
224: */
225:
226: public boolean isTransient() {
227: return false;
228: }
229:
230: /**
231: * Classes are never volatile.
232: */
233:
234: public boolean isVolatile() {
235: return false;
236: }
237:
238: public boolean isInterface() {
239: return false;
240: }
241:
242: /**
243: * returns the local declared supertypes
244: */
245: public ListOfKeYJavaType getSupertypes() {
246: ListOfKeYJavaType types = SLListOfKeYJavaType.EMPTY_LIST;
247: if (implementing != null) {
248: for (int i = implementing.getTypeReferenceCount() - 1; i >= 0; i--) {
249: types = types.prepend(implementing
250: .getTypeReferenceAt(i).getKeYJavaType());
251: }
252: }
253: if (extending != null) {
254: types = types.prepend(extending.getTypeReferenceAt(0)
255: .getKeYJavaType());
256: }
257: return types;
258: }
259:
260: /**
261: * returns the comments belonging to this ClassDeclaration + Comments
262: * declared in the body of the class that contain jml invariant or
263: * constraint statements.
264: * @return the comments.
265: */
266: public Comment[] getComments() {
267:
268: final Comment[] c1 = super .getComments();
269: assert c1 != null;
270:
271: LinkedList jmlComments = new LinkedList();
272: //HACK: RECODER interprets comments, that are intended to be refering
273: // to the class, as comments belonging to fields or methods.
274: for (int i = 0, cc = getChildCount(); i < cc; i++) {
275: ProgramElement p = getChildAt(i);
276: Comment[] c2 = p.getComments();
277: if (c2 != null) {
278: for (int j = 0; j < c2.length; j++) {
279: if (UsefulTools.isClassSpec(c2[j])
280: || (p instanceof Modifier)) {
281: jmlComments.add(c2[j]);
282: }
283: }
284: }
285: }
286: final Comment[] c2 = new Comment[c1.length + jmlComments.size()];
287: System.arraycopy(c1, 0, c2, 0, c1.length);
288:
289: for (int i = c1.length; i < c2.length; i++) {
290: c2[i] = (Comment) jmlComments.removeFirst();
291: }
292: return c2;
293: }
294:
295: /** calls the corresponding method of a visitor in order to
296: * perform some action/transformation on this element
297: * @param v the Visitor
298: */
299: public void visit(Visitor v) {
300: v.performActionOnClassDeclaration(this );
301: }
302:
303: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
304: p.printClassDeclaration(this);
305: }
306:
307: }
|