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.declaration.ArrayOfVariableSpecification;
015: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
016: import de.uka.ilkd.key.java.declaration.VariableSpecification;
017: import de.uka.ilkd.key.java.visitor.Visitor;
018: import de.uka.ilkd.key.util.ExtList;
019:
020: /**
021: * For.
022: *
023: */
024:
025: public class For extends LoopStatement implements VariableScope {
026:
027: private static final ArrayOfVariableSpecification EMPTY_VARSPECS = new ArrayOfVariableSpecification(
028: new VariableSpecification[0]);
029:
030: /**
031: * For.
032: */
033: public For() {
034: }
035:
036: /**
037: * For. Used for the Recoder2KeY transformation
038: * @param inits a loop initializer mutable list.
039: * @param guard an expression.
040: * @param updates an expression mutable list.
041: * @param body a statement.
042: */
043: public For(LoopInitializer[] inits, Expression guard,
044: Expression[] updates, Statement body) {
045: super (inits, guard, updates, body);
046: }
047:
048: public For(ILoopInit inits, IGuard guard, IForUpdates updates,
049: Statement body, ExtList comments) {
050: super (inits, guard, updates, body, comments);
051: }
052:
053: public For(ILoopInit inits, IGuard guard, IForUpdates updates,
054: Statement body, ExtList comments, PositionInfo pos) {
055: super (inits, guard, updates, body, comments, pos);
056: }
057:
058: public For(ILoopInit inits, IGuard guard, IForUpdates updates,
059: Statement body) {
060: super (inits, guard, updates, body);
061: }
062:
063: public For(ExtList children) {
064: super ((ILoopInit) children.get(ILoopInit.class),
065: (IGuard) children.get(IGuard.class),
066: (IForUpdates) children.get(IForUpdates.class),
067: (Statement) children.get(Statement.class), children);
068: }
069:
070: public SourceElement getLastElement() {
071: return (body != null) ? body.getLastElement() : this ;
072: }
073:
074: /**
075: * Is exit condition.
076: * @return the boolean value.
077: */
078:
079: public boolean isExitCondition() {
080: return false;
081: }
082:
083: /**
084: * Is checked before iteration.
085: * @return the boolean value.
086: */
087:
088: public boolean isCheckedBeforeIteration() {
089: return true;
090: }
091:
092: public boolean isDefinedScope() {
093: return true;
094: }
095:
096: public ArrayOfVariableSpecification getVariablesInScope() {
097: if (inits != null) {
098: LoopInitializer li = inits.getInits().getLoopInitializer(0);
099: if (li instanceof LocalVariableDeclaration) {
100: return ((LocalVariableDeclaration) li).getVariables();
101: }
102: }
103: return EMPTY_VARSPECS;
104: }
105:
106: public VariableSpecification getVariableInScope(String name) {
107: if (inits != null) {
108: LoopInitializer li = inits.getInits().getLoopInitializer(0);
109: if (li instanceof LocalVariableDeclaration) {
110: ArrayOfVariableSpecification vars = ((LocalVariableDeclaration) li)
111: .getVariables();
112: for (int i = 0, s = vars.size(); i < s; i += 1) {
113: VariableSpecification v = vars
114: .getVariableSpecification(i);
115: if (name.equals(v.getName())) {
116: return v;
117: }
118: }
119: }
120: }
121: return null;
122: }
123:
124: /** calls the corresponding method of a visitor in order to
125: * perform some action/transformation on this element
126: * @param v the Visitor
127: */
128: public void visit(Visitor v) {
129: v.performActionOnFor(this );
130: }
131:
132: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
133: p.printFor(this);
134: }
135:
136: }
|