| Interface | Description |
|---|---|
| TraceExtractor |
This interfaces containts helper methods for
CpaRuns producing witness traces. |
| Class | Description |
|---|---|
| BamLocationDependentJvmMemoryLocation<AbstractStateT extends AbstractState & ProgramLocationDependent<JvmCfaNode,JvmCfaEdge,MethodSignature>> |
This class wraps a
JvmMemoryLocation adding information on its program location and
source reached set. |
| JvmMemoryLocationAbstractState<AbstractStateT extends AbstractState & ProgramLocationDependent<JvmCfaNode,JvmCfaEdge,MethodSignature>> |
This
AbstractState consists of a BamLocationDependentJvmMemoryLocation with a set
of sources contributed into its value and the call stack that generated it. |
| JvmMemoryLocationAbstractState.StackEntry |
An entry of the call stack of the state.
|
| JvmMemoryLocationBamCpaRun<CpaT extends ConfigurableProgramAnalysis,AbstractStateT extends LatticeAbstractState<AbstractStateT>> |
This abstract analyzer runs the
JvmMemoryLocationCpa and returns the ReachedSet. |
| JvmMemoryLocationCpa<AbstractStateT extends LatticeAbstractState<AbstractStateT>> |
The
JvmMemoryLocationCpa backtraces memory locations. |
| JvmMemoryLocationMergeJoinOperator |
This
MergeOperator applies the join operator to its arguments sharing the same memory
location. |
| JvmMemoryLocationTransferRelation<AbstractStateT extends LatticeAbstractState<AbstractStateT>> |
The
JvmMemoryLocationTransferRelation computes the backward successors of an JvmMemoryLocationAbstractState for a given instruction. |