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.*;
016: import de.uka.ilkd.key.java.abstraction.Method;
017: import de.uka.ilkd.key.java.reference.TypeReference;
018: import de.uka.ilkd.key.java.reference.TypeReferenceContainer;
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: * Method declaration.
025: * taken from COMPOST and changed to achieve an immutable structure
026: */
027:
028: public class MethodDeclaration extends JavaDeclaration implements
029: MemberDeclaration, TypeReferenceContainer, NamedProgramElement,
030: ParameterContainer, Method, VariableScope {
031:
032: /**
033: * Return type.
034: */
035:
036: protected final TypeReference returnType;
037:
038: /**
039: * Name.
040: */
041:
042: protected final ProgramElementName name;
043:
044: /**
045: * Parameters.
046: */
047:
048: protected final ArrayOfParameterDeclaration parameters;
049:
050: /**
051: * Exceptions.
052: */
053:
054: protected final Throws exceptions;
055:
056: /**
057: * Body.
058: */
059:
060: protected final StatementBlock body;
061:
062: /** this field stores if parent is an InterfaceDeclaration because we will be
063: * unable to walk the tree upwards to check this
064: */
065: protected final boolean parentIsInterfaceDeclaration;
066:
067: /**
068: * Method declaration.
069: * @param children an ExtList of children. May
070: * include: a TypeReference (as a reference to the return type), a
071: * de.uka.ilkd.key.logic.ProgramElementName (as Name of the method),
072: * several ParameterDeclaration (as parameters of the declared method), a
073: * StatementBlock (as body of the declared method), several Modifier
074: * (taken as modifiers of the declaration), a Comment
075: * @param parentIsInterfaceDeclaration a boolean set true iff
076: * parent is an InterfaceDeclaration
077: */
078: public MethodDeclaration(ExtList children,
079: boolean parentIsInterfaceDeclaration) {
080: super (children);
081: returnType = (TypeReference) children.get(TypeReference.class);
082: name = (ProgramElementName) children
083: .get(ProgramElementName.class);
084: this .parameters = new ArrayOfParameterDeclaration(
085: (ParameterDeclaration[]) children
086: .collect(ParameterDeclaration.class));
087: exceptions = (Throws) children.get(Throws.class);
088: body = (StatementBlock) children.get(StatementBlock.class);
089: this .parentIsInterfaceDeclaration = parentIsInterfaceDeclaration;
090: }
091:
092: /**
093: * Method declaration.
094: * @param modifiers a modifier array
095: * @param returnType a type reference.
096: * @param name an identifier.
097: * @param parameters a parameter declaration mutable list.
098: * @param exceptions a throws.
099: * @param body a statement block.
100: * @param parentIsInterfaceDeclaration a boolean set true iff
101: * parent is an InterfaceDeclaration
102: */
103:
104: public MethodDeclaration(Modifier[] modifiers,
105: TypeReference returnType, ProgramElementName name,
106: ParameterDeclaration[] parameters, Throws exceptions,
107: StatementBlock body, boolean parentIsInterfaceDeclaration) {
108: this (modifiers, returnType, name,
109: new ArrayOfParameterDeclaration(parameters),
110: exceptions, body, parentIsInterfaceDeclaration);
111: }
112:
113: /**
114: * Method declaration.
115: * @param modifiers a modifier array
116: * @param returnType a type reference.
117: * @param name an identifier.
118: * @param parameters a parameter declaration mutable list.
119: * @param exceptions a throws.
120: * @param body a statement block.
121: * @param parentIsInterfaceDeclaration a boolean set true iff
122: * parent is an InterfaceDeclaration
123: */
124:
125: public MethodDeclaration(Modifier[] modifiers,
126: TypeReference returnType, ProgramElementName name,
127: ArrayOfParameterDeclaration parameters, Throws exceptions,
128: StatementBlock body, boolean parentIsInterfaceDeclaration) {
129: super (modifiers);
130: this .returnType = returnType;
131: this .name = name;
132: this .parameters = parameters;
133: this .exceptions = exceptions;
134: this .body = body;
135: this .parentIsInterfaceDeclaration = parentIsInterfaceDeclaration;
136: }
137:
138: public ProgramElementName getProgramElementName() {
139: return name;
140: }
141:
142: public SourceElement getFirstElement() {
143: return getChildAt(0);
144: }
145:
146: public SourceElement getLastElement() {
147: return getChildAt(getChildCount() - 1).getLastElement();
148: }
149:
150: /**
151: * Returns the number of children of this node.
152: * @return an int giving the number of children of this node
153: */
154:
155: public int getChildCount() {
156: int result = 0;
157: if (modArray != null)
158: result += modArray.size();
159: if (returnType != null)
160: result++;
161: if (name != null)
162: result++;
163: if (parameters != null)
164: result += parameters.size();
165: if (exceptions != null)
166: result++;
167: if (body != null)
168: result++;
169: return result;
170: }
171:
172: /**
173: * Returns the child at the specified index in this node's "virtual"
174: * child array
175: * @param index an index into this node's "virtual" child array
176: * @return the program element at the given position
177: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
178: * of bounds
179: */
180:
181: public ProgramElement getChildAt(int index) {
182: int len;
183: if (modArray != null) {
184: len = modArray.size();
185: if (len > index) {
186: return modArray.getModifier(index);
187: }
188: index -= len;
189: }
190: if (returnType != null) {
191: if (index == 0)
192: return returnType;
193: index--;
194: }
195: if (name != null) {
196: if (index == 0)
197: return name;
198: index--;
199: }
200: if (parameters != null) {
201: len = parameters.size();
202: if (len > index) {
203: return parameters.getParameterDeclaration(index);
204: }
205: index -= len;
206: }
207: if (exceptions != null) {
208: if (index == 0)
209: return exceptions;
210: index--;
211: }
212: if (body != null) {
213: if (index == 0)
214: return body;
215: }
216: throw new ArrayIndexOutOfBoundsException();
217: }
218:
219: /**
220: * Get the number of statements in this container.
221: * @return the number of statements.
222: */
223:
224: public int getStatementCount() {
225: return (body != null) ? 1 : 0;
226: }
227:
228: /*
229: Return the statement at the specified index in this node's
230: "virtual" statement array.
231: @param index an index for a statement.
232: @return the statement with the given index.
233: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
234: of bounds.
235: */
236:
237: public Statement getStatementAt(int index) {
238: if (body != null && index == 0) {
239: return body;
240: }
241: throw new ArrayIndexOutOfBoundsException();
242: }
243:
244: /**
245: * Get the number of type references in this container.
246: * @return the number of type references.
247: */
248:
249: public int getTypeReferenceCount() {
250: return (returnType != null) ? 1 : 0;
251: }
252:
253: /*
254: Return the type reference at the specified index in this node's
255: "virtual" type reference array.
256: @param index an index for a type reference.
257: @return the type reference with the given index.
258: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
259: of bounds.
260: */
261:
262: public TypeReference getTypeReferenceAt(int index) {
263: if (returnType != null && index == 0) {
264: return returnType;
265: }
266: throw new ArrayIndexOutOfBoundsException();
267: }
268:
269: /**
270: * Get the number of parameters in this container.
271: * @return the number of parameters.
272: */
273:
274: public int getParameterDeclarationCount() {
275: return (parameters != null) ? parameters.size() : 0;
276: }
277:
278: /*
279: Return the parameter declaration at the specified index in this node's
280: "virtual" parameter declaration array.
281: @param index an index for a parameter declaration.
282: @return the parameter declaration with the given index.
283: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
284: of bounds.
285: */
286: public ParameterDeclaration getParameterDeclarationAt(int index) {
287: if (parameters != null) {
288: return parameters.getParameterDeclaration(index);
289: }
290: throw new ArrayIndexOutOfBoundsException();
291: }
292:
293: /**
294: * Get return type.
295: * @return the type reference.
296: */
297:
298: public TypeReference getTypeReference() {
299: return returnType;
300: }
301:
302: public final String getName() {
303: return (name == null) ? null : name.toString();
304: }
305:
306: /**
307: * Get parameters.
308: * @return the parameter declaration array wrapper.
309: */
310:
311: public ArrayOfParameterDeclaration getParameters() {
312: return parameters;
313: }
314:
315: public String getFullName() {
316: return getName();
317: }
318:
319: /**
320: * Get thrown.
321: * @return the throws.
322: */
323:
324: public Throws getThrown() {
325: return exceptions;
326: }
327:
328: /**
329: * Get body.
330: * @return the statement block.
331: */
332:
333: public StatementBlock getBody() {
334: return body;
335: }
336:
337: /**
338: * Test whether the declaration is final.
339: */
340:
341: public boolean isFinal() {
342: return super .isFinal();
343: }
344:
345: /**
346: * Test whether the declaration is private.
347: */
348:
349: public boolean isPrivate() {
350: return super .isPrivate();
351: }
352:
353: /**
354: * Test whether the declaration is protected.
355: */
356:
357: public boolean isProtected() {
358: return super .isProtected();
359: }
360:
361: /**
362: * Test whether the declaration is public. Methods of interfaces
363: * are always public.
364: */
365:
366: public boolean isPublic() {
367: return parentIsInterfaceDeclaration || super .isPublic();
368: }
369:
370: /**
371: * Test whether the declaration is static.
372: */
373:
374: public boolean isStatic() {
375: return super .isStatic();
376: }
377:
378: /**
379: * Test whether the declaration is model (the jml modifier is meant).
380: */
381:
382: public boolean isModel() {
383: return super .isModel();
384: }
385:
386: /**
387: * Test whether the declaration is strictfp.
388: */
389:
390: public boolean isStrictFp() {
391: return super .isStrictFp();
392: }
393:
394: /**
395: * Test whether the declaration is abstract. Methods of interfaces
396: * are always abstract.
397: */
398:
399: public boolean isAbstract() {
400: return parentIsInterfaceDeclaration || super .isAbstract();
401: }
402:
403: /**
404: * Test whether the declaration is native. Constructors
405: * are never native.
406: */
407:
408: public boolean isNative() {
409: return super .isNative();
410: }
411:
412: /**
413: * Test whether the declaration is synchronized.
414: */
415:
416: public boolean isSynchronized() {
417: return super .isSynchronized();
418: }
419:
420: /** calls the corresponding method of a visitor in order to
421: * perform some action/transformation on this element
422: * @param v the Visitor
423: */
424: public void visit(Visitor v) {
425: v.performActionOnMethodDeclaration(this );
426: }
427:
428: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
429: p.printMethodDeclaration(this );
430: }
431:
432: /**
433: * returns the comments belonging to this MethodDeclaration.
434: * @return the comments.
435: */
436: public Comment[] getComments() {
437: final Comment[] c1 = super .getComments();
438: assert c1 != null;
439: LinkedList jmlComments = new LinkedList();
440: for (int i = 0, cc = getChildCount(); i < cc; i++) {
441: ProgramElement p = getChildAt(i);
442: final Comment[] c2 = p.getComments();
443: if (c2 != null) {
444: for (int j = 0; j < c2.length; j++) {
445: if (c2[j].containsJMLSpec()
446: && (c2[j].getJMLSpec().indexOf("pure") != -1 || c2[j]
447: .getJMLSpec().indexOf("helper") != -1)) {
448: jmlComments.add(c2[j]);
449: }
450: }
451: }
452: }
453:
454: final Comment[] c2 = new Comment[c1.length + jmlComments.size()];
455:
456: System.arraycopy(c1, 0, c2, 0, c1.length);
457:
458: for (int i = c1.length; i < c2.length; i++) {
459: c2[i] = (Comment) jmlComments.removeFirst();
460: }
461: return c2;
462: }
463:
464: }
|