public static class ExecutionVariableExtractor.ExtractedExecutionValue extends AbstractExecutionValue
IExecutionValue
instantiated by the ExecutionVariableExtractor
.Modifier and Type | Field and Description |
---|---|
private java.util.List<ExecutionVariableExtractor.ExtractedExecutionVariable> |
childVariables
The available child
ExecutionVariableExtractor.ExtractedExecutionVariable . |
private IExecutionNode<?> |
parentNode
The
IExecutionNode providing the IExecutionConstraint s. |
Constructor and Description |
---|
ExtractedExecutionValue(IExecutionNode<?> parentNode,
Node proofNode,
IExecutionVariable variable,
Term condition,
Term value)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected void |
addChildVariable(ExecutionVariableExtractor.ExtractedExecutionVariable variable)
Adds a child
ExecutionVariableExtractor.ExtractedExecutionVariable . |
ExecutionVariableExtractor.ExtractedExecutionVariable[] |
getChildVariables()
Returns contained child variables which forms complex data types.
|
java.lang.String |
getConditionString()
Returns the condition under which the variable (
IExecutionValue.getVariable() )
has this value as human readable String . |
protected IExecutionConstraint[] |
getNodeConstraints()
Returns all available
IExecutionConstraint s of the IExecutionNode on which this IExecutionValue is part of. |
java.lang.String |
getTypeString()
Returns the type of the variable as human readable string.
|
java.lang.String |
getValueString()
Returns the value of the variable as human readable string representation.
|
boolean |
isValueUnknown()
Checks if the value is unknown.
|
collectRelevantTerms, containsTerm, fillRelevantTerms, getCondition, getConstraints, getElementType, getModalityPIO, getValue, getVariable, isValueAnObject, lazyComputeConstraints, lazyComputeName
formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final java.util.List<ExecutionVariableExtractor.ExtractedExecutionVariable> childVariables
ExecutionVariableExtractor.ExtractedExecutionVariable
.private final IExecutionNode<?> parentNode
IExecutionNode
providing the IExecutionConstraint
s.public ExtractedExecutionValue(IExecutionNode<?> parentNode, Node proofNode, IExecutionVariable variable, Term condition, Term value)
parentNode
- The IExecutionNode
providing relevant information.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.variable
- The parent IExecutionVariable
which contains this value.condition
- The condition.value
- The value.public java.lang.String getConditionString() throws ProofInputException
IExecutionValue.getVariable()
)
has this value as human readable String
.String
.ProofInputException
- Occurred Exception.public boolean isValueUnknown() throws ProofInputException
Checks if the value is unknown.
Imagine the following class:
public class A {
private A next;
public int main() {
return 42; // breakpoint
}
}
If the main method is debugged symbolically and stopped at the statement
marked with the comment // breakpoint
the field self.next
has the symbolic value SVself.next
. And its field
self.next.next
has again a symbolic value SVself.next.next
.
This chain is infinite deep. But on the other side the Sequent contains
no information about self.next
so the symbolic value can be
null
or a concrete object. Such symbolic values which are not
founded in the Sequent are treated in the symbolic execution API as
"unknown" to avoid infinite deep value hierarchies if they are not cyclic.
true
value is unknown, false
value is known.ProofInputException
public java.lang.String getValueString() throws ProofInputException
ProofInputException
public java.lang.String getTypeString() throws ProofInputException
ProofInputException
protected void addChildVariable(ExecutionVariableExtractor.ExtractedExecutionVariable variable)
ExecutionVariableExtractor.ExtractedExecutionVariable
.variable
- The ExecutionVariableExtractor.ExtractedExecutionVariable
to add.public ExecutionVariableExtractor.ExtractedExecutionVariable[] getChildVariables() throws ProofInputException
ProofInputException
protected IExecutionConstraint[] getNodeConstraints()
IExecutionConstraint
s of the IExecutionNode
on which this IExecutionValue
is part of.getNodeConstraints
in class AbstractExecutionValue
IExecutionConstraint
s.