001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010: package de.uka.ilkd.key.java.visitor;
011:
012: import java.util.HashSet;
013:
014: import de.uka.ilkd.key.java.ProgramElement;
015: import de.uka.ilkd.key.java.SourceElement;
016: import de.uka.ilkd.key.java.annotation.Annotation;
017: import de.uka.ilkd.key.java.annotation.LoopInvariantAnnotation;
018: import de.uka.ilkd.key.logic.ArrayOfTerm;
019: import de.uka.ilkd.key.logic.Term;
020: import de.uka.ilkd.key.logic.op.AttributeOp;
021: import de.uka.ilkd.key.logic.op.LocationVariable;
022: import de.uka.ilkd.key.logic.op.ProgramConstant;
023: import de.uka.ilkd.key.logic.op.ProgramVariable;
024:
025: /**
026: * Walks through a java AST in depth-left-fist-order.
027: * This walker is used collect all ProgramVariables in a program.
028: */
029: public class ProgramVariableCollector extends JavaASTVisitor {
030:
031: private HashSet result = new HashSet();
032: private boolean wAnnotations;
033:
034: /**
035: * collects all program variables occuring in the AST <tt>root</tt>
036: * using this constructor is equivalent to <tt>ProggramVariableCollector(root, false)</tt>
037: * @param root the ProgramElement which is the root of the AST
038: */
039: public ProgramVariableCollector(ProgramElement root) {
040: super (root);
041: }
042:
043: /**
044: * collects all program variables occuring in the AST <tt>root</tt>
045: *
046: * @param root the ProgramElement which is the root of the AST
047: * @param wAnnotations a boolean flag, if set to true program variables in
048: * annotations will be collected, too
049: */
050: public ProgramVariableCollector(ProgramElement root,
051: boolean wAnnotations) {
052: super (root);
053: this .wAnnotations = wAnnotations;
054: }
055:
056: /** the action that is performed just before leaving the node the
057: * last time
058: */
059: protected void doAction(ProgramElement node) {
060: node.visit(this );
061: }
062:
063: /** starts the walker*/
064: public void start() {
065: walk(root());
066: }
067:
068: public HashSet result() {
069: return result;
070: }
071:
072: public String toString() {
073: return result.toString();
074: }
075:
076: protected void doDefaultAction(SourceElement x) {
077: }
078:
079: public void performActionOnProgramVariable(ProgramVariable pv) {
080: result.add(pv);
081: }
082:
083: private void performActionOnTerm(Term t) {
084: if (t != null) {
085: if (t.op() instanceof AttributeOp) {
086: result.add(((AttributeOp) t.op()).attribute());
087: } else if (t.op() instanceof ProgramVariable) {
088: result.add(t.op());
089: }
090:
091: for (int i = 0, ar = t.arity(); i < ar; i++) {
092: performActionOnTerm(t.sub(i));
093: }
094: }
095: }
096:
097: public void performActionOnAnnotationArray(Annotation[] a) {
098: if (wAnnotations) {
099: for (int i = 0; i < a.length; i++) {
100: if (a[i] instanceof LoopInvariantAnnotation) {
101: LoopInvariantAnnotation lia = (LoopInvariantAnnotation) a[i];
102: if (lia.invariant() != null) {
103: performActionOnTerm(lia.invariant());
104: }
105:
106: if (lia.variant() != null) {
107: performActionOnTerm(lia.variant());
108: }
109:
110: if (lia.post() != null) {
111: performActionOnTerm(lia.post());
112: }
113:
114: final ArrayOfTerm terms = lia.olds();
115: for (int j = 0, len = terms.size(); j < len; j++) {
116: performActionOnTerm(terms.getTerm(j));
117: }
118: } else {
119: doDefaultAction(a[i]);
120: }
121: }
122: }
123: }
124:
125: public void performActionOnLocationVariable(LocationVariable x) {
126: performActionOnProgramVariable(x);
127: }
128:
129: public void performActionOnProgramConstant(ProgramConstant x) {
130: performActionOnProgramVariable(x);
131: }
132:
133: }
|