de.uka.ilkd.key.symbolic_execution

Class ExecutionVariableExtractor.ExtractedExecutionVariable

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

All Implemented Interfaces:

IExecutionElement, IExecutionVariable

Enclosing class:

ExecutionVariableExtractor

public static class ExecutionVariableExtractor.ExtractedExecutionVariable
extends AbstractExecutionVariable

The IExecutionVariable instantiated by the ExecutionVariableExtractor.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private Term	arrayEndIndex The array end index or null if not used.
private Term	arrayStartIndex The array start index or null if not used.
private java.util.List<IExecutionValue>	values The contained IExecutionValues.

Constructor Summary

Constructors

Constructor and Description
ExtractedExecutionVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, IProgramVariable programVariable, Term arrayIndex, Term arrayStartIndex, Term arrayEndIndex, Term additionalCondition, ExecutionVariableExtractor.ExtractedExecutionValue parentValue) 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().
Term	getArrayEndIndex() Returns the array end index.
java.lang.String	getArrayEndIndexString() Returns the human readable array end index.
Term	getArrayStartIndex() Returns the array start index.
java.lang.String	getArrayStartIndexString() Returns the human readable array start index.
IExecutionValue[]	getValues() Returns the possible values of this IExecutionVariable.
protected java.lang.String	lazyComputeName() Computes the name of this node lazily when AbstractExecutionElement.getName() is called the first time.
private void	setValues(java.util.List<IExecutionValue> values) Sets the IExecutionValues.

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

getAdditionalCondition, getArrayIndex, getArrayIndexString, getElementType, getModalityPIO, getParentValue, getProgramVariable, isArrayIndex

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 java.util.List<IExecutionValue> values

The contained IExecutionValues.

arrayStartIndex

private final Term arrayStartIndex

The array start index or null if not used.

arrayEndIndex

private final Term arrayEndIndex

The array end index or null if not used.

Constructor Detail

ExtractedExecutionVariable

public ExtractedExecutionVariable(IExecutionNode<?> parentNode,
                                  Node proofNode,
                                  PosInOccurrence modalityPIO,
                                  IProgramVariable programVariable,
                                  Term arrayIndex,
                                  Term arrayStartIndex,
                                  Term arrayEndIndex,
                                  Term additionalCondition,
                                  ExecutionVariableExtractor.ExtractedExecutionValue parentValue)

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.

parentValue - The parent IExecutionValue or null if not available.

Method Detail

setValues

private void setValues(java.util.List<IExecutionValue> values)

Sets the IExecutionValues.

Parameters:

values - The IExecutionValues to set.

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.

getArrayStartIndex

public Term getArrayStartIndex()

Returns the array start index.

Returns:

The array start index.

getArrayStartIndexString

public java.lang.String getArrayStartIndexString()

Returns the human readable array start index.

Returns:

The human readable array start index.

getArrayEndIndex

public Term getArrayEndIndex()

Returns the array end index.

Returns:

The array end index.

getArrayEndIndexString

public java.lang.String getArrayEndIndexString()

Returns the human readable array end index.

Returns:

The human readable array end index.

lazyComputeName

protected java.lang.String lazyComputeName()
                                    throws ProofInputException

Computes the name of this node lazily when AbstractExecutionElement.getName() is called the first time.

Overrides:

lazyComputeName in class AbstractExecutionVariable

Returns:

The human readable name of this IExecutionNode.

Throws:

ProofInputException