public interface IExecutionValue extends IExecutionElement
A value of an IExecutionVariable
, e.g.
the method parameter int x = 42;
will have the variable value pair
x = 42
. This class represents the value (42
).
The default implementation is ExecutionValue
which
is instantiated lazily by the IExecutionVariable
implementation.
IExecutionVariable
,
ExecutionValue
Modifier and Type | Method and Description |
---|---|
IExecutionVariable[] |
getChildVariables()
Returns contained child variables which forms complex data types.
|
Term |
getCondition()
Returns the condition under which the variable (
getVariable() )
has this value. |
java.lang.String |
getConditionString()
Returns the condition under which the variable (
getVariable() )
has this value as human readable String . |
IExecutionConstraint[] |
getConstraints()
Returns all available
IExecutionConstraint s. |
java.lang.String |
getTypeString()
Returns the type of the variable as human readable string.
|
Term |
getValue()
Returns the value of the variable.
|
java.lang.String |
getValueString()
Returns the value of the variable as human readable string representation.
|
IExecutionVariable |
getVariable()
Returns the parent
IExecutionVariable . |
boolean |
isValueAnObject()
Checks if the value represents an object or an attribute of the object
defined by the parent
IExecutionValue . |
boolean |
isValueUnknown()
Checks if the value is unknown.
|
getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
Term getCondition() throws ProofInputException
getVariable()
)
has this value.ProofInputException
- Occurred Exception.java.lang.String getConditionString() throws ProofInputException
getVariable()
)
has this value as human readable String
.String
.ProofInputException
- Occurred Exception.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
Term getValue() throws ProofInputException
ProofInputException
java.lang.String getValueString() throws ProofInputException
ProofInputException
boolean isValueAnObject() throws ProofInputException
Checks if the value represents an object or an attribute of the object
defined by the parent IExecutionValue
.
All values which are not a basic datatype (integer, boolean, ...) and not an instance of a library class will be treated as object.
true
is an object, false
is an attribute of the object defined by the parent IExecutionValue
.ProofInputException
- Occurred Exception.java.lang.String getTypeString() throws ProofInputException
ProofInputException
IExecutionVariable getVariable()
IExecutionVariable
.IExecutionVariable
.IExecutionVariable[] getChildVariables() throws ProofInputException
ProofInputException
IExecutionConstraint[] getConstraints() throws ProofInputException
IExecutionConstraint
s.IExecutionConstraint
s.ProofInputException
- Occurred Exception.