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.Expression;
14: import de.uka.ilkd.key.java.Services;
15: import de.uka.ilkd.key.java.reference.TypeReference;
16: import de.uka.ilkd.key.logic.Term;
17: import de.uka.ilkd.key.logic.op.SVSubstitute;
18: import de.uka.ilkd.key.logic.op.SchemaVariable;
19: import de.uka.ilkd.key.logic.sort.ArraySort;
20: import de.uka.ilkd.key.logic.sort.ObjectSort;
21: import de.uka.ilkd.key.logic.sort.Sort;
22: import de.uka.ilkd.key.rule.VariableConditionAdapter;
23: import de.uka.ilkd.key.rule.inst.SVInstantiations;
24:
25: /**
26: * This variable condition checks if an array component is of reference type
27: */
28: public class ArrayComponentTypeCondition extends
29: VariableConditionAdapter {
30:
31: private SchemaVariable var;
32: private boolean checkReferenceType;
33:
34: /**
35: * creates an instance of this condition checking if array var has reference
36: * or primitive component type depending on the value of
37: * <code>checkReferenceType</code>
38: * @param var the SchemaVariable to be checked
39: * @param checkReferenceType the boolean flag which when is set (<tt>true</tt>)
40: * checks for reference otherwise for primitive type
41: */
42: public ArrayComponentTypeCondition(SchemaVariable var,
43: boolean checkReferenceType) {
44: this .var = var;
45: this .checkReferenceType = checkReferenceType;
46: }
47:
48: /**
49: * checks if the condition for a correct instantiation is fulfilled
50: * @param var the template Variable to be instantiated
51: * @param candidate the SVSubstitute which is a candidate for an
52: * instantiation of var
53: * @param svInst the SVInstantiations that are already known to be needed
54: * @return true iff condition is fulfilled
55: */
56: public boolean check(SchemaVariable var, SVSubstitute candidate,
57: SVInstantiations svInst, Services services) {
58: if (var != this .var)
59: return true;
60: Sort s = null;
61: if (candidate instanceof Term) {
62: s = ((Term) candidate).sort();
63: } else if (candidate instanceof Expression) {
64: s = ((Expression) candidate).getKeYJavaType(services,
65: svInst.getExecutionContext()).getSort();
66: } else if (candidate instanceof TypeReference) {
67: s = ((TypeReference) candidate).getKeYJavaType().getSort();
68: }
69:
70: if (s == null || !(s instanceof ArraySort)) {
71: return false;
72: }
73: return !(((ArraySort) s).elementSort() instanceof ObjectSort)
74: ^ checkReferenceType;
75: }
76:
77: public String toString() {
78: return (checkReferenceType ? "" : " \\not ")
79: + "\\isReferenceArray(" + var + ")";
80: }
81:
82: }
|