public static class ExecutionNodeReader.KeYlessValue extends ExecutionNodeReader.AbstractKeYlessExecutionElement implements IExecutionValue
IExecutionValue
which is independent
from KeY and provides such only children and default attributes.Modifier and Type | Field and Description |
---|---|
private java.util.List<IExecutionVariable> |
childVariables
The child variables.
|
private java.lang.String |
conditionString
The condition as
String . |
private java.util.List<IExecutionConstraint> |
constraints
The related
IExecutionConstraint s. |
private java.lang.String |
typeString
The type string.
|
private boolean |
valueAnObject
Is the value an object?
|
private java.lang.String |
valueString
The value string.
|
private boolean |
valueUnknown
Is the value unknown?
|
private IExecutionVariable |
variable
The parent
IExecutionVariable if available. |
Constructor and Description |
---|
KeYlessValue(IExecutionVariable variable,
java.lang.String typeString,
java.lang.String valueString,
java.lang.String name,
boolean valueUnknown,
boolean valueAnObject,
java.lang.String conditionString)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addChildVariable(IExecutionVariable variable)
Adds the given child
IExecutionVariable . |
void |
addConstraint(IExecutionConstraint constraint)
Adds the given
IExecutionConstraint . |
IExecutionVariable[] |
getChildVariables()
Returns contained child variables which forms complex data types.
|
Term |
getCondition()
Returns the condition under which the variable (
IExecutionValue.getVariable() )
has this value. |
java.lang.String |
getConditionString()
Returns the condition under which the variable (
IExecutionValue.getVariable() )
has this value as human readable String . |
IExecutionConstraint[] |
getConstraints()
Returns all available
IExecutionConstraint s. |
java.lang.String |
getElementType()
Returns a human readable element type name.
|
PosInOccurrence |
getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
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, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final IExecutionVariable variable
IExecutionVariable
if available.private final java.lang.String typeString
private final java.lang.String valueString
private final boolean valueUnknown
private final boolean valueAnObject
private final java.util.List<IExecutionVariable> childVariables
private final java.lang.String conditionString
String
.private final java.util.List<IExecutionConstraint> constraints
IExecutionConstraint
s.public KeYlessValue(IExecutionVariable variable, java.lang.String typeString, java.lang.String valueString, java.lang.String name, boolean valueUnknown, boolean valueAnObject, java.lang.String conditionString)
variable
- The parent IExecutionVariable
.typeString
- The type string.valueString
- The value string.name
- The name.valueUnknown
- Is the value unknown?valueAnObject
- Is the value an object?conditionString
- The condition as human readable String
.public void addChildVariable(IExecutionVariable variable)
IExecutionVariable
.variable
- The child IExecutionVariable
to add.public java.lang.String getValueString() throws ProofInputException
getValueString
in interface IExecutionValue
ProofInputException
public java.lang.String getTypeString()
getTypeString
in interface IExecutionValue
public java.lang.String getConditionString() throws ProofInputException
IExecutionValue.getVariable()
)
has this value as human readable String
.getConditionString
in interface IExecutionValue
String
.ProofInputException
- Occurred Exception.public IExecutionVariable getVariable()
IExecutionVariable
.getVariable
in interface IExecutionValue
IExecutionVariable
.public IExecutionVariable[] getChildVariables() throws ProofInputException
getChildVariables
in interface IExecutionValue
ProofInputException
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.
isValueUnknown
in interface IExecutionValue
true
value is unknown, false
value is known.ProofInputException
public 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.
isValueAnObject
in interface IExecutionValue
true
is an object, false
is an attribute of the object defined by the parent IExecutionValue
.ProofInputException
- Occurred Exception.public Term getValue() throws ProofInputException
getValue
in interface IExecutionValue
ProofInputException
public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public Term getCondition() throws ProofInputException
IExecutionValue.getVariable()
)
has this value.getCondition
in interface IExecutionValue
ProofInputException
- Occurred Exception.public void addConstraint(IExecutionConstraint constraint)
IExecutionConstraint
.constraint
- The IExecutionConstraint
to add.public IExecutionConstraint[] getConstraints() throws ProofInputException
IExecutionConstraint
s.getConstraints
in interface IExecutionValue
IExecutionConstraint
s.ProofInputException
- Occurred Exception.public PosInOccurrence getModalityPIO()
PosInOccurrence
of the modality of interest including updates.getModalityPIO
in interface IExecutionElement
PosInOccurrence
of the modality of interest including updates.