public final class ProgramConstant extends ProgramVariable
Modifier and Type | Field and Description |
---|---|
private Literal |
compileTimeConstant |
Constructor and Description |
---|
ProgramConstant(ProgramElementName name,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
Literal compileTimeConstant) |
Modifier and Type | Method and Description |
---|---|
Literal |
getCompileTimeConstant() |
Operator |
rename(Name name)
Returns an equivalent variable with the new name.
|
void |
visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
convertToProgram, equalsModRenaming, getComments, getContainerType, getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getKeYJavaType, getKeYJavaType, getKeYJavaType, getLastElement, getPositionInfo, getProgramElementName, getReferencePrefix, getRelativePosition, getStartPosition, isFinal, isGhost, isImplicit, isMember, isModel, isStatic, match, prettyPrint, proofToString
additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort
arity, bindVarsAt, isRigid, name, toString, validTopLevel, whereToBind
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
argSort, argSorts, sort
arity, bindVarsAt, isRigid, sort, validTopLevel
private final Literal compileTimeConstant
public ProgramConstant(ProgramElementName name, KeYJavaType t, KeYJavaType containingType, boolean isStatic, Literal compileTimeConstant)
public Literal getCompileTimeConstant()
public void visit(Visitor v)
SourceElement
visit
in interface SourceElement
visit
in class ProgramVariable
v
- the Visitorpublic Operator rename(Name name)
ProgramVariable
rename
in class ProgramVariable
name
- the new name