de.uka.ilkd.key.symbolic_execution.object_model

Interface ISymbolicLayout

All Superinterfaces:

ISymbolicElement

All Known Implementing Classes:

SymbolicLayout, SymbolicLayoutReader.KeYlessLayout

public interface ISymbolicLayout
extends ISymbolicElement

This interface represents the root element of a symbolic memory layout.

A symbolic memory layout defines how a heap and stack looks like and which objects are the same (equivalent classes). Such memory layouts can be created automatically via a SymbolicLayoutExtractor and saved/loaded via SymbolicLayoutWriter/SymbolicLayoutReader.

The default implementation is SymbolicLayout.

Author:

Martin Hentschel

See Also:

SymbolicLayoutExtractor, SymbolicLayoutWriter, SymbolicLayoutReader, SymbolicLayout

Method Summary

Modifier and Type	Method and Description
ImmutableList<ISymbolicEquivalenceClass>	getEquivalenceClasses() Returns the equivalence classes.
ImmutableList<ISymbolicObject>	getObjects() Returns all available symbolic objects.
ISymbolicState	getState() Returns the symbolic state.

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

getSettings

Method Detail

getEquivalenceClasses

ImmutableList<ISymbolicEquivalenceClass> getEquivalenceClasses()

Returns the equivalence classes.

Returns:

The equivalence classes.

getState

ISymbolicState getState()

Returns the symbolic state.

Returns:

the symbolic state.

getObjects

ImmutableList<ISymbolicObject> getObjects()

Returns all available symbolic objects.

Returns:

The available symbolic objects.