| Interface | Description |
|---|---|
| TraceExtractor<ContentT extends AbstractState<ContentT>> |
This interface contains helper methods for producing witness traces.
|
| Class | Description |
|---|---|
| BamLocationDependentJvmMemoryLocation<ContentT extends AbstractState<ContentT>> |
This class wraps a
JvmMemoryLocation adding information on its program location and
source reached set. |
| JvmMemoryLocationAbstractState<ContentT extends AbstractState<ContentT>> |
This
AbstractState consists of a BamLocationDependentJvmMemoryLocation with a set
of sources contributed into its value and the call stack that generated it. |
| JvmMemoryLocationAbstractState.StackEntry<ContentT extends AbstractState<ContentT>> |
An entry of the call stack of the state.
|
| JvmMemoryLocationCpa<ContentT extends AbstractState<ContentT>> |
The
JvmMemoryLocationCpa backtraces memory locations. |
| JvmMemoryLocationMergeJoinOperator<ContentT extends AbstractState<ContentT>> |
This
MergeOperator applies the join operator to its arguments sharing the same memory
location. |
| JvmMemoryLocationTransferRelation<ContentT extends AbstractState<ContentT>> |
The
JvmMemoryLocationTransferRelation computes the backward successors of an JvmMemoryLocationAbstractState for a given instruction. |