public abstract class ProgramVariable extends AbstractSortedOperator implements SourceElement, ProgramElement, Expression, ReferencePrefix, IProgramVariable, ParsableVariable, ReferenceSuffix, ProgramInLogic
Modifier and Type | Field and Description |
---|---|
private KeYJavaType |
containingType |
private boolean |
isFinal |
private boolean |
isGhost |
private boolean |
isModel |
private boolean |
isStatic |
private KeYJavaType |
type |
Modifier | Constructor and Description |
---|---|
protected |
ProgramVariable(ProgramElementName name,
Sort s,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost) |
protected |
ProgramVariable(ProgramElementName name,
Sort s,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost,
boolean isFinal) |
Modifier and Type | Method and Description |
---|---|
Expression |
convertToProgram(Term t,
ExtList l) |
boolean |
equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
equals modulo renaming is described in the corresponding
comment in class SourceElement.
|
Comment[] |
getComments()
Get comments.
|
KeYJavaType |
getContainerType()
returns the KeYJavaType where the program variable is declared or
null if the program variable denotes not a field
|
Position |
getEndPosition()
Returns the end position of the primary token of this element.
|
SourceElement |
getFirstElement()
Finds the source element that occurs first in the source.
|
SourceElement |
getFirstElementIncludingBlocks()
Finds the source element that occurs first in the source.
|
KeYJavaType |
getKeYJavaType() |
KeYJavaType |
getKeYJavaType(Services javaServ) |
KeYJavaType |
getKeYJavaType(Services javaServ,
ExecutionContext ec)
returns the
KeYJavaType of an expression |
SourceElement |
getLastElement()
Finds the source element that occurs last in the source.
|
PositionInfo |
getPositionInfo()
complete position information
|
ProgramElementName |
getProgramElementName() |
ReferencePrefix |
getReferencePrefix()
We do not have a prefix, so fake it!
|
Position |
getRelativePosition()
Returns the relative position (number of blank heading lines and
columns) of the primary token of this element.
|
Position |
getStartPosition()
Returns the start position of the primary token of this element.
|
boolean |
isFinal()
returns true iff the program variable has been declared as final
|
boolean |
isGhost()
returns true if the program variable has been declared as ghost
|
boolean |
isImplicit() |
boolean |
isMember()
returns true iff the program variable is a member
|
boolean |
isModel()
returns true iff the program variable has been declared as model
|
boolean |
isStatic()
returns true iff the program variable has been declared as static
|
MatchConditions |
match(SourceData source,
MatchConditions matchCond)
matches the source "text" (@link SourceData#getSource()) against the pattern represented
by this object.
|
void |
prettyPrint(PrettyPrinter w)
Pretty print.
|
java.lang.String |
proofToString() |
abstract 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
|
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 KeYJavaType type
private final boolean isStatic
private final boolean isModel
private final boolean isGhost
private final boolean isFinal
private final KeYJavaType containingType
protected ProgramVariable(ProgramElementName name, Sort s, KeYJavaType t, KeYJavaType containingType, boolean isStatic, boolean isModel, boolean isGhost, boolean isFinal)
protected ProgramVariable(ProgramElementName name, Sort s, KeYJavaType t, KeYJavaType containingType, boolean isStatic, boolean isModel, boolean isGhost)
public ProgramElementName getProgramElementName()
public boolean isStatic()
public boolean isModel()
public boolean isGhost()
public boolean isFinal()
public boolean isMember()
public KeYJavaType getContainerType()
public SourceElement getFirstElement()
SourceElement
getFirstElement
in interface SourceElement
SourceElement.getStartPosition()
public SourceElement getFirstElementIncludingBlocks()
SourceElement
getFirstElementIncludingBlocks
in interface SourceElement
SourceElement.getStartPosition()
public SourceElement getLastElement()
SourceElement
getLastElement
in interface SourceElement
SourceElement.getEndPosition()
public Comment[] getComments()
ProgramElement
getComments
in interface ProgramElement
public void visit(Visitor v)
SourceElement
visit
in interface SourceElement
v
- the Visitorpublic void prettyPrint(PrettyPrinter w) throws java.io.IOException
SourceElement
prettyPrint
in interface SourceElement
w
- a pretty printer.java.io.IOException
- occasionally thrown.public Position getStartPosition()
SourceElement
getFirstElement()
.getStartPosition
in interface SourceElement
public Position getEndPosition()
SourceElement
getLastElement()
.getEndPosition
in interface SourceElement
public Position getRelativePosition()
SourceElement
getFirstElement()
.getRelativePosition
in interface SourceElement
public PositionInfo getPositionInfo()
SourceElement
getPositionInfo
in interface SourceElement
public KeYJavaType getKeYJavaType()
getKeYJavaType
in interface IProgramVariable
public KeYJavaType getKeYJavaType(Services javaServ)
getKeYJavaType
in interface IProgramVariable
public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec)
Expression
KeYJavaType
of an expressiongetKeYJavaType
in interface Expression
getKeYJavaType
in interface IProgramVariable
public ReferencePrefix getReferencePrefix()
getReferencePrefix
in interface ReferencePrefix
public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat)
equalsModRenaming
in interface SourceElement
public Expression convertToProgram(Term t, ExtList l)
convertToProgram
in interface ProgramInLogic
public java.lang.String proofToString()
public boolean isImplicit()
public MatchConditions match(SourceData source, MatchConditions matchCond)
ProgramElement
MatchConditions
with
the found instantiations of the schemavariables. If the match
failed, null is returned instead.match
in interface ProgramElement
source
- the SourceData with the program element to matchmatchCond
- the MatchConditions found up to this point