de.uka.ilkd.key.symbolic_execution.model

Interface IExecutionVariable

All Superinterfaces:

IExecutionElement

All Known Implementing Classes:

AbstractExecutionVariable, ExecutionAllArrayIndicesVariable, ExecutionNodeReader.KeYlessVariable, ExecutionVariable, ExecutionVariableExtractor.ExtractedExecutionVariable, ExecutionVariableExtractor.StateExecutionVariable

public interface IExecutionVariable
extends IExecutionElement

A variable value pair contained in an IExecutionNode, e.g. the method parameter int x = 42; will have the variable value pair x = 42. This class represents the variable (x) which is represented while its values are represented as child IExecutionValue instances.

The default implementation is ExecutionVariable which is instantiated lazily by the IExecutionNode implementations.

Author:

Martin Hentschel

See Also:

IExecutionNode, IExecutionValue, ExecutionVariable

Method Summary

Modifier and Type	Method and Description
Term	createSelectTerm() Creates recursive a term which can be used to determine the value of getProgramVariable().
Term	getAdditionalCondition() Returns the optional additional condition considered during value computation.
Term	getArrayIndex() Returns the index in the parent array if an array cell value is represented.
java.lang.String	getArrayIndexString() Returns the human readable index in the parent array if an array cell value is represented.
IExecutionValue	getParentValue() Returns the parent IExecutionValue if available.
IProgramVariable	getProgramVariable() Returns the IProgramVariable which contains the represented value.
IExecutionValue[]	getValues() Returns the possible values of this IExecutionVariable.
boolean	isArrayIndex() Checks if the current value is part of a parent array.

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionElement

getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Method Detail

getProgramVariable

IProgramVariable getProgramVariable()

Returns the IProgramVariable which contains the represented value.

Returns:

The IProgramVariable which contains the represented value.

getArrayIndex

Term getArrayIndex()

Returns the index in the parent array if an array cell value is represented.

Returns:

The index in the parent array or null if no array cell value is represented.

getArrayIndexString

java.lang.String getArrayIndexString()

Returns the human readable index in the parent array if an array cell value is represented.

Returns:

The human readable index in the parent array or null if no array cell value is represented.

isArrayIndex

boolean isArrayIndex()

Checks if the current value is part of a parent array.

Returns:

true is array cell value, false is a "normal" value.

getAdditionalCondition

Term getAdditionalCondition()

Returns the optional additional condition considered during value computation.

Returns:

The optional additional condition considered during value computation.

getParentValue

IExecutionValue getParentValue()

Returns the parent IExecutionValue if available.

Returns:

The parent IExecutionValue if available and null otherwise.

getValues

IExecutionValue[] getValues()
                     throws ProofInputException

Returns the possible values of this IExecutionVariable.

Returns:

The possible values of this IExecutionVariable.

Throws:

ProofInputException

createSelectTerm

Term createSelectTerm()

Creates recursive a term which can be used to determine the value of getProgramVariable().

Returns:

The created term.