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.java.expression.Literal;
12: import de.uka.ilkd.key.logic.ProgramElementName;
13: import de.uka.ilkd.key.logic.Term;
14:
15: /**
16: * This class represents currently only static final fields initialised with
17: * a compile time constant. These fields cannot occur on the left side of an
18: * update.
19: */
20: public class ProgramConstant extends ProgramVariable {
21:
22: // the value of the initializer as a literal, if this variable is
23: // a compile-time constant, <code>null</code> otherwise
24: private final Literal compileTimeConstant;
25:
26: public ProgramConstant(ProgramElementName name, KeYJavaType t,
27: KeYJavaType containingType, boolean isStatic,
28: Literal compileTimeConstant) {
29: super (name, t.getSort(), t, containingType, isStatic, false,
30: false);
31: this .compileTimeConstant = compileTimeConstant;
32: }
33:
34: /**
35: * @return the value of the initializer as a literal, if this
36: * variable is a compile-time constant, </code>null</code>
37: * otherwise
38: */
39: public Literal getCompileTimeConstant() {
40: return compileTimeConstant;
41: }
42:
43: /**
44: * @return true if the value of "term" having this operator as
45: * top-level operator and may not be changed by modalities
46: */
47: public boolean isRigid(Term t) {
48: return t.arity() == 0 && t.op() == this ;
49: }
50:
51: /** calls the corresponding method of a visitor in order to
52: * perform some action/transformation on this element
53: * @param v the Visitor
54: */
55: public void visit(de.uka.ilkd.key.java.visitor.Visitor v) {
56: v.performActionOnProgramConstant(this);
57: }
58: }
|