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: package de.uka.ilkd.key.java;
010:
011: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
012: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
013: import de.uka.ilkd.key.java.declaration.Modifier;
014: import de.uka.ilkd.key.java.declaration.ParameterDeclaration;
015: import de.uka.ilkd.key.java.declaration.VariableSpecification;
016: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
017: import de.uka.ilkd.key.java.reference.FieldReference;
018: import de.uka.ilkd.key.java.reference.ReferencePrefix;
019: import de.uka.ilkd.key.java.reference.TypeRef;
020: import de.uka.ilkd.key.java.reference.TypeReference;
021: import de.uka.ilkd.key.java.statement.*;
022: import de.uka.ilkd.key.logic.ProgramElementName;
023: import de.uka.ilkd.key.logic.op.LocationVariable;
024: import de.uka.ilkd.key.logic.op.ProgramVariable;
025:
026: /**
027: * The KeYASTFactory helps building KeY Java AST structures.
028: */
029: public abstract class KeYJavaASTFactory {
030:
031: /**
032: * creates an assignment <code> lhs:=rhs </code>
033: */
034: public static Statement assign(Expression lhs, Expression rhs) {
035: return new CopyAssignment(lhs, rhs);
036: }
037:
038: /**
039: * creates an attribute access <code>prefix.field </code>
040: */
041: public static Expression attribute(ReferencePrefix prefix,
042: ProgramVariable field) {
043: return new FieldReference(field, prefix);
044: }
045:
046: /**
047: * creates a local variable declaration <code> typeRef name; </code>
048: */
049: public static LocalVariableDeclaration declare(
050: ProgramElementName name, TypeReference typeRef) {
051: return new LocalVariableDeclaration(typeRef,
052: new VariableSpecification(new LocationVariable(name,
053: typeRef.getKeYJavaType())));
054: }
055:
056: /**
057: * create a local variable declaration <br></br>
058: * <code>type name = init; </code>
059: */
060: public static LocalVariableDeclaration declare(
061: ProgramElementName name, Expression init, KeYJavaType type) {
062: return new LocalVariableDeclaration(new TypeRef(type),
063: new VariableSpecification(new LocationVariable(name,
064: type), init, type));
065: }
066:
067: public static LocalVariableDeclaration declare(ProgramVariable var,
068: Expression init, KeYJavaType type) {
069: return new LocalVariableDeclaration(new TypeRef(type),
070: new VariableSpecification(var, init, type));
071: }
072:
073: public static LocalVariableDeclaration declare(ProgramVariable var,
074: KeYJavaType type) {
075: return new LocalVariableDeclaration(new TypeRef(type),
076: new VariableSpecification(var, type));
077: }
078:
079: /**
080: * create a local variable declaration
081: */
082: public static LocalVariableDeclaration declare(String name,
083: KeYJavaType type) {
084: return new LocalVariableDeclaration(new TypeRef(type),
085: new VariableSpecification(new LocationVariable(
086: new ProgramElementName(name), type)));
087: }
088:
089: /**
090: * create a parameter declaration
091: */
092:
093: public static ParameterDeclaration parameterDeclaration(
094: JavaInfo javaInfo, KeYJavaType kjt, String name) {
095: return new ParameterDeclaration(new Modifier[0], javaInfo
096: .createTypeReference(kjt), new VariableSpecification(
097: localVariable(name, kjt)), false);
098: }
099:
100: public static ParameterDeclaration parameterDeclaration(
101: JavaInfo javaInfo, KeYJavaType kjt, ProgramVariable var) {
102: return new ParameterDeclaration(new Modifier[0], javaInfo
103: .createTypeReference(kjt), new VariableSpecification(
104: var), false);
105: }
106:
107: public static ParameterDeclaration parameterDeclaration(
108: JavaInfo javaInfo, String type, String name) {
109: KeYJavaType kjt = javaInfo.getKeYJavaType(type);
110: return new ParameterDeclaration(new Modifier[0], javaInfo
111: .createTypeReference(kjt), new VariableSpecification(
112: localVariable(name, kjt)), false);
113: }
114:
115: /**
116: * create a local variable
117: */
118: public static ProgramVariable localVariable(String name,
119: KeYJavaType kjt) {
120: return localVariable(new ProgramElementName(name), kjt);
121: }
122:
123: /**
124: * create a local variable
125: */
126: public static ProgramVariable localVariable(
127: ProgramElementName name, KeYJavaType kjt) {
128: return new LocationVariable(name, kjt);
129: }
130:
131: /**
132: * create a catch clause
133: */
134:
135: public static Catch catchClause(ParameterDeclaration param,
136: StatementBlock body) {
137:
138: return new Catch(param, body);
139: }
140:
141: public static Catch catchClause(JavaInfo javaInfo, String param,
142: KeYJavaType kjt, StatementBlock body) {
143:
144: return new Catch(parameterDeclaration(javaInfo, kjt, param),
145: body);
146: }
147:
148: public static Catch catchClause(JavaInfo javaInfo, String param,
149: String type, StatementBlock body) {
150:
151: return catchClause(javaInfo, param, javaInfo
152: .getKeYJavaType(type), body);
153: }
154:
155: public static Throw throwClause(Expression e) {
156: return new Throw(e);
157: }
158:
159: public static Return returnClause(Expression e) {
160: return new Return(e);
161: }
162:
163: public static If ifThen(Expression guard, Statement then) {
164: return new If(guard, new Then(then));
165: }
166:
167: public static If ifElse(Expression guard, Then then, Else els) {
168: return new If(guard, then, els);
169: }
170:
171: public static Break breakStatement(Label l) {
172: return new Break(l);
173: }
174:
175: public static EmptyStatement emptyStatement() {
176: return new EmptyStatement();
177: }
178:
179: /** inserts the given statements at the begin of the block
180: * @param stmnt array of Statement those have to be inserted
181: * @param b the Statementblock where to insert
182: */
183: public static StatementBlock insertStatementInBlock(
184: Statement[] stmnt, StatementBlock b) {
185:
186: Statement[] block = new Statement[b.getStatementCount()
187: + stmnt.length];
188: System.arraycopy(stmnt, 0, block, 0, stmnt.length);
189: b.getBody().arraycopy(0, block, stmnt.length,
190: b.getStatementCount());
191: return new StatementBlock(new ArrayOfStatement(block));
192: }
193:
194: /** inserts the given statements at the begin of the block
195: * @param stmnt array of Statement those have to be inserted
196: * @param b the Statementblock where to insert
197: */
198: public static StatementBlock insertStatementInBlock(
199: StatementBlock stmnt, StatementBlock b) {
200: Statement[] stmnts = new Statement[stmnt.getStatementCount()];
201: for (int i = 0; i < stmnt.getStatementCount(); i++)
202: stmnts[i] = stmnt.getStatementAt(i);
203: return insertStatementInBlock(stmnts, b);
204: }
205:
206: }
|