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: package de.uka.ilkd.key.unittest;
09:
10: import de.uka.ilkd.key.java.*;
11: import de.uka.ilkd.key.logic.*;
12: import de.uka.ilkd.key.proof.mgt.InstantiatedMethodContract;
13: import de.uka.ilkd.key.rule.UseMethodContractRule;
14: import de.uka.ilkd.key.rule.metaconstruct.ExpandMethodBody;
15: import de.uka.ilkd.key.rule.updatesimplifier.Update;
16:
17: public class UseMethodContractRuleForTestGen extends
18: UseMethodContractRule {
19:
20: /** The only instance of this rule */
21: public static UseMethodContractRule INSTANCE = new UseMethodContractRuleForTestGen();
22:
23: private Name name = new Name(
24: "Use Method Contract (TestCase Gen. version)");
25:
26: private UseMethodContractRuleForTestGen() {
27: }
28:
29: protected UseMethodContractRule getContractRule() {
30: return UseMethodContractRuleForTestGen.INSTANCE;
31: }
32:
33: /**
34: * returns the name of this rule
35: */
36: public Name name() {
37: return name;
38: }
39:
40: protected Term preFma(InstantiatedMethodContract iCt,
41: MbsInfo mbsPos, UpdateFactory uf, Update u,
42: Services services) {
43:
44: ExpandMethodBody exMB = new ExpandMethodBody(mbsPos.mbs);
45: StatementBlock methodReplaceStatements = new StatementBlock(
46: (Statement) exMB.symbolicExecution(mbsPos.mbs,
47: services, null));
48:
49: final Term focus = mbsPos.pio.subTerm();
50: final JavaNonTerminalProgramElement all = (JavaNonTerminalProgramElement) focus
51: .javaBlock().program();
52: final NonTerminalProgramElement npe = replaceStatement(all,
53: mbsPos, methodReplaceStatements);
54: Term restFma = TermBuilder.DF.tf().createProgramTerm(
55: iCt.getModality(),
56: JavaBlock.createJavaBlock((StatementBlock) npe),
57: focus.sub(0));
58:
59: return uf.apply(u, restFma);
60: // return postFmaHelp(iCt, mbsPos, uf, u, methodReplaceStatements, extraPre);
61: }
62:
63: protected String getPreLabel() {
64: return "Expanded Method Body";
65: }
66:
67: }
|