public class ExecutionValue extends AbstractExecutionValue
IExecutionValue
.Modifier and Type | Field and Description |
---|---|
private IExecutionVariable[] |
childVariables
The child
IExecutionVariable s. |
private java.lang.String |
conditionString
The condition under which the variable has this value as human readable
String . |
private java.lang.String |
typeString
The type of the value.
|
private java.lang.String |
valueString
The value as human readable
String . |
private boolean |
valueUnknown
Is the value unknown?
|
Constructor and Description |
---|
ExecutionValue(Node proofNode,
ExecutionVariable variable,
boolean valueUnknown,
Term value,
java.lang.String valueString,
java.lang.String typeString,
Term condition,
java.lang.String conditionString)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
IExecutionVariable[] |
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.
|
ExecutionVariable |
getVariable()
Returns the parent
IExecutionVariable . |
boolean |
isValueUnknown()
Checks if the value is unknown.
|
protected IExecutionVariable[] |
lazyComputeChildVariables()
Computes the contained child variables lazily when
getChildVariables() is called the first time. |
collectRelevantTerms, containsTerm, fillRelevantTerms, getCondition, getConstraints, getElementType, getModalityPIO, getValue, 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 boolean valueUnknown
private final java.lang.String valueString
String
.private final java.lang.String typeString
private final java.lang.String conditionString
String
.private IExecutionVariable[] childVariables
IExecutionVariable
s.public ExecutionValue(Node proofNode, ExecutionVariable variable, boolean valueUnknown, Term value, java.lang.String valueString, java.lang.String typeString, Term condition, java.lang.String conditionString)
proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.variable
- The parent ExecutionVariable
which contains this value.valueProofNode
- The Node
in the value site proof from which this value was extracted.valueUnknown
- Is the value unknown?value
- The value.valueString
- The value as human readable string.typeString
- The type of the value.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
public IExecutionVariable[] getChildVariables() throws ProofInputException
ProofInputException
protected IExecutionVariable[] lazyComputeChildVariables() throws ProofInputException
getChildVariables()
is called the first time.IExecutionVariable
s.ProofInputException
- Occurred Exception.public java.lang.String getConditionString() throws ProofInputException
IExecutionValue.getVariable()
)
has this value as human readable String
.String
.ProofInputException
- Occurred Exception.public ExecutionVariable getVariable()
IExecutionVariable
.getVariable
in interface IExecutionValue
getVariable
in class AbstractExecutionValue
IExecutionVariable
.protected IExecutionConstraint[] getNodeConstraints()
IExecutionConstraint
s of the IExecutionNode
on which this IExecutionValue
is part of.getNodeConstraints
in class AbstractExecutionValue
IExecutionConstraint
s.