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.logic.Term;
15: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
16: import de.uka.ilkd.key.logic.op.Function;
17: import de.uka.ilkd.key.logic.op.Operator;
18: import de.uka.ilkd.key.logic.op.SVSubstitute;
19: import de.uka.ilkd.key.logic.op.SchemaVariable;
20: import de.uka.ilkd.key.rule.VariableConditionAdapter;
21: import de.uka.ilkd.key.rule.inst.SVInstantiations;
22:
23: /**
24: * ensures that the given instantiation for the schemavariable denotes
25: * a static method. For determining the method the callee and the
26: * arguments of the method are needed as arguments.
27: */
28: public class TestLiteral extends VariableConditionAdapter {
29:
30: private final SchemaVariable litSV1;
31: private final SchemaVariable litSV2;
32:
33: /**
34: * the static reference condition checks if a suggested
35: * instantiation for a schema variable denotes a static method
36: * call. The flag negation allows to reuse this condition for
37: * ensuring non static references.
38: */
39: public TestLiteral(SchemaVariable litSV1, SchemaVariable litSV2) {
40: this .litSV1 = litSV1;
41: this .litSV2 = litSV2;
42: }
43:
44: private boolean testLiteral(Term t, IntegerLDT ldt) {
45: Term lit = t;
46: Operator litOp = lit.op();
47: while (lit.arity() == 1) {
48: if (!(litOp instanceof Function)
49: || !(lit.arity() > 0 && ldt
50: .hasLiteralFunction((Function) litOp))) {
51: return false;
52: }
53: lit = lit.sub(0);
54: litOp = lit.op();
55: }
56: return litOp == ldt.getNumberTerminator();
57: }
58:
59: /**
60: * tests if the instantiation suggestions goes along with the static
61: * condition
62: * @param var the template Variable to be instantiated
63: * @param subst the SVSubstitute to be mapped to var
64: * @param svInst the SVInstantiations that are already known to be
65: * needed
66: * @return true iff condition is fulfilled
67: */
68: public boolean check(SchemaVariable var, SVSubstitute subst,
69: SVInstantiations svInst, Services services) {
70:
71: final IntegerLDT ldt = services.getTypeConverter()
72: .getIntegerLDT();
73: final Term lit1;
74: final Term lit2;
75: if (var == litSV1) {
76: lit1 = (Term) subst;
77: lit2 = (Term) svInst.getInstantiation(litSV2);
78: } else if (var == litSV2) {
79: lit1 = (Term) svInst.getInstantiation(litSV1);
80: lit2 = (Term) subst;
81: } else {
82: lit1 = (Term) svInst.getInstantiation(litSV1);
83: lit2 = (Term) svInst.getInstantiation(litSV2);
84: }
85: if (lit1 == null || lit2 == null) {
86: return true;
87: } else if (testLiteral(lit1, ldt) && testLiteral(lit2, ldt)) {
88: return !lit1.equals(lit2);
89: }
90: return false;
91: }
92:
93: public String toString() {
94: return "\\notSameLiteral(" + litSV1 + ", " + litSV2 + ")";
95: }
96:
97: }
|