AbstractUpdateExtractor.ExecutionVariableValuePair (KeY API Documentation)

java.lang.Object
- de.uka.ilkd.key.symbolic_execution.AbstractUpdateExtractor.ExecutionVariableValuePair

Enclosing class:

AbstractUpdateExtractor
```
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.

Author:

Martin Hentschel

Field Summary

Fields
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`	`arrayStartIndex` The array start index or `null` if not used.
`private Term`	`condition` An optional condition under which the value is valid.
`private Node`	`goalNode` The `Node` on which this result is based on.
`private Term`	`parent` An optional parent object or `null` if it is a value/association of the state.
`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 Term`	`value` The value or association target.

Constructor Summary

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

Method Summary

All Methods Instance Methods Concrete Methods
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()`

Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait

- Field Detail
  - programVariable
```
private final ProgramVariable programVariable
```
    The ProgramVariable or null if an array index is used instead.
  - arrayIndex
```
private final Term arrayIndex
```
    The array index or null if not used.
  - arrayStartIndex
```
private final Term arrayStartIndex
```
    The array start index or null if not used.
  - arrayEndIndex
```
private final Term arrayEndIndex
```
    The array end index or null if not used.
  - parent
```
private final Term parent
```
    An optional parent object or null if it is a value/association of the state.
  - value
```
private final Term value
```
    The value or association target.
  - stateMember
```
private final boolean stateMember
```
    Defines if this location should explicitly be shown on the state.
  - condition
```
private final Term condition
```
    An optional condition under which the value is valid.
  - goalNode
```
private final Node goalNode
```
    The Node on which this result is based on.
- Constructor Detail
  - ExecutionVariableValuePair
```
public ExecutionVariableValuePair(ProgramVariable programVariable,
                                  Term parent,
                                  Term value,
                                  Term condition,
                                  boolean stateMember,
                                  Node goalNode)
```
    Constructor.
    
    Parameters:
    
    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.
  - ExecutionVariableValuePair
```
public ExecutionVariableValuePair(Term arrayIndex,
                                  Term parent,
                                  Term value,
                                  Term condition,
                                  boolean stateMember,
                                  Node goalNode)
```
    Constructor.
    
    Parameters:
    
    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.
  - ExecutionVariableValuePair
```
public ExecutionVariableValuePair(Term arrayStartIndex,
                                  Term arrayEndIndex,
                                  Term arrayRangeConstant,
                                  Term parent,
                                  Term value,
                                  Term condition,
                                  boolean stateMember,
                                  Node goalNode)
```
    Constructor.
    
    Parameters:
    
    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.
- Method Detail
  - getProgramVariable
```
public ProgramVariable getProgramVariable()
```
    Returns the ProgramVariable or null if an array index is used instead.
    
    Returns:
    
    The ProgramVariable or null if an array index is used instead.
  - getParent
```
public Term getParent()
```
    Returns the optional parent object or null if it is a value/association of the state.
    
    Returns:
    
    The optional parent object or null if it is a value/association of the state.
  - getValue
```
public Term getValue()
```
    Returns the value or association target.
    
    Returns:
    
    The value or association target.
  - isArrayIndex
```
public boolean isArrayIndex()
```
    Checks if an array index is represented.
    
    Returns:
    
    true is array index, false is something else.
  - isArrayRange
```
public boolean isArrayRange()
```
    Checks if an array range is represented.
    
    Returns:
    
    true is array range, false is something else.
  - getArrayIndex
```
public Term getArrayIndex()
```
    Returns the array index.
    
    Returns:
    
    The array index.
  - getArrayStartIndex
```
public Term getArrayStartIndex()
```
    Returns the array start index.
    
    Returns:
    
    The array start index.
  - getArrayEndIndex
```
public Term getArrayEndIndex()
```
    Returns the array end index.
    
    Returns:
    
    The array end index.
  - isStateMember
```
public boolean isStateMember()
```
    Checks if this location should explicitly be shown on the state.
    
    Returns:
    
    Show location on state?
  - getCondition
```
public Term getCondition()
```
    Returns the optional condition under which the value is valid.
    
    Returns:
    
    The optional condition under which the value is valid.
  - getGoalNode
```
public Node getGoalNode()
```
    Returns the Node on which this result is based on.
    
    Returns:
    
    The Node on which this result is based on.
  - equals
```
public boolean equals(java.lang.Object obj)
```
    Overrides:
    
    equals in class java.lang.Object
  - hashCode
```
public int hashCode()
```
    Overrides:
    
    hashCode in class java.lang.Object
  - toString
```
public java.lang.String toString()
```
    Overrides:
    
    toString in class java.lang.Object

Class AbstractUpdateExtractor.ExecutionVariableValuePair

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

programVariable

arrayIndex

arrayStartIndex

arrayEndIndex

parent

value

stateMember

condition

goalNode

Constructor Detail

ExecutionVariableValuePair

ExecutionVariableValuePair

ExecutionVariableValuePair

Method Detail

getProgramVariable

getParent

getValue

isArrayIndex

isArrayRange

getArrayIndex

getArrayStartIndex

getArrayEndIndex

isStateMember

getCondition

getGoalNode

equals

hashCode

toString