Package | Description |
---|---|
gov.nasa.jpf.jvm.bytecode | |
gov.nasa.jpf.vm |
Modifier and Type | Method and Description |
---|---|
Instruction |
SwitchInstruction.executeAllBranches(SystemState ss,
KernelState ks,
ThreadInfo ti)
useful for symbolic execution modes
|
protected Instruction |
IfInstruction.executeBothBranches(SystemState ss,
KernelState ks,
ThreadInfo ti)
use this as a delegatee in overridden executes of derived IfInstructions
(e.g.
|
Modifier and Type | Field and Description |
---|---|
protected KernelState |
AbstractRestorer.ks |
KernelState |
SystemState.ks
current execution state of the VM (stored separately by VM)
|
protected KernelState |
AbstractSerializer.ks |
Modifier and Type | Method and Description |
---|---|
KernelState |
MJIEnv.getKernelState() |
KernelState |
SystemState.getKernelState() |
KernelState |
VM.getKernelState() |
Modifier and Type | Method and Description |
---|---|
protected Memento<KernelState> |
MementoRestorer.computeRestorableData() |
Memento<KernelState> |
KernelState.getMemento() |
Memento<KernelState> |
MementoFactory.getMemento(KernelState ks) |
Memento<KernelState> |
DefaultMementoRestorer.getMemento(KernelState ks) |
Memento<KernelState> |
KernelState.getMemento(MementoFactory factory) |
Modifier and Type | Method and Description |
---|---|
Memento<KernelState> |
MementoFactory.getMemento(KernelState ks) |
Memento<KernelState> |
DefaultMementoRestorer.getMemento(KernelState ks) |
boolean |
Instruction.isSchedulingRelevant(SystemState ss,
KernelState ks,
ThreadInfo ti) |
void |
KernelState.ChangeListener.kernelStateChanged(KernelState ks) |
void |
AbstractRestorer.kernelStateChanged(KernelState same) |
void |
AbstractSerializer.kernelStateChanged(KernelState same) |
Modifier and Type | Method and Description |
---|---|
protected void |
MementoRestorer.doRestore(Memento<KernelState> data) |
Constructor and Description |
---|
GenericHeap(Config config,
KernelState ks) |
GenericSGOIDHeap(Config config,
KernelState ks) |
OVHeap(Config config,
KernelState ks) |
PSIMHeap(Config config,
KernelState ks) |
ThreadList(Config config,
KernelState ks)
Creates a new empty thread list.
|