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.rule.encapsulation;
12:
13: import de.uka.ilkd.key.java.ProgramElement;
14: import de.uka.ilkd.key.java.SourceElement;
15: import de.uka.ilkd.key.java.declaration.VariableSpecification;
16: import de.uka.ilkd.key.java.visitor.JavaASTVisitor;
17: import de.uka.ilkd.key.logic.op.*;
18: import de.uka.ilkd.key.logic.sort.ObjectSort;
19:
20: class FreeProgramVariableDetector extends JavaASTVisitor {
21: private SetOfProgramVariable freeVars;
22: private SetOfProgramVariable declaredVars;
23:
24: public FreeProgramVariableDetector(ProgramElement root) {
25: super (root);
26: }
27:
28: protected void doAction(ProgramElement node) {
29: node.visit(this );
30: }
31:
32: protected void doDefaultAction(SourceElement node) {
33: }
34:
35: private boolean isLocalReferenceVar(ProgramVariable pv) {
36: return !pv.isMember() && pv.sort() instanceof ObjectSort;
37: }
38:
39: public boolean findFreePV() {
40: freeVars = SetAsListOfProgramVariable.EMPTY_SET;
41: declaredVars = SetAsListOfProgramVariable.EMPTY_SET;
42: walk(root());
43: return freeVars.size() > 0;
44: }
45:
46: public void performActionOnProgramVariable(ProgramVariable pv) {
47: if (isLocalReferenceVar(pv) && !declaredVars.contains(pv)) {
48: freeVars = freeVars.add(pv);
49: }
50: }
51:
52: public void performActionOnVariableSpecification(
53: VariableSpecification vs) {
54: ProgramVariable pv = (ProgramVariable) vs.getProgramVariable();
55: if (isLocalReferenceVar(pv)) {
56: freeVars = freeVars.remove(pv);
57: declaredVars = declaredVars.add(pv);
58: }
59: }
60:
61: public void performActionOnLocationVariable(LocationVariable x) {
62: performActionOnProgramVariable(x);
63: }
64:
65: public void performActionOnProgramConstant(ProgramConstant x) {
66: performActionOnProgramVariable(x);
67: }
68: }
|