de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.KeYlessVariable

java.lang.Object

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

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.KeYlessVariable

All Implemented Interfaces:

IExecutionElement, IExecutionVariable

Enclosing class:

ExecutionNodeReader

public static class ExecutionNodeReader.KeYlessVariable
extends ExecutionNodeReader.AbstractKeYlessExecutionElement
implements IExecutionVariable

An implementation of IExecutionVariable 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	arrayIndexString The array index.
private boolean	isArrayIndex The is array flag.
private IExecutionValue	parentValue The parent IExecutionValue if available.
private java.util.List<IExecutionValue>	values The contained values.

Constructor Summary

Constructors

Constructor and Description
KeYlessVariable(IExecutionValue parentValue, boolean isArrayIndex, java.lang.String arrayIndexString, java.lang.String name) Constructor.

Method Summary

Modifier and Type	Method and Description
void	addValue(IExecutionValue variable) Adds the given child IExecutionValue.
Term	createSelectTerm() Creates recursive a term which can be used to determine the value of IExecutionVariable.getProgramVariable().
Term	getAdditionalCondition() Returns the optional additional condition considered during value computation.
Term	getArrayIndex() Returns the index in the parent array if an array cell value is represented.
java.lang.String	getArrayIndexString() Returns the human readable index in the parent array if an array cell value is represented.
java.lang.String	getElementType() Returns a human readable element type name.
PosInOccurrence	getModalityPIO() Returns the PosInOccurrence of the modality of interest including updates.
IExecutionValue	getParentValue() Returns the parent IExecutionValue if available.
IProgramVariable	getProgramVariable() Returns the IProgramVariable which contains the represented value.
IExecutionValue[]	getValues() Returns the possible values of this IExecutionVariable.
boolean	isArrayIndex() Checks if the current value is part of a parent array.

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

parentValue

private final IExecutionValue parentValue

The parent IExecutionValue if available.

isArrayIndex

private final boolean isArrayIndex

The is array flag.

arrayIndexString

private final java.lang.String arrayIndexString

The array index.

values

private final java.util.List<IExecutionValue> values

The contained values.

Constructor Detail

KeYlessVariable

public KeYlessVariable(IExecutionValue parentValue,
                       boolean isArrayIndex,
                       java.lang.String arrayIndexString,
                       java.lang.String name)

Constructor.

Parameters:

parentVariable - The parent IExecutionValue if available.

isArrayIndex - The is array flag.

arrayIndexString - The array index.

name - The name.

Method Detail

addValue

public void addValue(IExecutionValue variable)

Adds the given child IExecutionValue.

Parameters:

variable - The child IExecutionValue to add.

getParentValue

public IExecutionValue getParentValue()

Returns the parent IExecutionValue if available.

Specified by:

getParentValue in interface IExecutionVariable

Returns:

The parent IExecutionValue if available and null otherwise.

getValues

public IExecutionValue[] getValues()

Returns the possible values of this IExecutionVariable.

Specified by:

getValues in interface IExecutionVariable

Returns:

The possible values of this IExecutionVariable.

getArrayIndex

public Term getArrayIndex()

Returns the index in the parent array if an array cell value is represented.

Specified by:

getArrayIndex in interface IExecutionVariable

Returns:

The index in the parent array or null if no array cell value is represented.

getArrayIndexString

public java.lang.String getArrayIndexString()

Returns the human readable index in the parent array if an array cell value is represented.

Specified by:

getArrayIndexString in interface IExecutionVariable

Returns:

The human readable index in the parent array or null if no array cell value is represented.

isArrayIndex

public boolean isArrayIndex()

Checks if the current value is part of a parent array.

Specified by:

isArrayIndex in interface IExecutionVariable

Returns:

true is array cell value, false is a "normal" value.

getProgramVariable

public IProgramVariable getProgramVariable()

Returns the IProgramVariable which contains the represented value.

Specified by:

getProgramVariable in interface IExecutionVariable

Returns:

The IProgramVariable which contains the represented value.

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.

getAdditionalCondition

public Term getAdditionalCondition()

Returns the optional additional condition considered during value computation.

Specified by:

getAdditionalCondition in interface IExecutionVariable

Returns:

The optional additional condition considered during value computation.

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.

createSelectTerm

public Term createSelectTerm()

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

Specified by:

createSelectTerm in interface IExecutionVariable

Returns:

The created term.