de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.KeYlessMethodReturnValue

java.lang.Object

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

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.KeYlessMethodReturnValue

All Implemented Interfaces:

IExecutionElement, IExecutionMethodReturnValue

Enclosing class:

ExecutionNodeReader

public static class ExecutionNodeReader.KeYlessMethodReturnValue
extends ExecutionNodeReader.AbstractKeYlessExecutionElement
implements IExecutionMethodReturnValue

An implementation of IExecutionMethodReturn 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.lang.String	conditionString The optional human readable condition.
private boolean	hasCondition Is a condition available?
private java.lang.String	returnValueString The human readable return value.

Constructor Summary

Constructors

Constructor and Description
KeYlessMethodReturnValue(java.lang.String name, java.lang.String returnValueString, boolean hasCondition, java.lang.String conditionString) Constructor.

Method Summary

Modifier and Type	Method and Description
Term	getCondition() Returns the optional condition under which the return value is valid.
java.lang.String	getConditionString() Returns the optional condition under which the return value is valid as human readable String.
java.lang.String	getElementType() Returns a human readable element type name.
PosInOccurrence	getModalityPIO() Returns the PosInOccurrence of the modality of interest including updates.
Term	getReturnValue() Returns the return value.
java.lang.String	getReturnValueString() Returns the return value as human readable String.
boolean	hasCondition() Checks if a condition is available via IExecutionMethodReturnValue.getCondition() under which this return value is returned.

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

returnValueString

private final java.lang.String returnValueString

The human readable return value.

hasCondition

private final boolean hasCondition

Is a condition available?

conditionString

private final java.lang.String conditionString

The optional human readable condition.

Constructor Detail

KeYlessMethodReturnValue

public KeYlessMethodReturnValue(java.lang.String name,
                                java.lang.String returnValueString,
                                boolean hasCondition,
                                java.lang.String conditionString)

Constructor.

Parameters:

name - The name of this node.

returnValueString - The human readable return value.

hasCondition - Is a condition available?

conditionString - The optional human readable condition.

Method Detail

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.

getReturnValue

public Term getReturnValue()
                    throws ProofInputException

Returns the return value.

Specified by:

getReturnValue in interface IExecutionMethodReturnValue

Returns:

The return value.

Throws:

ProofInputException - Occurred Exception.

getReturnValueString

public java.lang.String getReturnValueString()
                                      throws ProofInputException

Returns the return value as human readable String.

Specified by:

getReturnValueString in interface IExecutionMethodReturnValue

Returns:

The return value as human readable String.

Throws:

ProofInputException - Occurred Exception.

hasCondition

public boolean hasCondition()
                     throws ProofInputException

Checks if a condition is available via IExecutionMethodReturnValue.getCondition() under which this return value is returned.

Specified by:

hasCondition in interface IExecutionMethodReturnValue

Returns:

true condition is available, false condition is not available.

Throws:

ProofInputException

getCondition

public Term getCondition()
                  throws ProofInputException

Returns the optional condition under which the return value is valid.

Specified by:

getCondition in interface IExecutionMethodReturnValue

Returns:

The optional condition under which the return value is valid.

Throws:

ProofInputException - Occurred Exception.

getConditionString

public java.lang.String getConditionString()
                                    throws ProofInputException

Returns the optional condition under which the return value is valid as human readable String.

Specified by:

getConditionString in interface IExecutionMethodReturnValue

Returns:

The optional condition as human readable String.

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.