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.conditions;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.java.reference.FieldReference;
15: import de.uka.ilkd.key.logic.op.ProgramConstant;
16: import de.uka.ilkd.key.logic.op.ProgramVariable;
17: import de.uka.ilkd.key.logic.op.SVSubstitute;
18: import de.uka.ilkd.key.logic.op.SchemaVariable;
19: import de.uka.ilkd.key.rule.VariableConditionAdapter;
20: import de.uka.ilkd.key.rule.inst.SVInstantiations;
21:
22: /**
23: * ensures that the given instantiation for the schemavariable denotes a
24: * static field
25: */
26: public class StaticReferenceCondition extends VariableConditionAdapter {
27:
28: private final SchemaVariable reference;
29: private final boolean negation;
30:
31: /**
32: * the static reference condition checks if a suggested
33: * instantiation for a schema variable denotes a static
34: * reference. The flag negation allows to reuse this condition for
35: * ensuring non static references.
36: */
37: public StaticReferenceCondition(SchemaVariable reference,
38: boolean negation) {
39: this .reference = reference;
40: this .negation = negation;
41: }
42:
43: /**
44: * tests if the instantiation suggestions goes along with the static
45: * condition
46: * @param var the template Variable to be instantiated
47: * @param subst the SVSubstitute to be mapped to var
48: * @param svInst the SVInstantiations that are already known to be
49: * needed
50: * @return true iff condition is fulfilled
51: */
52: public boolean check(SchemaVariable var, SVSubstitute subst,
53: SVInstantiations svInst, Services services) {
54:
55: if (var == reference) {
56: ProgramVariable attribute;
57: if (subst instanceof FieldReference) {
58: attribute = ((FieldReference) subst)
59: .getProgramVariable();
60: } else {
61: attribute = (ProgramVariable) subst;
62: }
63: return (negation ^ attribute.isStatic())
64: && !(attribute instanceof ProgramConstant);
65: }
66: return true;
67: }
68:
69: public String toString() {
70: return (negation ? " \\not " : "") + "\\static(" + reference
71: + ")";
72: }
73:
74: }
|