de.uka.ilkd.key.symbolic_execution

Class ExecutionVariableExtractor.ExtractedExecutionValue

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.ExecutionVariableExtractor.ExtractedExecutionValue

All Implemented Interfaces:

IExecutionElement, IExecutionValue

Enclosing class:

ExecutionVariableExtractor

public static class ExecutionVariableExtractor.ExtractedExecutionValue
extends AbstractExecutionValue

The IExecutionValue instantiated by the ExecutionVariableExtractor.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.List<ExecutionVariableExtractor.ExtractedExecutionVariable>	childVariables The available child ExecutionVariableExtractor.ExtractedExecutionVariable.
private IExecutionNode<?>	parentNode The IExecutionNode providing the IExecutionConstraints.

Constructor Summary

Constructors

Constructor and Description
ExtractedExecutionValue(IExecutionNode<?> parentNode, Node proofNode, IExecutionVariable variable, Term condition, Term value) Constructor.

Method Summary

Modifier and Type	Method and Description
protected void	addChildVariable(ExecutionVariableExtractor.ExtractedExecutionVariable variable) Adds a child ExecutionVariableExtractor.ExtractedExecutionVariable.
ExecutionVariableExtractor.ExtractedExecutionVariable[]	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.
boolean	isValueUnknown() Checks if the value is unknown.

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

collectRelevantTerms, containsTerm, fillRelevantTerms, getCondition, getConstraints, getElementType, getModalityPIO, getValue, getVariable, 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

childVariables

private final java.util.List<ExecutionVariableExtractor.ExtractedExecutionVariable> childVariables

The available child ExecutionVariableExtractor.ExtractedExecutionVariable.

parentNode

private final IExecutionNode<?> parentNode

The IExecutionNode providing the IExecutionConstraints.

Constructor Detail

ExtractedExecutionValue

public ExtractedExecutionValue(IExecutionNode<?> parentNode,
                               Node proofNode,
                               IExecutionVariable variable,
                               Term condition,
                               Term value)

Constructor.

Parameters:

parentNode - The IExecutionNode providing relevant information.

proofNode - The Node of KeY's proof tree which is represented by this IExecutionNode.

variable - The parent IExecutionVariable which contains this value.

condition - The condition.

value - The value.

Method Detail

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.

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

addChildVariable

protected void addChildVariable(ExecutionVariableExtractor.ExtractedExecutionVariable variable)

Adds a child ExecutionVariableExtractor.ExtractedExecutionVariable.

Parameters:

variable - The ExecutionVariableExtractor.ExtractedExecutionVariable to add.

getChildVariables

public ExecutionVariableExtractor.ExtractedExecutionVariable[] getChildVariables()
                                                                          throws ProofInputException

Returns contained child variables which forms complex data types.

Returns:

The contained child variables.

Throws:

ProofInputException

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.