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: package de.uka.ilkd.key.rule.metaconstruct;
11:
12: import de.uka.ilkd.key.java.ProgramElement;
13: import de.uka.ilkd.key.java.Statement;
14: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
15: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
16: import de.uka.ilkd.key.logic.Name;
17: import de.uka.ilkd.key.logic.op.ProgramMethod;
18: import de.uka.ilkd.key.logic.op.ProgramSV;
19: import de.uka.ilkd.key.logic.op.SchemaVariable;
20:
21: /**
22: * Symbolically executes a method invocation
23: */
24: public class MethodCallContract extends MethodCall {
25:
26: /** creates the methodcall-MetaConstruct
27: * @param result the SchemaVariable that is used to keep the result
28: * @param body the ProgramElement contained by the meta construct
29: */
30: public MethodCallContract(ProgramSV ec, SchemaVariable result,
31: ProgramElement body) {
32: super (new Name("method-call-contract"), ec, result, body);
33: }
34:
35: protected Statement makeIfCascade(ListOfKeYJavaType imps) {
36: ProgramMethod meth = getMethod(staticPrefixType, methRef);
37: return new MethodBodyStatement(meth, newContext, pvar,
38: arguments, true);
39: }
40:
41: }
|