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.logic.op;
09:
10: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
11: import de.uka.ilkd.key.logic.ProgramElementName;
12: import de.uka.ilkd.key.logic.Term;
13: import de.uka.ilkd.key.logic.sort.Sort;
14:
15: /**
16: * This class represents all kind of local and instance variables. In addition it represents
17: * static variables, which are no compile time constants, i.e. which are not final or
18: * not initialised with a compile time constant.
19: *
20: */
21: public class LocationVariable extends ProgramVariable implements
22: Location {
23:
24: public LocationVariable(ProgramElementName name, KeYJavaType t,
25: KeYJavaType containingType, boolean isStatic,
26: boolean isModel, boolean isGhost) {
27: super (name, t.getSort(), t, containingType, isStatic, isModel,
28: isGhost);
29: }
30:
31: public LocationVariable(ProgramElementName name, KeYJavaType t,
32: KeYJavaType containingType, boolean isStatic) {
33: super (name, t.getSort(), t, containingType, isStatic, false,
34: false);
35: }
36:
37: public LocationVariable(ProgramElementName name, KeYJavaType t) {
38: super (name, t.getSort(), t, null, false, false, false);
39: }
40:
41: public LocationVariable(ProgramElementName name, Sort s) {
42: super (name, s, null, null, false, false, false);
43: }
44:
45: /**
46: * @return true if the value of "term" having this operator as
47: * top-level operator and may not be changed by modalities
48: */
49: public boolean isRigid(Term term) {
50: return false;
51: }
52:
53: /** calls the corresponding method of a visitor in order to
54: * perform some action/transformation on this element
55: * @param v the Visitor
56: */
57: public void visit(de.uka.ilkd.key.java.visitor.Visitor v) {
58: v.performActionOnLocationVariable(this);
59: }
60:
61: }
|