Package | Description |
---|---|
gov.nasa.jpf.listener | |
gov.nasa.jpf.report | |
gov.nasa.jpf.util | |
gov.nasa.jpf.util.script | |
gov.nasa.jpf.util.test | |
gov.nasa.jpf.vm |
Modifier and Type | Field and Description |
---|---|
protected JPF |
Reporter.jpf |
Constructor and Description |
---|
Reporter(Config conf,
JPF jpf) |
Modifier and Type | Method and Description |
---|---|
void |
StateExtensionClient.registerListener(JPF jpf) |
Modifier and Type | Method and Description |
---|---|
void |
ScriptEnvironment.registerListener(JPF jpf) |
Modifier and Type | Method and Description |
---|---|
protected JPF |
TestJPF.assertionError(StackTraceElement testMethod,
String... args)
run JPF expecting a AssertionError in the SuT
|
protected JPF |
TestJPF.assertionError(String... args) |
protected JPF |
TestJPF.assertionErrorDetails(StackTraceElement testMethod,
String details,
String... args) |
protected JPF |
TestJPF.assertionErrorDetails(String details,
String... args) |
protected JPF |
TestJPF.createAndRunJPF(StackTraceElement testMethod,
String[] args)
needs to be broken up into two methods for cases that do additional
JPF initialization (jpf-inspector)
this is called from the various verifyX() methods (i.e.
|
protected JPF |
TestJPF.createJPF(StackTraceElement testMethod,
String[] args)
this is never executed under JPF
|
protected JPF |
TestJPF.deadlock(String... args)
run JPF expecting a deadlock in the SuT
|
protected JPF |
TestJPF.jpfException(Class<? extends Throwable> xCls,
String... args) |
protected JPF |
TestJPF.jpfException(StackTraceElement testMethod,
Class<? extends Throwable> xCls,
String... args)
run JPF expecting it to throw an exception
NOTE - xClassName needs to be the concrete exception, not a super class
|
protected JPF |
TestJPF.noPropertyViolation(StackTraceElement testMethod,
String... args)
run JPF expecting no SuT property violations or JPF exceptions
|
protected JPF |
TestJPF.noPropertyViolation(String... args) |
protected JPF |
TestJPF.propertyViolation(Class<? extends Property> propertyCls,
String... args) |
protected JPF |
TestJPF.propertyViolation(StackTraceElement testMethod,
Class<? extends Property> propertyCls,
String... args)
run JPF expecting a property violation of the SuT
|
protected JPF |
TestJPF.unhandledException(StackTraceElement testMethod,
String xClassName,
String details,
String... args)
NOTE: this uses the exception class name because it might be an
exception type that is only known to JPF (i.e.
|
protected JPF |
TestJPF.unhandledException(String xClassName,
String details,
String... args) |
Modifier and Type | Method and Description |
---|---|
JPF |
MJIEnv.getJPF() |
JPF |
VM.getJPF() |
Constructor and Description |
---|
MultiProcessVM(JPF jpf,
Config conf) |
SingleProcessVM(JPF jpf,
Config conf) |
VM(JPF jpf,
Config conf)
be prepared this might throw JPFConfigExceptions
|