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.JavaNonTerminalProgramElement;
014: import de.uka.ilkd.key.java.PrettyPrinter;
015: import de.uka.ilkd.key.java.ProgramElement;
016: import de.uka.ilkd.key.java.SourceElement;
017: import de.uka.ilkd.key.java.reference.ArrayOfTypeReference;
018: import de.uka.ilkd.key.java.reference.TypeReference;
019: import de.uka.ilkd.key.java.reference.TypeReferenceContainer;
020: import de.uka.ilkd.key.java.visitor.Visitor;
021: import de.uka.ilkd.key.util.ExtList;
022:
023: /**
024: * Throws.
025: * @author <TT>AutoDoc</TT>
026: */
027:
028: public class Throws extends JavaNonTerminalProgramElement implements
029: TypeReferenceContainer {
030:
031: /**
032: * Exceptions.
033: */
034: protected final ArrayOfTypeReference exceptions;
035:
036: /**
037: * Throws.
038: */
039: public Throws() {
040: this .exceptions = null;
041: }
042:
043: /**
044: * Throws.
045: * @param exception a type reference.
046: */
047: public Throws(TypeReference exception) {
048: this .exceptions = new ArrayOfTypeReference(exception);
049: }
050:
051: /**
052: * Throws.
053: * @param list a type reference array.
054: */
055: public Throws(TypeReference[] list) {
056: this .exceptions = new ArrayOfTypeReference(list);
057: }
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: * May contain:
063: * several of TypeReference (as references to thrown exceptions),
064: * Comments
065: */
066: public Throws(ExtList children) {
067: super (children);
068: this .exceptions = new ArrayOfTypeReference(
069: (TypeReference[]) children.collect(TypeReference.class));
070: }
071:
072: public SourceElement getLastElement() {
073: if (exceptions == null) {
074: return this ;
075: }
076: return exceptions.getTypeReference(exceptions.size() - 1);
077: }
078:
079: /**
080: * Returns the number of children of this node.
081: * @return an int giving the number of children of this node
082: */
083: public int getChildCount() {
084: int result = 0;
085: if (exceptions != null)
086: result += exceptions.size();
087: return result;
088: }
089:
090: /**
091: * Returns the child at the specified index in this node's "virtual"
092: * child array
093: * @param index an index into this node's "virtual" child array
094: * @return the program element at the given position
095: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
096: * of bounds
097: */
098: public ProgramElement getChildAt(int index) {
099: if (exceptions != null) {
100: return exceptions.getTypeReference(index);
101: }
102: throw new ArrayIndexOutOfBoundsException();
103: }
104:
105: /**
106: * Get exceptions.
107: * @return the type reference mutable list.
108: */
109: public ArrayOfTypeReference getExceptions() {
110: return exceptions;
111: }
112:
113: /**
114: * Get the number of type references in this container.
115: * @return the number of type references.
116: */
117: public int getTypeReferenceCount() {
118: return (exceptions != null) ? exceptions.size() : 0;
119: }
120:
121: /*
122: Return the type reference at the specified index in this node's
123: "virtual" type reference array.
124: @param index an index for a type reference.
125: @return the type reference with the given index.
126: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
127: of bounds.
128: */
129: public TypeReference getTypeReferenceAt(int index) {
130: if (exceptions != null) {
131: return exceptions.getTypeReference(index);
132: }
133: throw new ArrayIndexOutOfBoundsException();
134: }
135:
136: /** calls the corresponding method of a visitor in order to
137: * perform some action/transformation on this element
138: * @param v the Visitor
139: */
140: public void visit(Visitor v) {
141: v.performActionOnThrows(this );
142: }
143:
144: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
145: p.printThrows(this);
146: }
147: }
|