de.uka.ilkd.key.symbolic_execution

Class ExecutionVariableExtractor.StateExecutionVariable

java.lang.Object

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

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

de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.StateExecutionVariable

All Implemented Interfaces:

IExecutionElement, IExecutionVariable

Enclosing class:

ExecutionVariableExtractor

private class ExecutionVariableExtractor.StateExecutionVariable
extends AbstractExecutionVariable

The IExecutionVariable instantiated by the ExecutionVariableExtractor.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private IExecutionValue[]	values The contained IExecutionValues.

Constructor Summary

Constructors

Constructor and Description
StateExecutionVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, IProgramVariable programVariable, Term arrayIndex, Term additionalCondition) Constructor.

Method Summary

Modifier and Type	Method and Description
Term	createSelectTerm() Creates recursive a term which can be used to determine the value of IExecutionVariable.getProgramVariable().
IExecutionValue[]	getValues() Returns the possible values of this IExecutionVariable.

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

getAdditionalCondition, getArrayIndex, getArrayIndexString, getElementType, getModalityPIO, getParentValue, getProgramVariable, isArrayIndex, 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

values

private IExecutionValue[] values

The contained IExecutionValues.

Constructor Detail

StateExecutionVariable

public StateExecutionVariable(IExecutionNode<?> parentNode,
                              Node proofNode,
                              PosInOccurrence modalityPIO,
                              IProgramVariable programVariable,
                              Term arrayIndex,
                              Term additionalCondition)

Constructor.

Parameters:

parentNode - The IExecutionNode providing relevant information.

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

modalityPIO - The PosInOccurrence of the modality of interest.

programVariable - The represented IProgramVariable which value is shown.

arrayIndex - The index in the parent array.

additionalCondition - An optional additional condition to consider.

Method Detail

getValues

public IExecutionValue[] getValues()
                            throws ProofInputException

Returns the possible values of this IExecutionVariable.

Returns:

The possible values of this IExecutionVariable.

Throws:

ProofInputException

createSelectTerm

public Term createSelectTerm()

Creates recursive a term which can be used to determine the value of IExecutionVariable.getProgramVariable().

Returns:

The created term.