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.visitor;
12:
13: import java.util.HashSet;
14: import java.util.Iterator;
15:
16: import junit.framework.TestCase;
17: import de.uka.ilkd.key.java.Recoder2KeY;
18: import de.uka.ilkd.key.logic.JavaBlock;
19: import de.uka.ilkd.key.logic.Named;
20: import de.uka.ilkd.key.logic.NamespaceSet;
21: import de.uka.ilkd.key.rule.TacletForTests;
22:
23: public class TestDeclarationProgramVariableCollector extends TestCase {
24:
25: // some non sense java blocks with lots of statements and expressions
26: private static String[] jblocks = new String[] {
27: "{ int j1 = 0; int j2, j3, j4 = 0;}",
28: "{ int j1; { int j2; } { int j3; } for (int j4; j4=0; j4++) {} int j5; }",
29: "{ int j0; { { { { { int j1; } int j2; } int j3;} int j4; } } }" };
30:
31: // names of variables expected to be collected in jblocks
32: private static String[][] expectedVars = new String[][] {
33: { "j1", "j2", "j3", "j4" }, { "j1", "j5" }, { "j0" } };
34:
35: private static JavaBlock[] test_block = new JavaBlock[jblocks.length];
36:
37: private static int testCases = 0;
38: private static int down = 0;
39:
40: public TestDeclarationProgramVariableCollector(String name) {
41: super (name);
42: testCases++;
43: }
44:
45: public void setUp() {
46: if (down != 0)
47: return;
48: final Recoder2KeY r2k = new Recoder2KeY(TacletForTests
49: .services(), new NamespaceSet());
50: for (int i = 0; i < jblocks.length; i++) {
51: test_block[i] = r2k.readBlockWithEmptyContext(jblocks[i]);
52: }
53: }
54:
55: public void tearDown() {
56: down++;
57: if (down < testCases)
58: return;
59: test_block = null;
60: }
61:
62: private HashSet toNames(HashSet programVariables) {
63: HashSet result = new HashSet();
64: Iterator it = programVariables.iterator();
65: while (it.hasNext()) {
66: String name = "" + ((Named) it.next()).name();
67: if (result.contains(name)) {
68: System.out
69: .println("Warning: Program variables have same name."
70: + " Probably unsane test case");
71: }
72: result.add(name);
73: }
74: return result;
75: }
76:
77: public void testVisitor() {
78: DeclarationProgramVariableCollector dpvc;
79: for (int i = 0; i < jblocks.length; i++) {
80: dpvc = new DeclarationProgramVariableCollector(
81: test_block[i].program());
82: dpvc.start();
83: HashSet names = toNames(dpvc.result());
84:
85: assertTrue("Too many variables collected. Collected:"
86: + dpvc.result() + " in " + jblocks[i], dpvc
87: .result().size() <= expectedVars[i].length);
88:
89: for (int j = 0; j < expectedVars[i].length; j++) {
90: assertTrue("Missing variable: " + expectedVars[i][j]
91: + " of " + jblocks[i], names
92: .contains(expectedVars[i][j]));
93: }
94: }
95: }
96:
97: }
|