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