de.uka.ilkd.key.symbolic_execution.model.impl

Class ExecutionValue

java.lang.Object

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionValue

de.uka.ilkd.key.symbolic_execution.model.impl.ExecutionValue

All Implemented Interfaces:

IExecutionElement, IExecutionValue

public class ExecutionValue
extends AbstractExecutionValue

The default implementation of IExecutionValue.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private IExecutionVariable[]	childVariables The child IExecutionVariables.
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 Summary

Constructors

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.

Method Summary

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

Methods inherited from class de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionValue

collectRelevantTerms, containsTerm, fillRelevantTerms, getCondition, getConstraints, getElementType, getModalityPIO, getValue, isValueAnObject, lazyComputeConstraints, lazyComputeName

Methods inherited from class de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement

formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

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

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

Field Detail

valueUnknown

private final boolean valueUnknown

Is the value unknown?

valueString

private final java.lang.String valueString

The value as human readable String.

typeString

private final java.lang.String typeString

The type of the value.

conditionString

private final java.lang.String conditionString

The condition under which the variable has this value as human readable String.

childVariables

private IExecutionVariable[] childVariables

The child IExecutionVariables.

Constructor Detail

ExecutionValue

public ExecutionValue(Node proofNode,
                      ExecutionVariable variable,
                      boolean valueUnknown,
                      Term value,
                      java.lang.String valueString,
                      java.lang.String typeString,
                      Term condition,
                      java.lang.String conditionString)

Constructor.

Parameters:

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.

Method Detail

isValueUnknown

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.

Returns:

true value is unknown, false value is known.

Throws:

ProofInputException

getValueString

public 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

getTypeString

public 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

getChildVariables

public IExecutionVariable[] getChildVariables()
                                       throws ProofInputException

Returns contained child variables which forms complex data types.

Returns:

The contained child variables.

Throws:

ProofInputException

lazyComputeChildVariables

protected IExecutionVariable[] lazyComputeChildVariables()
                                                  throws ProofInputException

Computes the contained child variables lazily when getChildVariables() is called the first time.

Returns:

The contained child IExecutionVariables.

Throws:

ProofInputException - Occurred Exception.

getConditionString

public java.lang.String getConditionString()
                                    throws ProofInputException

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

Returns:

The condition as human readable String.

Throws:

ProofInputException - Occurred Exception.

getVariable

public ExecutionVariable getVariable()

Returns the parent IExecutionVariable.

Specified by:

getVariable in interface IExecutionValue

Overrides:

getVariable in class AbstractExecutionValue

Returns:

The parent IExecutionVariable.

getNodeConstraints

protected IExecutionConstraint[] getNodeConstraints()

Returns all available IExecutionConstraints of the IExecutionNode on which this IExecutionValue is part of.

Specified by:

getNodeConstraints in class AbstractExecutionValue

Returns:

All available IExecutionConstraints.