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.soundness;
12:
13: import java.util.HashSet;
14:
15: import de.uka.ilkd.key.java.visitor.ProgramVariableCollector;
16: import de.uka.ilkd.key.logic.JavaBlock;
17: import de.uka.ilkd.key.logic.Term;
18: import de.uka.ilkd.key.logic.Visitor;
19: import de.uka.ilkd.key.logic.op.ProgramVariable;
20:
21: public class TermProgramVariableCollector extends Visitor {
22:
23: private HashSet result = new HashSet();
24:
25: /** is called by the execPostOrder-method of a term
26: * @param Term to checked if it is a program variable and if true the
27: * variable is added to the list of found variables
28: */
29: public void visit(Term t) {
30: if (t.op() instanceof ProgramVariable) {
31: result.add(t.op());
32: }
33:
34: if (t.javaBlock() != JavaBlock.EMPTY_JAVABLOCK) {
35: ProgramVariableCollector pvc = new ProgramVariableCollector(
36: t.javaBlock().program());
37: pvc.start();
38: result.addAll(pvc.result());
39: }
40: }
41:
42: public HashSet result() {
43: return result;
44: }
45: }
|