de.uka.ilkd.key.logic.op

Class LocationVariable

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.LocationVariable

All Implemented Interfaces:

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

public final class LocationVariable
extends ProgramVariable
implements UpdateableOperator

This class represents proper program variables, which are not program constants. See the description of the superclass ProgramVariable for more information.

Constructor Summary

Constructors

Constructor and Description
LocationVariable(ProgramElementName name, KeYJavaType t)
LocationVariable(ProgramElementName name, KeYJavaType t, boolean isFinal)
LocationVariable(ProgramElementName name, KeYJavaType t, boolean isGhost, boolean isFinal)
LocationVariable(ProgramElementName name, KeYJavaType t, KeYJavaType containingType, boolean isStatic, boolean isModel)
LocationVariable(ProgramElementName name, KeYJavaType t, KeYJavaType containingType, boolean isStatic, boolean isModel, boolean isGhost, boolean isFinal)
LocationVariable(ProgramElementName name, Sort s)

Method Summary

Modifier and Type	Method and Description
UpdateableOperator	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

Constructor Detail

LocationVariable

public LocationVariable(ProgramElementName name,
                        KeYJavaType t,
                        KeYJavaType containingType,
                        boolean isStatic,
                        boolean isModel,
                        boolean isGhost,
                        boolean isFinal)

LocationVariable

public LocationVariable(ProgramElementName name,
                        KeYJavaType t,
                        KeYJavaType containingType,
                        boolean isStatic,
                        boolean isModel)

LocationVariable

public LocationVariable(ProgramElementName name,
                        KeYJavaType t)

LocationVariable

public LocationVariable(ProgramElementName name,
                        KeYJavaType t,
                        boolean isFinal)

LocationVariable

public LocationVariable(ProgramElementName name,
                        KeYJavaType t,
                        boolean isGhost,
                        boolean isFinal)

LocationVariable

public LocationVariable(ProgramElementName name,
                        Sort s)

Method Detail

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 UpdateableOperator 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