de.uka.ilkd.key.symbolic_execution.object_model

Interface ISymbolicAssociationValueContainer

All Superinterfaces:

ISymbolicElement

All Known Subinterfaces:

ISymbolicObject, ISymbolicState

All Known Implementing Classes:

AbstractSymbolicAssociationValueContainer, SymbolicLayoutReader.AbstractKeYlessAssociationValueContainer, SymbolicLayoutReader.KeYlessObject, SymbolicLayoutReader.KeYlessState, SymbolicObject, SymbolicState

public interface ISymbolicAssociationValueContainer
extends ISymbolicElement

This interface is not instantiated directly because it defines only the common behavior of ISymbolicState and ISymbolicObject which is to contain associations (references to other ISymbolicObjects) and values (local variables of simple types).

The default abstract implementation is AbstractSymbolicAssociationValueContainer.

Author:

Martin Hentschel

See Also:

AbstractSymbolicAssociationValueContainer, ISymbolicObject, ISymbolicState

Method Summary

Modifier and Type	Method and Description
ISymbolicAssociation	getAssociation(IProgramVariable programVariable, boolean isArrayIndex, Term arrayIndex, Term condition) Returns the ISymbolicAssociation with the given IProgramVariable.
ImmutableList<ISymbolicAssociation>	getAssociations() Returns the contained associations.
ISymbolicValue	getValue(IProgramVariable programVariable, boolean isArrayIndex, Term arrayIndex, Term condition) Returns the ISymbolicValue with the given IProgramVariable.
ImmutableList<ISymbolicValue>	getValues() Returns the contained values.

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicElement

getSettings

Method Detail

getAssociations

ImmutableList<ISymbolicAssociation> getAssociations()

Returns the contained associations.

Returns:

The contained associations.

getAssociation

ISymbolicAssociation getAssociation(IProgramVariable programVariable,
                                    boolean isArrayIndex,
                                    Term arrayIndex,
                                    Term condition)

Returns the ISymbolicAssociation with the given IProgramVariable.

Parameters:

programVariable - The IProgramVariable for which the ISymbolicAssociation is requested.

isArrayIndex - Is array index?

arrayIndex - The array index.

condition - The optional condition under which this association is valid.

Returns:

The found ISymbolicAssociation or null if no ISymbolicAssociation is available with the given IProgramVariable.

getValues

ImmutableList<ISymbolicValue> getValues()

Returns the contained values.

Returns:

The contained values.

getValue

ISymbolicValue getValue(IProgramVariable programVariable,
                        boolean isArrayIndex,
                        Term arrayIndex,
                        Term condition)

Returns the ISymbolicValue with the given IProgramVariable.

Parameters:

programVariable - The IProgramVariable for which the ISymbolicValue is requested.

isArrayIndex - Is array index?

arrayIndex - The array index.

condition - The optional condition under which this value is valid.

Returns:

The found ISymbolicValue or null if no ISymbolicValue is available with the given IProgramVariable.