Package | Description |
---|---|
de.uka.ilkd.key.symbolic_execution.model.impl |
Modifier and Type | Method and Description |
---|---|
ExecutionValue |
ExecutionVariable.getLengthValue()
Returns the
ExecutionValue from which the array length was computed. |
ExecutionValue |
ExecutionVariable.getParentValue()
Returns the parent
IExecutionValue if available. |
ExecutionValue[] |
ExecutionVariable.getValues()
Returns the possible values of this
IExecutionVariable . |
protected ExecutionValue[] |
ExecutionVariable.instantiateValuesFromSideProof(InitConfig initConfig,
Services services,
TermBuilder tb,
ApplyStrategyInfo info,
Operator resultOperator,
Term siteProofSelectTerm,
Term siteProofCondition)
Analyzes the side proof defined by the
ApplyStrategyInfo
and creates ExecutionValue s from it. |
protected ExecutionValue[] |
ExecutionAllArrayIndicesVariable.lazyComputeValues()
Computes the value for
ExecutionVariable.getValues()
lazily when the method is called the first time. |
protected ExecutionValue[] |
ExecutionVariable.lazyComputeValues()
Computes the value for
ExecutionVariable.getValues()
lazily when the method is called the first time. |
Constructor and Description |
---|
ExecutionAllArrayIndicesVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
IProgramVariable arrayProgramVariable,
Term additionalCondition)
Constructor.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
IProgramVariable programVariable,
Term additionalCondition)
Constructor for a "normal" child value.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
Term arrayIndex,
ExecutionValue lengthValue,
Term additionalCondition)
Constructor for an array cell value.
|
Copyright © 2003-2019 The KeY-Project.