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.java;
12:
13: import junit.framework.TestCase;
14: import de.uka.ilkd.key.logic.JavaBlock;
15: import de.uka.ilkd.key.logic.NamespaceSet;
16: import de.uka.ilkd.key.logic.PosInProgram;
17: import de.uka.ilkd.key.rule.TacletForTests;
18: import de.uka.ilkd.key.util.ExtList;
19:
20: public class TestContextStatementBlock extends TestCase {
21:
22: JavaBlock blockOne;
23:
24: public TestContextStatementBlock(String name) {
25: super (name);
26: }
27:
28: public void setUp() {
29: JavaInfo ji = TacletForTests.javaInfo();
30: Recoder2KeY c2k = new Recoder2KeY(ji.getKeYProgModelInfo()
31: .getServConf(), ji.rec2key(), new NamespaceSet(),
32: TacletForTests.services().getTypeConverter());
33: blockOne = c2k.readBlock("{int a=1; {int b=3; b++;} a++;}", c2k
34: .createEmptyContext());
35:
36: }
37:
38: public void tearDown() {
39: blockOne = null;
40: }
41:
42: public void testContextTermInstantiation() {
43: ExtList statementList = new ExtList();
44: StatementBlock stContainer = (StatementBlock) blockOne
45: .program();
46: int size = stContainer.getChildCount();
47: assertTrue("Wrong size. Should have only 3 children", size == 3);
48: PosInProgram prefixEnd = PosInProgram.TOP.down(0);
49: assertTrue(
50: "Prefix should end with an assignment",
51: PosInProgram
52: .getProgramAt(prefixEnd, blockOne.program()) instanceof de.uka.ilkd.key.java.declaration.LocalVariableDeclaration);
53: PosInProgram suffixStart = PosInProgram.TOP.down(2);
54: assertTrue(
55: "Suffix should start with an ++",
56: PosInProgram.getProgramAt(suffixStart, blockOne
57: .program()) instanceof de.uka.ilkd.key.java.expression.operator.PostIncrement);
58: for (int i = size - 2; i >= 1; i--) {
59: statementList.add((Statement) stContainer.getChildAt(i));
60: }
61:
62: }
63:
64: }
|