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 SystemState |
DefaultBacktracker.ss |
protected SystemState |
DefaultSchedulerFactory.ss |
protected SystemState |
VM.ss |
Modifier and Type | Method and Description |
---|---|
SystemState |
MJIEnv.getSystemState() |
SystemState |
VM.getSystemState()
Gets the system state.
|
Modifier and Type | Method and Description |
---|---|
protected void |
ThreadInfo.executeTransition(SystemState ss)
enter instructions until there is none left or somebody breaks
the transition (e.g.
|
boolean |
Instruction.isSchedulingRelevant(SystemState ss,
KernelState ks,
ThreadInfo ti) |
void |
ElementInfo.notifies(SystemState ss,
ThreadInfo ti)
notifies one of the waiters.
|
void |
ElementInfo.notifies(SystemState ss,
ThreadInfo ti,
boolean hasToHoldLock) |
Constructor and Description |
---|
ContextBoundingSchedulerFactory(Config config,
VM vm,
SystemState ss) |
DefaultSchedulerFactory(Config config,
VM vm,
SystemState ss) |
DistributedSchedulerFactory(Config config,
VM vm,
SystemState ss) |
PrioritySchedulerFactory(Config config,
VM vm,
SystemState ss) |