01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.rule.metaconstruct;
12:
13: import java.util.HashMap;
14:
15: import de.uka.ilkd.key.java.*;
16: import de.uka.ilkd.key.java.declaration.MethodDeclaration;
17: import de.uka.ilkd.key.java.reference.ExecutionContext;
18: import de.uka.ilkd.key.java.reference.ReferencePrefix;
19: import de.uka.ilkd.key.java.reference.TypeRef;
20: import de.uka.ilkd.key.java.reference.TypeReference;
21: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
22: import de.uka.ilkd.key.java.statement.MethodFrame;
23: import de.uka.ilkd.key.java.visitor.ProgVarReplaceVisitor;
24: import de.uka.ilkd.key.logic.Name;
25: import de.uka.ilkd.key.logic.op.ProgramMethod;
26: import de.uka.ilkd.key.logic.op.ProgramSV;
27: import de.uka.ilkd.key.logic.op.SchemaVariable;
28: import de.uka.ilkd.key.rule.inst.SVInstantiations;
29:
30: public class ExpandMethodBody extends ProgramMetaConstruct {
31:
32: static int counter = 0;
33:
34: public ExpandMethodBody(SchemaVariable sv) {
35: super (new Name("expand-method-body"), (ProgramSV) sv);
36: }
37:
38: public ExpandMethodBody(Statement mb) {
39: super (new Name("expand-method-body"), mb);
40: }
41:
42: /**
43: * Replaces the MethodBodyStatement shortcut with the full body,
44: * performs prefix adjustments in the body (execution context).
45: * @param services the Services with all necessary information
46: * about the java programs
47: * @param svInst the instantiations esp. of the inner and outer label
48: * @return the transformed program
49: */
50: public ProgramElement symbolicExecution(ProgramElement pe,
51: Services services, SVInstantiations svInst) {
52:
53: MethodBodyStatement mbs = (MethodBodyStatement) pe;
54: // MethodReference mr = mbs.getMethodReference();
55:
56: ProgramMethod pm = mbs.getProgramMethod(services);
57: //mr.method(services, mbs.getBodySource());
58:
59: MethodDeclaration methDecl = pm.getMethodDeclaration();
60:
61: StatementBlock result = (StatementBlock) mbs.getBody(services);
62: ReferencePrefix newCalled = mbs.getDesignatedContext();
63: if (newCalled instanceof TypeReference) {
64: // static method
65: newCalled = null;
66: }
67: TypeReference classContext = new TypeRef(mbs.getBodySource());
68:
69: // removed this again. see bugs #437,#479 -- vladimir
70: // result = prettyNewObjectNames(result, methDecl, classContext);
71:
72: // at this point all arguments should be program variables
73: ArrayOfExpression argsAsParam = mbs.getArguments();
74:
75: HashMap map = new HashMap();
76: for (int i = 0; i < argsAsParam.size(); i++) {
77: map.put(methDecl.getParameterDeclarationAt(i)
78: .getVariableSpecification().getProgramVariable(),
79: argsAsParam.getExpression(i));
80: }
81: ProgVarReplaceVisitor paramRepl = new ProgVarReplaceVisitor(
82: result, map);
83: paramRepl.start();
84: result = (StatementBlock) paramRepl.result();
85:
86: return new MethodFrame(mbs.getResultVariable(),
87: new ExecutionContext(classContext, newCalled), result,
88: pm, PositionInfo.UNDEFINED);
89: }
90:
91: }
|