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.util.ExtList;
016:
017: /**
018: * If.
019: * @author <TT>AutoDoc</TT>
020: */
021: public class If extends BranchStatement implements ExpressionContainer {
022:
023: /**
024: * Then branch.
025: */
026:
027: protected Then thenBranch;
028:
029: /**
030: * Else branch.
031: */
032:
033: protected Else elseBranch;
034:
035: /**
036: * Expression.
037: */
038:
039: protected Expression expression;
040:
041: /**
042: * Constructor for the transformation of COMPOST ASTs to KeY.
043: * @param children the children of this AST element as KeY classes.
044: * May contain: Comments, a Then, an Else, an Expression (as condition of If)
045: */
046: public If(ExtList children) {
047: super (children);
048: thenBranch = (Then) children.get(Then.class);
049: elseBranch = (Else) children.get(Else.class);
050: expression = (Expression) children.get(Expression.class);
051: }
052:
053: /**
054: * If.
055: * @param e an expression.
056: * @param thenBranch a then.
057: */
058:
059: public If(Expression e, Then thenBranch) {
060: this (e, thenBranch, null);
061: }
062:
063: /**
064: * If.
065: * @param e an expression.
066: * @param thenBranch a then.
067: * @param elseBranch an else.
068: */
069:
070: public If(Expression e, Then thenBranch, Else elseBranch) {
071: if (e == null) {
072: throw new NullPointerException();
073: }
074: expression = e;
075: this .thenBranch = thenBranch;
076: this .elseBranch = elseBranch;
077: }
078:
079: public SourceElement getLastElement() {
080: return getChildAt(getChildCount() - 1).getLastElement();
081: }
082:
083: /**
084: * Returns the number of children of this node.
085: * @return an int giving the number of children of this node
086: */
087:
088: public int getChildCount() {
089: int result = 0;
090: if (expression != null)
091: result++;
092: if (thenBranch != null)
093: result++;
094: if (elseBranch != null)
095: result++;
096: return result;
097: }
098:
099: /**
100: * Returns the child at the specified index in this node's "virtual"
101: * child array
102: * @param index an index into this node's "virtual" child array
103: * @return the program element at the given position
104: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
105: * of bounds
106: */
107: public ProgramElement getChildAt(int index) {
108: if (expression != null) {
109: if (index == 0)
110: return expression;
111: index--;
112: }
113: if (thenBranch != null) {
114: if (index == 0)
115: return thenBranch;
116: index--;
117: }
118: if (elseBranch != null) {
119: if (index == 0)
120: return elseBranch;
121: }
122: throw new ArrayIndexOutOfBoundsException();
123: }
124:
125: /**
126: * Get the number of expressions in this container.
127: * @return the number of expressions.
128: */
129: public int getExpressionCount() {
130: return (expression != null) ? 1 : 0;
131: }
132:
133: /*
134: Return the expression at the specified index in this node's
135: "virtual" expression array.
136: @param index an index for an expression.
137: @return the expression with the given index.
138: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
139: of bounds.
140: */
141: public Expression getExpressionAt(int index) {
142: if (expression != null && index == 0) {
143: return expression;
144: }
145: throw new ArrayIndexOutOfBoundsException();
146: }
147:
148: /**
149: * Get expression.
150: * @return the expression.
151: */
152:
153: public Expression getExpression() {
154: return expression;
155: }
156:
157: /**
158: * Get then.
159: * @return the then.
160: */
161: public Then getThen() {
162: return thenBranch;
163: }
164:
165: /**
166: * Get else.
167: * @return the else.
168: */
169: public Else getElse() {
170: return elseBranch;
171: }
172:
173: /**
174: * Get the number of branches in this container.
175: * @return the number of branches.
176: */
177: public int getBranchCount() {
178: int result = 0;
179: if (thenBranch != null)
180: result += 1;
181: if (elseBranch != null)
182: result += 1;
183: return result;
184: }
185:
186: /*
187: Return the branch at the specified index in this node's
188: "virtual" branch array.
189: @param index an index for a branch.
190: @return the branch with the given index.
191: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
192: of bounds.
193: */
194: public Branch getBranchAt(int index) {
195: if (thenBranch != null) {
196: if (index == 0) {
197: return thenBranch;
198: }
199: index -= 1;
200: }
201: if (elseBranch != null) {
202: if (index == 0) {
203: return elseBranch;
204: }
205: }
206: throw new ArrayIndexOutOfBoundsException();
207: }
208:
209: /**
210: * Add (or replace) an else-branch
211: * @author vladimir
212: */
213: public void addBranch(Else el) {
214: this .elseBranch = el;
215:
216: }
217:
218: /** calls the corresponding method of a visitor in order to
219: * perform some action/transformation on this element
220: * @param v the Visitor
221: */
222: public void visit(Visitor v) {
223: v.performActionOnIf(this );
224: }
225:
226: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
227: p.printIf(this);
228: }
229: }
|