public static class AbstractUpdateExtractor.ExecutionVariableValuePair
extends java.lang.Object
Represents a location (value or association of a given object/state) in a concrete memory layout of the initial or current state.
They are instantiated lazily when a concrete memory layout is requested
the first during lazily computation
SymbolicLayoutExtractor#lazyComputeLayout(Node, ImmutableSet, Term, Set, ImmutableList, Term, String)
.
The instances exists only temporary until the concrete ISymbolicLayout
was created from them.
Constructor and Description |
---|
ExecutionVariableValuePair(ProgramVariable programVariable,
Term parent,
Term value,
Term condition,
boolean stateMember,
Node goalNode)
Constructor.
|
ExecutionVariableValuePair(Term arrayIndex,
Term parent,
Term value,
Term condition,
boolean stateMember,
Node goalNode)
Constructor.
|
ExecutionVariableValuePair(Term arrayStartIndex,
Term arrayEndIndex,
Term arrayRangeConstant,
Term parent,
Term value,
Term condition,
boolean stateMember,
Node goalNode)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
boolean |
equals(java.lang.Object obj) |
Term |
getArrayEndIndex()
Returns the array end index.
|
Term |
getArrayIndex()
Returns the array index.
|
Term |
getArrayStartIndex()
Returns the array start index.
|
Term |
getCondition()
Returns the optional condition under which the value is valid.
|
Node |
getGoalNode()
Returns the
Node on which this result is based on. |
Term |
getParent()
Returns the optional parent object or
null if it is a value/association of the state. |
ProgramVariable |
getProgramVariable()
Returns the
ProgramVariable or null if an array index is used instead. |
Term |
getValue()
Returns the value or association target.
|
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.
|
java.lang.String |
toString() |
public ExecutionVariableValuePair(ProgramVariable programVariable, Term parent, Term value, Term condition, boolean stateMember, Node goalNode)
programVariable
- The ProgramVariable
.parent
- An optional parent object or null
if it is a value/association of the state.value
- The value or association target.condition
- An optional condition under which the value is valid.stateMember
- Defines if this location should explicitly be shown on the state.public ExecutionVariableValuePair(Term arrayIndex, Term parent, Term value, Term condition, boolean stateMember, Node goalNode)
arrayIndex
- The array index.parent
- The parent object.value
- The value or association target.condition
- An optional condition under which the value is valid.stateMember
- Defines if this location should explicitly be shown on the state.public ExecutionVariableValuePair(Term arrayStartIndex, Term arrayEndIndex, Term arrayRangeConstant, Term parent, Term value, Term condition, boolean stateMember, Node goalNode)
arrayStartIndex
- The array start index.arrayEndIndex
- The array end index.arrayRangeConstant
- The constant used to query an array range.parent
- The parent object.value
- The value or association target.condition
- An optional condition under which the value is valid.stateMember
- Defines if this location should explicitly be shown on the state.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 getParent()
null
if it is a value/association of the state.null
if it is a value/association of the state.public Term getValue()
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 boolean isStateMember()
public Term getCondition()
public Node getGoalNode()
Node
on which this result is based on.Node
on which this result is based on.public boolean equals(java.lang.Object obj)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.