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.soundness;
12:
13: import org.apache.log4j.Logger;
14:
15: import de.uka.ilkd.key.java.Services;
16: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
17: import de.uka.ilkd.key.logic.Constraint;
18: import de.uka.ilkd.key.logic.ProgramElementName;
19: import de.uka.ilkd.key.logic.Term;
20: import de.uka.ilkd.key.logic.op.*;
21: import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor;
22: import de.uka.ilkd.key.rule.inst.SVInstantiations;
23: import de.uka.ilkd.key.util.Debug;
24:
25: public class StaticCheckerSVI extends StaticChecker {
26:
27: private SVInstantiations svi;
28:
29: public StaticCheckerSVI(SVInstantiations p_svi, Services p_services) {
30: super (p_services);
31: svi = p_svi;
32: }
33:
34: public SVInstantiations getSVInstantiations() {
35: return svi;
36: }
37:
38: public void check(Term p_term) {
39: SyntacticalReplaceVisitor srv = new SyntacticalReplaceVisitor(
40: getServices(), getSVInstantiations(),
41: Constraint.BOTTOM, false, null, true, false);
42:
43: p_term.execPostOrder(srv);
44:
45: srv.getTerm().execPostOrder(this );
46: }
47:
48: public static boolean isValidType(Term p_formula,
49: SVInstantiations p_current, SchemaVariable p_sv,
50: KeYJavaType p_type, Services p_services) {
51: return isValidType(p_formula, p_current,
52: SLListOfSchemaVariable.EMPTY_LIST.prepend(p_sv),
53: p_type, p_services);
54: }
55:
56: public static boolean isValidType(Term p_formula,
57: SVInstantiations p_current, ListOfSchemaVariable p_svs,
58: KeYJavaType p_type, Services p_services) {
59:
60: return isValidType(p_formula, p_current, p_svs,
61: new LocationVariable(new ProgramElementName("x"),
62: p_type), p_services);
63: }
64:
65: public static boolean isValidType(Term p_formula,
66: SVInstantiations p_current, ListOfSchemaVariable p_svs,
67: IProgramVariable p_pv, Services p_services) {
68:
69: Logger.getLogger("key.taclet_soundness").debug(
70: "isValidType() with " + p_pv);
71:
72: try {
73: StaticCheckerSVI sc = new StaticCheckerSVI(
74: addInstantiation(p_current, p_svs, p_pv, 0),
75: p_services);
76: sc.check(p_formula);
77:
78: return true;
79: } catch (StaticTypeException e) {
80: // e.printStackTrace ();
81: Debug
82: .out("Exception thrown by class StaticCheckerSVI at check()");
83: }
84:
85: return false;
86: }
87:
88: public static SVInstantiations addInstantiation(
89: SVInstantiations p_current, ListOfSchemaVariable p_svs,
90: IProgramVariable p_pv, int p_instantiationType) {
91: IteratorOfSchemaVariable svIt;
92: for (svIt = p_svs.iterator(); svIt.hasNext();)
93: p_current = p_current.add(svIt.next(), p_pv,
94: p_instantiationType);
95:
96: return p_current;
97: }
98:
99: }
|