de.uka.ilkd.key.symbolic_execution.model

Interface IExecutionValue

All Superinterfaces:

IExecutionElement

All Known Implementing Classes:

AbstractExecutionValue, ExecutionNodeReader.KeYlessValue, ExecutionValue, ExecutionVariableExtractor.ExtractedExecutionValue

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.

Author:

Martin Hentschel

See Also:

IExecutionVariable, ExecutionValue

Method Summary

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 IExecutionConstraints.
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.

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionElement

getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Method Detail

getCondition

Term getCondition()
           throws ProofInputException

Returns the condition under which the variable (getVariable()) has this value.

Returns:

The condition.

Throws:

ProofInputException - Occurred Exception.

getConditionString

java.lang.String getConditionString()
                             throws ProofInputException

Returns the condition under which the variable (getVariable()) has this value as human readable String.

Returns:

The condition as human readable String.

Throws:

ProofInputException - Occurred Exception.

isValueUnknown

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.

Returns:

true value is unknown, false value is known.

Throws:

ProofInputException

getValue

Term getValue()
       throws ProofInputException

Returns the value of the variable.

Returns:

The value of the variable.

Throws:

ProofInputException

getValueString

java.lang.String getValueString()
                         throws ProofInputException

Returns the value of the variable as human readable string representation.

Returns:

The value of the variable as human readable string representation.

Throws:

ProofInputException

isValueAnObject

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.

Returns:

true is an object, false is an attribute of the object defined by the parent IExecutionValue.

Throws:

ProofInputException - Occurred Exception.

getTypeString

java.lang.String getTypeString()
                        throws ProofInputException

Returns the type of the variable as human readable string.

Returns:

The type of the variable as human readable string.

Throws:

ProofInputException

getVariable

IExecutionVariable getVariable()

Returns the parent IExecutionVariable.

Returns:

The parent IExecutionVariable.

getChildVariables

IExecutionVariable[] getChildVariables()
                                throws ProofInputException

Returns contained child variables which forms complex data types.

Returns:

The contained child variables.

Throws:

ProofInputException

getConstraints

IExecutionConstraint[] getConstraints()
                               throws ProofInputException

Returns all available IExecutionConstraints.

Returns:

The available IExecutionConstraints.

Throws:

ProofInputException - Occurred Exception.