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: package de.uka.ilkd.key.java.visitor;
09:
10: import de.uka.ilkd.key.java.Label;
11: import de.uka.ilkd.key.java.NonTerminalProgramElement;
12: import de.uka.ilkd.key.java.ProgramElement;
13: import de.uka.ilkd.key.java.statement.LabeledStatement;
14:
15: /**
16: * descends recursively a given program and looks for free occurrences of a specified label
17: */
18: public class FreeLabelFinder {
19:
20: public FreeLabelFinder() {
21: }
22:
23: public boolean findLabel(Label label, ProgramElement node) {
24: if (!(node instanceof LabeledStatement && ((LabeledStatement) node)
25: .getLabel().equals(label))) {
26: if (node instanceof NonTerminalProgramElement) {
27: final NonTerminalProgramElement nonTerminalNode = (NonTerminalProgramElement) node;
28: for (int i = 0; i < nonTerminalNode.getChildCount(); i++) {
29: if (nonTerminalNode.getChildAt(i) != null) {
30: if (findLabel(label, nonTerminalNode
31: .getChildAt(i))) {
32: return true;
33: }
34: }
35: }
36: } else if (node instanceof Label) {
37: if (node.equals(label)) {
38: return true;
39: }
40: }
41: }
42: return false;
43: }
44:
45: }
|