AbstractUpdateExtractor.ExtractLocationParameter (KeY API Documentation)

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

Enclosing class:

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

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

Constructor Summary

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

Method Summary

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

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.
  - parentTerm
```
private final Term parentTerm
```
    An optional parent object represented as Term. If it is null an IProgramVariable of the state is represented.
  - parentTermIndexInStatePredicate
```
private int parentTermIndexInStatePredicate
```
    The index of the parent argument in the predicate used in side proof to compute the values.
  - valueTermIndexInStatePredicate
```
private int valueTermIndexInStatePredicate
```
    The index of the value argument in the predicate used in side proof to compute the values.
  - preVariable
```
private final 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. x.next) might refer to different objects in the current state.
  - stateMember
```
private final boolean stateMember
```
    Defines if this location should explicitly be shown on the state.
  - arrayRangeConstant
```
private final Term arrayRangeConstant
```
    The constant used to query an array range.
  - notAValue
```
private final Term notAValue
```
    The constant representing the fact that no value is available.
- Constructor Detail
  - ExtractLocationParameter
```
public ExtractLocationParameter(AbstractUpdateExtractor.ExtractLocationParameter original,
                                Term newParent)
```
    Constructor for cloning purpose.
    
    Parameters:
    
    original - The original AbstractUpdateExtractor.ExtractLocationParameter to clone.
    
    newParent - The new parent Term to be used instead of the original one.
  - ExtractLocationParameter
```
public ExtractLocationParameter(ProgramVariable programVariable,
                                boolean stateMember)
                         throws ProofInputException
```
    Constructor.
    
    Parameters:
    
    programVariable - The ProgramVariable.
    
    stateMember - Defines if this location should explicitly be shown on the state.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - ExtractLocationParameter
```
public ExtractLocationParameter(ProgramVariable programVariable,
                                Term parentTerm)
                         throws ProofInputException
```
    Constructor.
    
    Parameters:
    
    programVariable - The ProgramVariable.
    
    parentTerm - The parent object represented as Term.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - ExtractLocationParameter
```
protected ExtractLocationParameter(ProgramVariable programVariable,
                                   Term parentTerm,
                                   boolean stateMember)
                            throws ProofInputException
```
    Constructor.
    
    Parameters:
    
    programVariable - The ProgramVariable.
    
    parentTerm - The parent object represented as Term.
    
    stateMember - Defines if this location should explicitly be shown on the state.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - ExtractLocationParameter
```
public ExtractLocationParameter(Term arrayIndex,
                                Term parentTerm)
                         throws ProofInputException
```
    Constructor.
    
    Parameters:
    
    arrayIndex - The array index.
    
    parentTerm - The parent object represented as Term.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - ExtractLocationParameter
```
public ExtractLocationParameter(Term arrayStartIndex,
                                Term arrayEndIndex,
                                Term parentTerm)
                         throws ProofInputException
```
    Constructor.
    
    Parameters:
    
    arrayStartIndex - The array start index.
    
    arrayEndIndex - The array end index.
    
    parentTerm - The parent object represented as Term.
    
    Throws:
    
    ProofInputException - Occurred Exception.
- Method Detail
  - createLocationVariable
```
protected LocationVariable createLocationVariable(java.lang.String name,
                                                  Sort sort)
                                           throws ProofInputException
```
    Creates a new LocationVariable with the given name and Sort.
    
    Parameters:
    
    name - The name of the new variable.
    
    sort - The Sort of the new variable.
    
    Returns:
    
    The created LocationVariable.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - isStateMember
```
public boolean isStateMember()
```
    Checks if this location should explicitly be shown on the state.
    
    Returns:
    
    Show location on state?
  - 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.
  - getArrayRangeConstant
```
public Term getArrayRangeConstant()
```
    Returns the constant used to query an array range.
    
    Returns:
    
    The constant used to query an array range.
  - getNotAValue
```
public Term getNotAValue()
```
    Returns the constant representing the fact that no value is available.
    
    Returns:
    
    The constant representing the fact that no value is available.
  - getPreVariable
```
public LocationVariable getPreVariable()
```
    Returns the pre variable.
    
    Returns:
    
    The pre variable.
  - getPreUpdateTarget
```
public Term getPreUpdateTarget()
```
    Returns the right side of the update created by createPreUpdate().
    
    Returns:
    
    The right side of the update created by createPreUpdate().
  - createPreUpdate
```
public 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.
    
    Returns:
    
    The created Term with the pre update.
  - createPreParentTerm
```
public Term createPreParentTerm()
```
    Creates the Term to compute the parent object with help of the pre update.
    
    Returns:
    
    The Term to compute the parent object with help of the pre update.
  - createPreValueTerm
```
public Term createPreValueTerm()
```
    Computes the Term to compute the value with help of the pre update.
    
    Returns:
    
    The Term to compute the value with help of the pre update.
  - 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.
  - getParentTerm
```
public Term getParentTerm()
```
    Returns the optional parent object represented as Term. If it is null an IProgramVariable of the state is represented.
    
    Returns:
    
    The optional parent object represented as Term. If it is null an IProgramVariable of the state is represented.
  - getParentTermIndexInStatePredicate
```
public int getParentTermIndexInStatePredicate()
```
    Returns the index of the parent argument in the predicate used in side proof to compute the values.
    
    Returns:
    
    The index of the parent argument in the predicate used in side proof to compute the values.
  - setParentTermIndexInStatePredicate
```
public void setParentTermIndexInStatePredicate(int selectParentTermIndexInStatePredicate)
```
    Sets the index of the parent argument in the predicate used in side proof to compute the values.
    
    Parameters:
    
    selectParentTermIndexInStatePredicate - The index of the parent argument in the predicate used in side proof to compute the values.
  - getValueTermIndexInStatePredicate
```
public int getValueTermIndexInStatePredicate()
```
    Returns the index of the value argument in the predicate used in side proof to compute the values.
    
    Returns:
    
    The index of the value argument in the predicate used in side proof to compute the values.
  - setValueTermIndexInStatePredicate
```
public void setValueTermIndexInStatePredicate(int selectValueTermIndexInStatePredicate)
```
    Sets the index of the value argument in the predicate used in side proof to compute the values.
    
    Parameters:
    
    selectValueTermIndexInStatePredicate - The index of the value argument in the predicate used in side proof to compute the values.
  - toString
```
public java.lang.String toString()
```
    Overrides:
    
    toString in class java.lang.Object
  - 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

Class AbstractUpdateExtractor.ExtractLocationParameter

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

programVariable

arrayIndex

arrayStartIndex

arrayEndIndex

parentTerm

parentTermIndexInStatePredicate

valueTermIndexInStatePredicate

preVariable

stateMember

arrayRangeConstant

notAValue

Constructor Detail

ExtractLocationParameter

ExtractLocationParameter

ExtractLocationParameter

ExtractLocationParameter

ExtractLocationParameter

ExtractLocationParameter

Method Detail

createLocationVariable

isStateMember

isArrayIndex

isArrayRange

getArrayIndex

getArrayStartIndex

getArrayEndIndex

getArrayRangeConstant

getNotAValue

getPreVariable

getPreUpdateTarget

createPreUpdate

createPreParentTerm

createPreValueTerm

getProgramVariable

getParentTerm

getParentTermIndexInStatePredicate

setParentTermIndexInStatePredicate

getValueTermIndexInStatePredicate

setValueTermIndexInStatePredicate

toString

equals

hashCode