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.java.visitor;
11:
12: import de.uka.ilkd.key.java.JavaProgramElement;
13: import de.uka.ilkd.key.java.ProgramElement;
14: import de.uka.ilkd.key.java.annotation.Annotation;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.op.ListOfSchemaVariable;
17: import de.uka.ilkd.key.logic.op.SLListOfSchemaVariable;
18: import de.uka.ilkd.key.logic.op.SchemaVariable;
19: import de.uka.ilkd.key.rule.inst.SVInstantiations;
20: import de.uka.ilkd.key.rule.metaconstruct.UnwindLoop;
21: import de.uka.ilkd.key.rule.metaconstruct.WhileInvRule;
22: import de.uka.ilkd.key.rule.metaconstruct.WhileInvRuleWrapper;
23:
24: /**
25: * This visitor is used to collect all appearing SchemaVariables in a
26: * java program
27: */
28: public class ProgramSVCollector extends JavaASTWalker {
29:
30: private ListOfSchemaVariable result = SLListOfSchemaVariable.EMPTY_LIST;
31:
32: /** the instantiations needed for unwind loop constructs */
33: private SVInstantiations instantiations = SVInstantiations.EMPTY_SVINSTANTIATIONS;
34:
35: /** create the ProgramSVCollector
36: * @param root the ProgramElement where to begin
37: * @param vars the ListOfSchemaVariable where to add the new found
38: * ones
39: */
40: public ProgramSVCollector(ProgramElement root,
41: ListOfSchemaVariable vars) {
42: super (root);
43: result = vars;
44: }
45:
46: /** create the ProgramSVCollector
47: * @param root the ProgramElement where to begin
48: * @param vars the ListOfSchemaVariable where to add the new found
49: * ones
50: * @param svInst the SVInstantiations previously found in order to determine
51: * the needed labels for the UnwindLoop construct.
52: */
53: public ProgramSVCollector(ProgramElement root,
54: ListOfSchemaVariable vars, SVInstantiations svInst) {
55: super (root);
56: result = vars;
57: instantiations = svInst;
58: }
59:
60: /** starts the walker*/
61: public void start() {
62: walk(root());
63: }
64:
65: public ListOfSchemaVariable getSchemaVariables() {
66: return result;
67: }
68:
69: /** the action that is performed just before leaving the node the
70: * last time
71: */
72: protected void doAction(ProgramElement node) {
73: // System.out.println("bbbbbbbbbbbbbbb "+node+(node instanceof WhileInvRuleWrapper));
74: if (node instanceof SchemaVariable) {
75: result = result.prepend((SchemaVariable) node);
76: } else if (node instanceof UnwindLoop) {
77: final UnwindLoop uwl = (UnwindLoop) node;
78: result = result.prepend(uwl.getInnerLabelSV()).prepend(
79: uwl.getOuterLabelSV());
80: } else if (node instanceof WhileInvRuleWrapper) {
81: Term t = ((WhileInvRuleWrapper) node).unwrap();
82: WhileInvRule wir = (WhileInvRule) t.op();
83: JavaProgramElement jpe = t.sub(0).javaBlock().program();
84: result = result.prepend(wir.neededInstantiations(
85: (ProgramElement) jpe, instantiations));
86: }
87: }
88:
89: protected void performActionOnAnnotationArray(Annotation[] a) {
90: // do nothing
91: }
92:
93: }
|