| gov.nasa.jpf.jvm.TestJPF
All known Subclasses: gov.nasa.jpf.mc.TestCrossingJPF, gov.nasa.jpf.jvm.TestArrayJPF, gov.nasa.jpf.jvm.TestJavaLangClassJPF, gov.nasa.jpf.jvm.TestAssertJPF, gov.nasa.jpf.jvm.TestThreadJPF, gov.nasa.jpf.jvm.TestJavaLangStringJPF, gov.nasa.jpf.jvm.TestFieldJPF, gov.nasa.jpf.jvm.TestNativePeerJPF, gov.nasa.jpf.mc.TestVMDeadlockJPF, gov.nasa.jpf.jvm.TestCastJPF, gov.nasa.jpf.mc.TestOldClassicJPF, gov.nasa.jpf.jvm.TestWaitJPF, gov.nasa.jpf.jvm.TestExceptionJPF, gov.nasa.jpf.mc.TestRandomJPF, gov.nasa.jpf.jvm.TestMethodJPF,
| TestJPF | | abstract public class TestJPF extends TestCase (Code) | | base class for JPF unit tests. TestJPF mostly includes JPF invocations
that check for occurrence or absence of certain execution results
|
| runJPFDeadlock | | protected void runJPFDeadlock(String[] args)(Code) | | |
| runJPFassertionError | | protected void runJPFassertionError(String[] args)(Code) | | run JPF and case the test to fail if NO AssertionsError is encountered
|
| runJPFnoAssertionError | | protected void runJPFnoAssertionError(String[] args)(Code) | | It runs JPF and cause the test to fail if an AssertionError is encountered
|
| runJPFnoException | | protected void runJPFnoException(String[] args)(Code) | | |
|
|