de.uka.ilkd.key.logic.op

Class ProgramConstant

java.lang.Object

de.uka.ilkd.key.logic.op.AbstractOperator

de.uka.ilkd.key.logic.op.AbstractSortedOperator

de.uka.ilkd.key.logic.op.ProgramVariable

de.uka.ilkd.key.logic.op.ProgramConstant

All Implemented Interfaces:

Expression, ModelElement, ProgramElement, ReferencePrefix, ReferenceSuffix, SourceElement, TerminalProgramElement, Named, IProgramVariable, Operator, ParsableVariable, SortedOperator, SVSubstitute, ProgramInLogic, Sorted

public final class ProgramConstant
extends ProgramVariable

This class represents currently only static final fields initialised with a compile time constant. These fields cannot occur on the left side of an update.

Field Summary

Fields

Modifier and Type	Field and Description
private Literal	compileTimeConstant

Constructor Summary

Constructors

Constructor and Description
ProgramConstant(ProgramElementName name, KeYJavaType t, KeYJavaType containingType, boolean isStatic, Literal compileTimeConstant)

Method Summary

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

Methods inherited from class de.uka.ilkd.key.logic.op.ProgramVariable

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

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractSortedOperator

additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractOperator

arity, bindVarsAt, isRigid, name, toString, validTopLevel, whereToBind

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.logic.op.SortedOperator

argSort, argSorts, sort

Methods inherited from interface de.uka.ilkd.key.logic.op.Operator

arity, bindVarsAt, isRigid, sort, validTopLevel

Methods inherited from interface de.uka.ilkd.key.logic.Named

name

Field Detail

compileTimeConstant

private final Literal compileTimeConstant

Constructor Detail

ProgramConstant

public ProgramConstant(ProgramElementName name,
                       KeYJavaType t,
                       KeYJavaType containingType,
                       boolean isStatic,
                       Literal compileTimeConstant)

Method Detail

getCompileTimeConstant

public Literal getCompileTimeConstant()

Returns:

the value of the initializer as a literal, if this variable is a compile-time constant, null otherwise

visit

public void visit(Visitor v)

Description copied from interface: SourceElement

calls the corresponding method of a visitor in order to perform some action/transformation on this element

Specified by:

visit in interface SourceElement

Overrides:

visit in class ProgramVariable

Parameters:

v - the Visitor

rename

public Operator rename(Name name)

Description copied from class: ProgramVariable

Returns an equivalent variable with the new name.

Specified by:

rename in class ProgramVariable

Parameters:

name - the new name

Returns:

equivalent operator with the new name