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.rule.conditions;
09:
10: import de.uka.ilkd.key.java.Label;
11: import de.uka.ilkd.key.java.ProgramElement;
12: import de.uka.ilkd.key.java.Services;
13: import de.uka.ilkd.key.java.visitor.FreeLabelFinder;
14: import de.uka.ilkd.key.logic.op.SVSubstitute;
15: import de.uka.ilkd.key.logic.op.SchemaVariable;
16: import de.uka.ilkd.key.rule.VariableConditionAdapter;
17: import de.uka.ilkd.key.rule.inst.SVInstantiations;
18:
19: public class FreeLabelInVariableCondition extends
20: VariableConditionAdapter {
21:
22: private final SchemaVariable label;
23: private final SchemaVariable statement;
24: private final boolean negated;
25: private final FreeLabelFinder freeLabelFinder = new FreeLabelFinder();
26:
27: public FreeLabelInVariableCondition(SchemaVariable label,
28: SchemaVariable statement, boolean negated) {
29: this .label = label;
30: this .statement = statement;
31: this .negated = negated;
32: }
33:
34: public boolean check(SchemaVariable var,
35: SVSubstitute instCandidate, SVInstantiations instMap,
36: Services services) {
37: Label prgLabel = null;
38: ProgramElement program = null;
39:
40: if (var == label) {
41: prgLabel = (Label) instCandidate;
42: program = (ProgramElement) instMap
43: .getInstantiation(statement);
44: } else if (var == statement) {
45: prgLabel = (Label) instMap.getInstantiation(label);
46: program = (ProgramElement) instCandidate;
47: }
48:
49: if (program == null || prgLabel == null) {
50: // not yet complete or not responsible
51: return true;
52: }
53:
54: final boolean freeIn = freeLabelFinder.findLabel(prgLabel,
55: program);
56: return negated ? !freeIn : freeIn;
57: }
58:
59: public String toString() {
60: return (negated ? "\\not" : "") + "\\freeLabelIn ("
61: + label.name() + "," + statement.name() + ")";
62: }
63:
64: }
|