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.statement;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.visitor.Visitor;
015: import de.uka.ilkd.key.logic.ArrayOfProgramPrefix;
016: import de.uka.ilkd.key.logic.PosInProgram;
017: import de.uka.ilkd.key.logic.ProgramPrefix;
018: import de.uka.ilkd.key.util.ExtList;
019:
020: /**
021: * Try.
022: * @author <TT>AutoDoc</TT>
023: */
024: public class Try extends BranchStatement implements StatementContainer,
025: ProgramPrefix {
026:
027: /**
028: * Body.
029: */
030:
031: private final StatementBlock body;
032:
033: /**
034: * Branches.
035: */
036:
037: private final ArrayOfBranch branches;
038:
039: private final ArrayOfProgramPrefix prefixElementArray;
040:
041: private PosInProgram firstActiveChildPos = null;
042:
043: /**
044: * Try.
045: * @param body a statement block.
046: */
047:
048: public Try(StatementBlock body) {
049: this .body = body;
050: this .branches = null;
051: prefixElementArray = computePrefix(body);
052: }
053:
054: /**
055: * Try.
056: * @param body a statement block.
057: * @param branches a branch array.
058: */
059:
060: public Try(StatementBlock body, Branch[] branches) {
061: this .body = body;
062: this .branches = new ArrayOfBranch(branches);
063: prefixElementArray = computePrefix(body);
064: }
065:
066: /**
067: * Try.
068: * @param body a statement block.
069: * @param branches a branch array.
070: */
071:
072: public Try(StatementBlock body, ArrayOfBranch branches) {
073: this .body = body;
074: this .branches = branches;
075: prefixElementArray = computePrefix(body);
076: }
077:
078: /**
079: * Try.
080: * @param children a list with all children
081: */
082:
083: public Try(ExtList children) {
084: super (children);
085: this .body = (StatementBlock) children.get(StatementBlock.class);
086: this .branches = new ArrayOfBranch((Branch[]) children
087: .collect(Branch.class));
088: prefixElementArray = computePrefix(body);
089: }
090:
091: private ArrayOfProgramPrefix computePrefix(StatementBlock b) {
092: return StatementBlock.computePrefixElements(b.getBody(), 0,
093: this );
094: }
095:
096: public int getPrefixLength() {
097: return prefixElementArray.size();
098: }
099:
100: public ProgramPrefix getPrefixElementAt(int i) {
101: return prefixElementArray.getProgramPrefix(i);
102: }
103:
104: public ArrayOfProgramPrefix getPrefixElements() {
105: return prefixElementArray;
106: }
107:
108: public SourceElement getFirstElement() {
109: return body.getFirstElement();
110: }
111:
112: public SourceElement getLastElement() {
113: return getChildAt(getChildCount() - 1).getLastElement();
114: }
115:
116: /**
117: * Returns the number of children of this node.
118: * @return an int giving the number of children of this node
119: */
120:
121: public int getChildCount() {
122: int result = 0;
123: if (body != null)
124: result++;
125: if (branches != null)
126: result += branches.size();
127: return result;
128: }
129:
130: /**
131: * Returns the child at the specified index in this node's "virtual"
132: * child array
133: * @param index an index into this node's "virtual" child array
134: * @return the program element at the given position
135: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
136: * of bounds
137: */
138:
139: public ProgramElement getChildAt(int index) {
140: if (body != null) {
141: if (index == 0)
142: return body;
143: index--;
144: }
145: if (branches != null) {
146: return branches.getBranch(index);
147: }
148: throw new ArrayIndexOutOfBoundsException();
149: }
150:
151: /**
152: * Get body.
153: * @return the statement block.
154: */
155:
156: public StatementBlock getBody() {
157: return body;
158: }
159:
160: /**
161: * Get the number of statements in this container.
162: * @return the number of statements.
163: */
164:
165: public int getStatementCount() {
166: return (body != null) ? 1 : 0;
167: }
168:
169: /*
170: Return the statement at the specified index in this node's
171: "virtual" statement array.
172: @param index an index for a statement.
173: @return the statement with the given index.
174: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
175: of bounds.
176: */
177:
178: public Statement getStatementAt(int index) {
179: if (body != null && index == 0) {
180: return body;
181: }
182: throw new ArrayIndexOutOfBoundsException();
183: }
184:
185: /**
186: * Get the number of branches in this container.
187: * @return the number of branches.
188: */
189:
190: public int getBranchCount() {
191: return (branches != null) ? branches.size() : 0;
192: }
193:
194: /*
195: Return the branch at the specified index in this node's
196: "virtual" branch array.
197: @param index an index for a branch.
198: @return the branch with the given index.
199: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
200: of bounds.
201: */
202:
203: public Branch getBranchAt(int index) {
204: if (branches != null) {
205: return branches.getBranch(index);
206: }
207: throw new ArrayIndexOutOfBoundsException();
208: }
209:
210: /* Return the branch array wrapper
211: * @return the array wrapper of the branches
212: */
213: public ArrayOfBranch getBranchList() {
214: return branches;
215: }
216:
217: public Branch containsAsBranch(Class cl) {
218: ArrayOfBranch br = getBranchList();
219: for (int i = 0, brSize = br.size(); i < brSize; i++) {
220: if (cl.isInstance(br.getBranch(i))) {
221: return branches.getBranch(i);
222: }
223: }
224: return null;
225: }
226:
227: /** calls the corresponding method of a visitor in order to
228: * perform some action/transformation on this element
229: * @param v the Visitor
230: */
231: public void visit(Visitor v) {
232: v.performActionOnTry(this );
233: }
234:
235: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
236: p.printTry(this );
237: }
238:
239: public PosInProgram getFirstActiveChildPos() {
240:
241: if (firstActiveChildPos == null) {
242: firstActiveChildPos = body.isEmpty() ? PosInProgram.TOP
243: : PosInProgram.TOP.down(0).down(0);
244: }
245:
246: return firstActiveChildPos;
247: }
248: }
|