public class AbstractUpdateExtractor.ExtractLocationParameter
extends java.lang.Object
Instances of this class provides the Term
which are required
to compute a location (value or association of a given object/state).
Instances of this class can be used to compute the values in each memory layout.
So they are instantiated during the analyzation phase
SymbolicLayoutExtractor.analyse()
once for initial and current memory layout.
Modifier and Type | Field and Description |
---|---|
private Term |
arrayEndIndex
The array end index or
null if not used. |
private Term |
arrayIndex
The array index or
null if not used. |
private Term |
arrayRangeConstant
The constant used to query an array range.
|
private Term |
arrayStartIndex
The array start index or
null if not used. |
private Term |
notAValue
The constant representing the fact that no value is available.
|
private Term |
parentTerm
An optional parent object represented as
Term . |
private int |
parentTermIndexInStatePredicate
The index of the parent argument in the predicate used in side proof to compute the values.
|
private LocationVariable |
preVariable
The
LocationVariable which is used to make sure that the defined parent object
of the initial state is used, because the expression (e.g. |
private ProgramVariable |
programVariable
The
ProgramVariable or null if an array index is used instead. |
private boolean |
stateMember
Defines if this location should explicitly be shown on the state.
|
private int |
valueTermIndexInStatePredicate
The index of the value argument in the predicate used in side proof to compute the values.
|
Modifier | Constructor and Description |
---|---|
|
ExtractLocationParameter(AbstractUpdateExtractor.ExtractLocationParameter original,
Term newParent)
Constructor for cloning purpose.
|
|
ExtractLocationParameter(ProgramVariable programVariable,
boolean stateMember)
Constructor.
|
|
ExtractLocationParameter(ProgramVariable programVariable,
Term parentTerm)
Constructor.
|
protected |
ExtractLocationParameter(ProgramVariable programVariable,
Term parentTerm,
boolean stateMember)
Constructor.
|
|
ExtractLocationParameter(Term arrayIndex,
Term parentTerm)
Constructor.
|
|
ExtractLocationParameter(Term arrayStartIndex,
Term arrayEndIndex,
Term parentTerm)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected LocationVariable |
createLocationVariable(java.lang.String name,
Sort sort)
Creates a new
LocationVariable with the given name and Sort . |
Term |
createPreParentTerm()
Creates the
Term to compute the parent object with help of the pre update. |
Term |
createPreUpdate()
Creates the pre update to make sure that the parent object defined
by the expression is evaluated on the initial state because it might
be changed in the current state due to updates.
|
Term |
createPreValueTerm()
Computes the
Term to compute the value with help of the pre update. |
boolean |
equals(java.lang.Object obj) |
Term |
getArrayEndIndex()
Returns the array end index.
|
Term |
getArrayIndex()
Returns the array index.
|
Term |
getArrayRangeConstant()
Returns the constant used to query an array range.
|
Term |
getArrayStartIndex()
Returns the array start index.
|
Term |
getNotAValue()
Returns the constant representing the fact that no value is available.
|
Term |
getParentTerm()
Returns the optional parent object represented as
Term . |
int |
getParentTermIndexInStatePredicate()
Returns the index of the parent argument in the predicate used in side proof to compute the values.
|
Term |
getPreUpdateTarget()
Returns the right side of the update created by
createPreUpdate() . |
LocationVariable |
getPreVariable()
Returns the pre variable.
|
ProgramVariable |
getProgramVariable()
Returns the
ProgramVariable or null if an array index is used instead. |
int |
getValueTermIndexInStatePredicate()
Returns the index of the value argument in the predicate used in side proof to compute the values.
|
int |
hashCode() |
boolean |
isArrayIndex()
Checks if an array index is represented.
|
boolean |
isArrayRange()
Checks if an array range is represented.
|
boolean |
isStateMember()
Checks if this location should explicitly be shown on the state.
|
void |
setParentTermIndexInStatePredicate(int selectParentTermIndexInStatePredicate)
Sets the index of the parent argument in the predicate used in side proof to compute the values.
|
void |
setValueTermIndexInStatePredicate(int selectValueTermIndexInStatePredicate)
Sets the index of the value argument in the predicate used in side proof to compute the values.
|
java.lang.String |
toString() |
private final ProgramVariable programVariable
ProgramVariable
or null
if an array index is used instead.private final Term arrayIndex
null
if not used.private final Term arrayStartIndex
null
if not used.private final Term arrayEndIndex
null
if not used.private final Term parentTerm
Term
. If it is null
an IProgramVariable
of the state is represented.private int parentTermIndexInStatePredicate
private int valueTermIndexInStatePredicate
private final LocationVariable preVariable
LocationVariable
which is used to make sure that the defined parent object
of the initial state is used, because the expression (e.g. x.next
) might refer
to different objects in the current state.private final boolean stateMember
private final Term arrayRangeConstant
private final Term notAValue
public ExtractLocationParameter(AbstractUpdateExtractor.ExtractLocationParameter original, Term newParent)
original
- The original AbstractUpdateExtractor.ExtractLocationParameter
to clone.newParent
- The new parent Term
to be used instead of the original one.public ExtractLocationParameter(ProgramVariable programVariable, boolean stateMember) throws ProofInputException
programVariable
- The ProgramVariable
.stateMember
- Defines if this location should explicitly be shown on the state.ProofInputException
- Occurred Exception.public ExtractLocationParameter(ProgramVariable programVariable, Term parentTerm) throws ProofInputException
programVariable
- The ProgramVariable
.parentTerm
- The parent object represented as Term
.ProofInputException
- Occurred Exception.protected ExtractLocationParameter(ProgramVariable programVariable, Term parentTerm, boolean stateMember) throws ProofInputException
programVariable
- The ProgramVariable
.parentTerm
- The parent object represented as Term
.stateMember
- Defines if this location should explicitly be shown on the state.ProofInputException
- Occurred Exception.public ExtractLocationParameter(Term arrayIndex, Term parentTerm) throws ProofInputException
arrayIndex
- The array index.parentTerm
- The parent object represented as Term
.ProofInputException
- Occurred Exception.public ExtractLocationParameter(Term arrayStartIndex, Term arrayEndIndex, Term parentTerm) throws ProofInputException
arrayStartIndex
- The array start index.arrayEndIndex
- The array end index.parentTerm
- The parent object represented as Term
.ProofInputException
- Occurred Exception.protected LocationVariable createLocationVariable(java.lang.String name, Sort sort) throws ProofInputException
LocationVariable
with the given name and Sort
.name
- The name of the new variable.sort
- The Sort
of the new variable.LocationVariable
.ProofInputException
- Occurred Exception.public boolean isStateMember()
public boolean isArrayIndex()
true
is array index, false
is something else.public boolean isArrayRange()
true
is array range, false
is something else.public Term getArrayIndex()
public Term getArrayStartIndex()
public Term getArrayEndIndex()
public Term getArrayRangeConstant()
public Term getNotAValue()
public LocationVariable getPreVariable()
public Term getPreUpdateTarget()
createPreUpdate()
.createPreUpdate()
.public Term createPreUpdate()
Term
with the pre update.public Term createPreParentTerm()
Term
to compute the parent object with help of the pre update.Term
to compute the parent object with help of the pre update.public Term createPreValueTerm()
Term
to compute the value with help of the pre update.Term
to compute the value with help of the pre update.public ProgramVariable getProgramVariable()
ProgramVariable
or null
if an array index is used instead.ProgramVariable
or null
if an array index is used instead.public Term getParentTerm()
Term
. If it is null
an IProgramVariable
of the state is represented.Term
. If it is null
an IProgramVariable
of the state is represented.public int getParentTermIndexInStatePredicate()
public void setParentTermIndexInStatePredicate(int selectParentTermIndexInStatePredicate)
selectParentTermIndexInStatePredicate
- The index of the parent argument in the predicate used in side proof to compute the values.public int getValueTermIndexInStatePredicate()
public void setValueTermIndexInStatePredicate(int selectValueTermIndexInStatePredicate)
selectValueTermIndexInStatePredicate
- The index of the value argument in the predicate used in side proof to compute the values.public java.lang.String toString()
toString
in class java.lang.Object
public boolean equals(java.lang.Object obj)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object