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