de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.KeYlessValue

java.lang.Object

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionElement

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.KeYlessValue

All Implemented Interfaces:

IExecutionElement, IExecutionValue

Enclosing class:

ExecutionNodeReader

public static class ExecutionNodeReader.KeYlessValue
extends ExecutionNodeReader.AbstractKeYlessExecutionElement
implements IExecutionValue

An implementation of IExecutionValue which is independent from KeY and provides such only children and default attributes.

Author:

Martin Hentschel

Field Summary

Fields

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

Constructors

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.

Method Summary

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

Methods inherited from class de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionElement

getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, 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

variable

private final IExecutionVariable variable

The parent IExecutionVariable if available.

typeString

private final java.lang.String typeString

The type string.

valueString

private final java.lang.String valueString

The value string.

valueUnknown

private final boolean valueUnknown

Is the value unknown?

valueAnObject

private final boolean valueAnObject

Is the value an object?

childVariables

private final java.util.List<IExecutionVariable> childVariables

The child variables.

conditionString

private final java.lang.String conditionString

The condition as String.

constraints

private final java.util.List<IExecutionConstraint> constraints

The related IExecutionConstraints.

Constructor Detail

KeYlessValue

public KeYlessValue(IExecutionVariable variable,
                    java.lang.String typeString,
                    java.lang.String valueString,
                    java.lang.String name,
                    boolean valueUnknown,
                    boolean valueAnObject,
                    java.lang.String conditionString)

Constructor.

Parameters:

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.

Method Detail

addChildVariable

public void addChildVariable(IExecutionVariable variable)

Adds the given child IExecutionVariable.

Parameters:

variable - The child IExecutionVariable to add.

getValueString

public java.lang.String getValueString()
                                throws ProofInputException

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

Specified by:

getValueString in interface IExecutionValue

Returns:

The value of the variable as human readable string representation.

Throws:

ProofInputException

getTypeString

public java.lang.String getTypeString()

Returns the type of the variable as human readable string.

Specified by:

getTypeString in interface IExecutionValue

Returns:

The type of the variable as human readable string.

getConditionString

public java.lang.String getConditionString()
                                    throws ProofInputException

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

Specified by:

getConditionString in interface IExecutionValue

Returns:

The condition as human readable String.

Throws:

ProofInputException - Occurred Exception.

getVariable

public IExecutionVariable getVariable()

Returns the parent IExecutionVariable.

Specified by:

getVariable in interface IExecutionValue

Returns:

The parent IExecutionVariable.

getChildVariables

public IExecutionVariable[] getChildVariables()
                                       throws ProofInputException

Returns contained child variables which forms complex data types.

Specified by:

getChildVariables in interface IExecutionValue

Returns:

The contained child variables.

Throws:

ProofInputException

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.

Specified by:

isValueUnknown in interface IExecutionValue

Returns:

true value is unknown, false value is known.

Throws:

ProofInputException

isValueAnObject

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.

Specified by:

isValueAnObject in interface IExecutionValue

Returns:

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

Throws:

ProofInputException - Occurred Exception.

getValue

public Term getValue()
              throws ProofInputException

Returns the value of the variable.

Specified by:

getValue in interface IExecutionValue

Returns:

The value of the variable.

Throws:

ProofInputException

getElementType

public java.lang.String getElementType()

Returns a human readable element type name.

Specified by:

getElementType in interface IExecutionElement

Returns:

The human readable element type.

getCondition

public Term getCondition()
                  throws ProofInputException

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

Specified by:

getCondition in interface IExecutionValue

Returns:

The condition.

Throws:

ProofInputException - Occurred Exception.

addConstraint

public void addConstraint(IExecutionConstraint constraint)

Adds the given IExecutionConstraint.

Parameters:

constraint - The IExecutionConstraint to add.

getConstraints

public IExecutionConstraint[] getConstraints()
                                      throws ProofInputException

Returns all available IExecutionConstraints.

Specified by:

getConstraints in interface IExecutionValue

Returns:

The available IExecutionConstraints.

Throws:

ProofInputException - Occurred Exception.

getModalityPIO

public PosInOccurrence getModalityPIO()

Returns the PosInOccurrence of the modality of interest including updates.

Specified by:

getModalityPIO in interface IExecutionElement

Returns:

The PosInOccurrence of the modality of interest including updates.