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.LocalVariableDeclaration;
015: import de.uka.ilkd.key.java.declaration.Modifier;
016: import de.uka.ilkd.key.java.declaration.ParameterDeclaration;
017: import de.uka.ilkd.key.java.declaration.VariableSpecification;
018: import de.uka.ilkd.key.java.expression.literal.NullLiteral;
019: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
020: import de.uka.ilkd.key.java.reference.TypeRef;
021: import de.uka.ilkd.key.java.visitor.Visitor;
022: import de.uka.ilkd.key.logic.ProgramElementName;
023: import de.uka.ilkd.key.logic.op.IProgramVariable;
024: import de.uka.ilkd.key.logic.op.LocationVariable;
025: import de.uka.ilkd.key.logic.op.ProgramVariable;
026:
027: /**
028: * A shortcut-statement for a method body.
029: */
030: public class CatchAllStatement extends JavaNonTerminalProgramElement
031: implements Statement, NonTerminalProgramElement, Desugarable,
032: StatementContainer {
033:
034: private StatementBlock body;
035: private ParameterDeclaration paramdecl;
036:
037: public CatchAllStatement(StatementBlock body,
038: ParameterDeclaration paramdecl) {
039: this .body = body;
040: this .paramdecl = paramdecl;
041: }
042:
043: public Statement getBody() {
044: return body;
045: }
046:
047: public ParameterDeclaration getParameterDeclaration() {
048: return paramdecl;
049: }
050:
051: /**
052: * Returns the number of children of this node.
053: * @return an int giving the number of children of this node
054: */
055: public int getChildCount() {
056: int i = 0;
057: if (body != null)
058: i++;
059: if (paramdecl != null)
060: i++;
061: return i;
062: }
063:
064: public Statement getStatementAt(int i) {
065: return body;
066: }
067:
068: public int getStatementCount() {
069: return 1;
070: }
071:
072: /**
073: * Returns the child at the specified index in this node's "virtual"
074: * child array.
075: * @param index an index into this node's "virtual" child array
076: * @return the program element at the given position
077: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
078: * of bounds
079: */
080: public ProgramElement getChildAt(int index) {
081: if (index == 0) {
082: return paramdecl;
083: }
084: if (index == 1) {
085: return body;
086: }
087: throw new ArrayIndexOutOfBoundsException();
088: }
089:
090: /** calls the corresponding method of a visitor in order to
091: * perform some action/transformation on this element
092: * @param v the Visitor
093: */
094: public void visit(Visitor v) {
095: v.performActionOnCatchAllStatement(this );
096: }
097:
098: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
099: p.printCatchAllStatement(this );
100: }
101:
102: public Object desugar() {
103: IProgramVariable pv = getParameterDeclaration()
104: .getVariableSpecification().getProgramVariable();
105: LocalVariableDeclaration lvd = new LocalVariableDeclaration(
106: new TypeRef(pv.getKeYJavaType()),
107: new VariableSpecification(pv, 0, NullLiteral.NULL, pv
108: .getKeYJavaType()));
109: ProgramVariable paramExc = new LocationVariable(
110: new ProgramElementName("e"), pv.getKeYJavaType());
111: CopyAssignment ass = new CopyAssignment((Expression) pv,
112: paramExc);
113: ParameterDeclaration parDecl = new ParameterDeclaration(
114: new Modifier[0], new TypeRef(pv.getKeYJavaType()),
115: new VariableSpecification(paramExc), false);
116: Catch catchBranch = new Catch(parDecl, new StatementBlock(ass));
117: Try tryBlock = new Try(body, new Branch[] { catchBranch });
118: return new StatementBlock(new Statement[] { lvd, tryBlock });
119: }
120:
121: }
|