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.ProgramElementName;
018: import de.uka.ilkd.key.logic.ProgramPrefix;
019: import de.uka.ilkd.key.util.Debug;
020: import de.uka.ilkd.key.util.ExtList;
021:
022: /**
023: * Labeled statement.
024: */
025:
026: public class LabeledStatement extends JavaStatement implements
027: StatementContainer, NamedProgramElement, ProgramPrefix {
028:
029: /**
030: * Name.
031: */
032:
033: protected final Label name;
034:
035: /**
036: * Body.
037: */
038:
039: protected final Statement body;
040:
041: private final ArrayOfProgramPrefix prefixElementArray;
042:
043: /**
044: * Constructor for the transformation of COMPOST ASTs to KeY.
045: * @param children the children of this AST element as KeY classes.
046: * May contain: a Label (as name of the label)
047: * a Statement (as body of the labeled statement)
048: * Comments
049: */
050: public LabeledStatement(ExtList children, Label label,
051: PositionInfo pos) {
052: super (children, pos);
053: name = label;
054:
055: body = (Statement) children.get(Statement.class);
056: prefixElementArray = computePrefix(body);
057: }
058:
059: /**
060: * Labeled statement.
061: * @param name an identifier.
062: */
063:
064: public LabeledStatement(Label name) {
065: this .name = name;
066: body = new EmptyStatement();
067: prefixElementArray = new ArrayOfProgramPrefix();
068: }
069:
070: /**
071: * Labeled statement.
072: * @param id a Label.
073: * @param statement a statement.
074: */
075:
076: public LabeledStatement(Label id, Statement statement) {
077: this .name = id;
078: body = statement;
079: prefixElementArray = computePrefix(body);
080: }
081:
082: private ArrayOfProgramPrefix computePrefix(Statement b) {
083: if (b instanceof StatementBlock) {
084: return StatementBlock.computePrefixElements(
085: ((StatementBlock) b).getBody(), 0, this );
086: } else if (b instanceof ProgramPrefix) {
087: return StatementBlock.computePrefixElements(
088: new ArrayOfStatement(b), 0, this );
089: }
090: return new ArrayOfProgramPrefix(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 SourceElement getFirstElement() {
106: return getBody().getFirstElement();
107: }
108:
109: public SourceElement getLastElement() {
110: return body.getLastElement();
111: }
112:
113: /**
114: * Get name.
115: * @return the string.
116: */
117:
118: public final String getName() {
119: return (name == null) ? null : name.toString();
120: }
121:
122: /**
123: * Get identifier.
124: * @return the identifier.
125: */
126:
127: public Label getLabel() {
128: return name;
129: }
130:
131: /**
132: * Get identifier.
133: * @return the identifier.
134: */
135: public ProgramElementName getProgramElementName() {
136: if ((name instanceof ProgramElementName) || (name == null)) {
137: return (ProgramElementName) name;
138: }
139: Debug
140: .out("labeledstatement: SCHEMAVARIABLE IN LABELEDSTATEMENT");
141: return null;
142: }
143:
144: /**
145: * Get body.
146: * @return the statement.
147: */
148: public Statement getBody() {
149: return body;
150: }
151:
152: /**
153: * Returns the number of children of this node.
154: * @return an int giving the number of children of this node
155: */
156:
157: public int getChildCount() {
158: int result = 0;
159: if (name != null)
160: result++;
161: if (body != null)
162: result++;
163: return result;
164: }
165:
166: /**
167: * Returns the child at the specified index in this node's "virtual"
168: * child array
169: * @param index an index into this node's "virtual" child array
170: * @return the program element at the given position
171: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
172: * of bounds
173: */
174:
175: public ProgramElement getChildAt(int index) {
176: if (name != null) {
177: if (index == 0)
178: return name;
179: index--;
180: }
181: if (body != null) {
182: if (index == 0)
183: return body;
184: index--;
185: }
186: throw new ArrayIndexOutOfBoundsException();
187: }
188:
189: /**
190: * Get the number of statements in this container.
191: * @return the number of statements.
192: */
193:
194: public int getStatementCount() {
195: return (body != null) ? 1 : 0;
196: }
197:
198: /**
199: * Return the statement at the specified index in this node's
200: * "virtual" statement array.
201: * @param index an index for a statement.
202: * @return the statement with the given index.
203: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
204: * of bounds.
205: */
206:
207: public Statement getStatementAt(int index) {
208: if (body != null && index == 0) {
209: return body;
210: }
211: throw new ArrayIndexOutOfBoundsException();
212: }
213:
214: /** calls the corresponding method of a visitor in order to
215: * perform some action/transformation on this element
216: * @param v the Visitor
217: */
218: public void visit(Visitor v) {
219: v.performActionOnLabeledStatement(this );
220: }
221:
222: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
223: p.printLabeledStatement(this );
224: }
225:
226: /** testing if programelements are equal modulo renaming abstract
227: * from names. Therefore declaration of label names have to be
228: * mapped to the same abstract name. This is done here.
229: */
230: public boolean equalsModRenaming(SourceElement se,
231: NameAbstractionTable nat) {
232: if (!(se instanceof LabeledStatement)) {
233: return false;
234: }
235: final LabeledStatement lSt = (LabeledStatement) se;
236: nat.add(getLabel(), lSt.getLabel());
237: return super .equalsModRenaming(lSt, nat);
238: }
239:
240: public int hashCode() {
241: int result = 17;
242: result = 37 * result + getChildCount();
243: for (int i = 0; i < getChildCount(); i++) {
244: result = 37 * result + getChildAt(i).hashCode();
245: }
246: return result;
247: }
248:
249: public boolean equals(Object o) {
250: return super .equals(o);
251: }
252:
253: private PosInProgram firstActiveChildPos = null;
254:
255: public PosInProgram getFirstActiveChildPos() {
256: if (firstActiveChildPos == null) {
257: firstActiveChildPos = body instanceof StatementBlock ? (((StatementBlock) body)
258: .isEmpty() ? PosInProgram.TOP : PosInProgram.TOP
259: .down(1).down(0))
260: : PosInProgram.TOP.down(1);
261: }
262: return firstActiveChildPos;
263: }
264:
265: }
|