public abstract class TestJPF extends java.lang.Object implements JPFShell
Modifier and Type | Field and Description |
---|---|
protected static boolean |
globalRunDirectly |
protected static boolean |
globalShowConfig |
protected static boolean |
hideSummary |
protected static boolean |
quiet |
protected static boolean |
runDirectly |
static java.lang.String |
SAME_PACKAGE |
protected static boolean |
showConfig |
protected static boolean |
showConfigSources |
protected static boolean |
stopOnFailure |
protected java.lang.String |
sutClassName |
static java.lang.String |
UNNAMED_PACKAGE |
Modifier | Constructor and Description |
---|---|
|
TestJPF() |
protected |
TestJPF(java.lang.String sutClassName)
to be used from default ctor of derived class if the SuT is in a different
package
|
Modifier and Type | Method and Description |
---|---|
static void |
assertArrayEquals(byte[] expected,
byte[] actual) |
static void |
assertEquals(double expected,
double actual) |
static void |
assertEquals(double expected,
double actual,
double delta) |
static void |
assertEquals(float expected,
float actual) |
static void |
assertEquals(float expected,
float actual,
float delta) |
static void |
assertEquals(int expected,
int actual) |
static void |
assertEquals(long expected,
long actual) |
static void |
assertEquals(java.lang.Object expected,
java.lang.Object actual) |
static void |
assertEquals(java.lang.String msg,
double expected,
double actual) |
static void |
assertEquals(java.lang.String msg,
double expected,
double actual,
double delta) |
static void |
assertEquals(java.lang.String msg,
float expected,
float actual) |
static void |
assertEquals(java.lang.String msg,
float expected,
float actual,
float delta) |
static void |
assertEquals(java.lang.String msg,
int expected,
int actual) |
static void |
assertEquals(java.lang.String msg,
long expected,
long actual) |
static void |
assertEquals(java.lang.String msg,
java.lang.Object expected,
java.lang.Object actual) |
static void |
assertFalse(boolean cond) |
static void |
assertFalse(java.lang.String msg,
boolean cond) |
protected JPF |
assertionError(java.lang.StackTraceElement testMethod,
java.lang.String... args)
run JPF expecting a AssertionError in the SuT
|
protected JPF |
assertionError(java.lang.String... args) |
protected JPF |
assertionErrorDetails(java.lang.StackTraceElement testMethod,
java.lang.String details,
java.lang.String... args) |
protected JPF |
assertionErrorDetails(java.lang.String details,
java.lang.String... args) |
static void |
assertNotNull(java.lang.Object o) |
static void |
assertNotNull(java.lang.String msg,
java.lang.Object o) |
static void |
assertNull(java.lang.Object o) |
static void |
assertNull(java.lang.String msg,
java.lang.Object o) |
static void |
assertSame(java.lang.Object expected,
java.lang.Object actual) |
static void |
assertSame(java.lang.String msg,
java.lang.Object expected,
java.lang.Object actual) |
static void |
assertTrue(boolean cond) |
static void |
assertTrue(java.lang.String msg,
boolean cond) |
protected JPF |
createAndRunJPF(java.lang.StackTraceElement testMethod,
java.lang.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 |
createJPF(java.lang.StackTraceElement testMethod,
java.lang.String[] args)
this is never executed under JPF
|
protected JPF |
deadlock(java.lang.String... args)
run JPF expecting a deadlock in the SuT
|
static void |
fail() |
static void |
fail(java.lang.String msg) |
static void |
fail(java.lang.String msg,
java.lang.String[] args,
java.lang.String cause) |
protected static java.util.List<java.lang.reflect.Method> |
getAfterClassMethods(java.lang.Class<? extends TestJPF> testCls) |
protected static java.util.List<java.lang.reflect.Method> |
getAfterMethods(java.lang.Class<? extends TestJPF> testCls) |
protected static java.util.List<java.lang.reflect.Method> |
getBeforeClassMethods(java.lang.Class<? extends TestJPF> testCls) |
protected static java.util.List<java.lang.reflect.Method> |
getBeforeMethods(java.lang.Class<? extends TestJPF> testCls) |
protected java.lang.StackTraceElement |
getCaller() |
protected static java.util.List<java.lang.reflect.Method> |
getContextMethods(java.lang.Class<? extends TestJPF> testCls,
int setModifiers,
int unsetModifiers,
java.lang.String annotation) |
protected static java.util.ArrayList<gov.nasa.jpf.util.test.TestJPF.GlobalArg> |
getGlobalArgs() |
protected static java.util.List<java.lang.reflect.Method> |
getMatchingMethods(java.lang.Class<? extends TestJPF> testCls,
int setModifiers,
int unsetModifiers,
java.lang.String[] annotationNames) |
protected static void |
getOptions(java.lang.String[] args) |
protected static java.lang.String |
getSutClassName(java.lang.String testClassName,
java.lang.String sutPackage)
compute the SuT class name for a given JUnit test class: remove
optionally ending "..Test", and replace package (if specified)
|
protected static java.util.List<java.lang.reflect.Method> |
getTestMethods(java.lang.Class<? extends TestJPF> testCls,
java.lang.String[] args) |
protected static boolean |
hasExplicitTestMethods(java.lang.String[] args) |
protected static boolean |
haveTestMethodSpecs(java.lang.String[] args) |
static boolean |
isJPFRun() |
static boolean |
isJUnitRun() |
protected static boolean |
isMatchingMethod(java.lang.reflect.Method m,
int setModifiers,
int unsetModifiers,
java.lang.String[] annotationNames) |
static boolean |
isRunTestRun() |
protected JPF |
jpfException(java.lang.Class<? extends java.lang.Throwable> xCls,
java.lang.String... args) |
protected JPF |
jpfException(java.lang.StackTraceElement testMethod,
java.lang.Class<? extends java.lang.Throwable> xCls,
java.lang.String... args)
run JPF expecting it to throw an exception
NOTE - xClassName needs to be the concrete exception, not a super class
|
protected JPF |
noPropertyViolation(java.lang.StackTraceElement testMethod,
java.lang.String... args)
run JPF expecting no SuT property violations
|
protected JPF |
noPropertyViolation(java.lang.String... args) |
protected JPF |
propertyViolation(java.lang.Class<? extends Property> propertyCls,
java.lang.String... args) |
protected JPF |
propertyViolation(java.lang.StackTraceElement testMethod,
java.lang.Class<? extends Property> propertyCls,
java.lang.String... args)
run JPF expecting a property violation of the SuT
|
void |
report(java.lang.String[] args) |
protected static void |
reportResults(java.lang.String clsName,
int nTests,
int nFailures,
int nErrors,
java.util.List<java.lang.String> results) |
protected static void |
reportTestCleanup(java.lang.String mthName) |
protected static void |
reportTestFinished(java.lang.String msg) |
protected static void |
reportTestInitialization(java.lang.String mthName) |
protected static void |
reportTestStart(java.lang.String mthName) |
static void |
runTests(java.lang.Class<? extends TestJPF> testCls,
java.lang.String... args)
this is the main test loop if this TestJPF instance is executed directly
or called from RunTest.
|
protected static void |
runTestsOfThisClass(java.lang.String[] testMethods)
NOTE: this needs to be called from the concrete test class, typically from
its main() method, otherwise we don't know the name of the class we have
to pass to JPF
|
protected java.lang.StackTraceElement |
setTestMethod(java.lang.String mthName) |
protected java.lang.StackTraceElement |
setTestMethod(java.lang.String clsName,
java.lang.String mthName) |
protected void |
setTestTargetKeys(Config conf,
java.lang.StackTraceElement testMethod) |
void |
start(java.lang.String[] testMethods) |
protected JPF |
unhandledException(java.lang.StackTraceElement testMethod,
java.lang.String xClassName,
java.lang.String details,
java.lang.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 |
unhandledException(java.lang.String xClassName,
java.lang.String details,
java.lang.String... args) |
protected boolean |
verifyAssertionError(java.lang.String... args) |
protected boolean |
verifyAssertionErrorDetails(java.lang.String details,
java.lang.String... args) |
protected boolean |
verifyDeadlock(java.lang.String... args) |
protected boolean |
verifyJPFException(TypeRef xClsSpec,
java.lang.String... args) |
protected boolean |
verifyNoPropertyViolation(java.lang.String... args) |
protected boolean |
verifyPropertyViolation(TypeRef propertyClsSpec,
java.lang.String... args) |
protected boolean |
verifyUnhandledException(java.lang.String xClassName,
java.lang.String... args) |
protected boolean |
verifyUnhandledExceptionDetails(java.lang.String xClassName,
java.lang.String details,
java.lang.String... args) |
public static final java.lang.String UNNAMED_PACKAGE
public static final java.lang.String SAME_PACKAGE
protected static boolean globalRunDirectly
protected static boolean globalShowConfig
protected static boolean runDirectly
protected static boolean stopOnFailure
protected static boolean showConfig
protected static boolean showConfigSources
protected static boolean hideSummary
protected static boolean quiet
protected java.lang.String sutClassName
public TestJPF()
protected TestJPF(java.lang.String sutClassName)
sutClassName
- the qualified SuT class name to be checked by JPFprotected static java.util.ArrayList<gov.nasa.jpf.util.test.TestJPF.GlobalArg> getGlobalArgs()
public static void fail(java.lang.String msg, java.lang.String[] args, java.lang.String cause)
public static void fail()
public static void fail(java.lang.String msg)
public void report(java.lang.String[] args)
protected static java.lang.String getSutClassName(java.lang.String testClassName, java.lang.String sutPackage)
testClassName
- the JUnit test classsutPackage
- optional SuT package name (without ending '.', null
os SAME_PACKAGE means same package, "" or UNNAMED_PACKAGE means unnamed package)public static boolean isJPFRun()
public static boolean isJUnitRun()
public static boolean isRunTestRun()
protected static void getOptions(java.lang.String[] args)
protected static boolean hasExplicitTestMethods(java.lang.String[] args)
protected static java.util.List<java.lang.reflect.Method> getMatchingMethods(java.lang.Class<? extends TestJPF> testCls, int setModifiers, int unsetModifiers, java.lang.String[] annotationNames)
protected static boolean isMatchingMethod(java.lang.reflect.Method m, int setModifiers, int unsetModifiers, java.lang.String[] annotationNames)
protected static java.util.List<java.lang.reflect.Method> getContextMethods(java.lang.Class<? extends TestJPF> testCls, int setModifiers, int unsetModifiers, java.lang.String annotation)
protected static java.util.List<java.lang.reflect.Method> getBeforeMethods(java.lang.Class<? extends TestJPF> testCls)
protected static java.util.List<java.lang.reflect.Method> getAfterMethods(java.lang.Class<? extends TestJPF> testCls)
protected static java.util.List<java.lang.reflect.Method> getBeforeClassMethods(java.lang.Class<? extends TestJPF> testCls)
protected static java.util.List<java.lang.reflect.Method> getAfterClassMethods(java.lang.Class<? extends TestJPF> testCls)
protected static boolean haveTestMethodSpecs(java.lang.String[] args)
protected static java.util.List<java.lang.reflect.Method> getTestMethods(java.lang.Class<? extends TestJPF> testCls, java.lang.String[] args)
protected static void reportTestStart(java.lang.String mthName)
protected static void reportTestInitialization(java.lang.String mthName)
protected static void reportTestCleanup(java.lang.String mthName)
protected static void reportTestFinished(java.lang.String msg)
protected static void reportResults(java.lang.String clsName, int nTests, int nFailures, int nErrors, java.util.List<java.lang.String> results)
public static void runTests(java.lang.Class<? extends TestJPF> testCls, java.lang.String... args)
protected static void runTestsOfThisClass(java.lang.String[] testMethods)
protected JPF createAndRunJPF(java.lang.StackTraceElement testMethod, java.lang.String[] args)
protected JPF createJPF(java.lang.StackTraceElement testMethod, java.lang.String[] args)
protected void setTestTargetKeys(Config conf, java.lang.StackTraceElement testMethod)
protected java.lang.StackTraceElement getCaller()
protected java.lang.StackTraceElement setTestMethod(java.lang.String clsName, java.lang.String mthName)
protected java.lang.StackTraceElement setTestMethod(java.lang.String mthName)
protected JPF assertionError(java.lang.StackTraceElement testMethod, java.lang.String... args)
args
- JPF main() argumentsprotected JPF assertionError(java.lang.String... args)
protected JPF assertionErrorDetails(java.lang.StackTraceElement testMethod, java.lang.String details, java.lang.String... args)
protected JPF assertionErrorDetails(java.lang.String details, java.lang.String... args)
protected boolean verifyAssertionErrorDetails(java.lang.String details, java.lang.String... args)
protected boolean verifyAssertionError(java.lang.String... args)
protected JPF noPropertyViolation(java.lang.StackTraceElement testMethod, java.lang.String... args)
protected JPF noPropertyViolation(java.lang.String... args)
protected boolean verifyNoPropertyViolation(java.lang.String... args)
protected JPF unhandledException(java.lang.StackTraceElement testMethod, java.lang.String xClassName, java.lang.String details, java.lang.String... args)
xClassName
- name of the exception base type that is expecteddetails
- detail message of the expected exceptionargs
- JPF argumentsprotected JPF unhandledException(java.lang.String xClassName, java.lang.String details, java.lang.String... args)
protected boolean verifyUnhandledExceptionDetails(java.lang.String xClassName, java.lang.String details, java.lang.String... args)
protected boolean verifyUnhandledException(java.lang.String xClassName, java.lang.String... args)
protected JPF jpfException(java.lang.StackTraceElement testMethod, java.lang.Class<? extends java.lang.Throwable> xCls, java.lang.String... args)
args
- JPF main() argumentsprotected JPF jpfException(java.lang.Class<? extends java.lang.Throwable> xCls, java.lang.String... args)
protected boolean verifyJPFException(TypeRef xClsSpec, java.lang.String... args)
protected JPF propertyViolation(java.lang.StackTraceElement testMethod, java.lang.Class<? extends Property> propertyCls, java.lang.String... args)
args
- JPF main() argumentsprotected JPF propertyViolation(java.lang.Class<? extends Property> propertyCls, java.lang.String... args)
protected boolean verifyPropertyViolation(TypeRef propertyClsSpec, java.lang.String... args)
protected JPF deadlock(java.lang.String... args)
args
- JPF main() argumentsprotected boolean verifyDeadlock(java.lang.String... args)
public static void assertEquals(java.lang.String msg, java.lang.Object expected, java.lang.Object actual)
public static void assertEquals(java.lang.Object expected, java.lang.Object actual)
public static void assertEquals(java.lang.String msg, int expected, int actual)
public static void assertEquals(int expected, int actual)
public static void assertEquals(java.lang.String msg, long expected, long actual)
public static void assertEquals(long expected, long actual)
public static void assertEquals(double expected, double actual)
public static void assertEquals(java.lang.String msg, double expected, double actual)
public static void assertEquals(float expected, float actual)
public static void assertEquals(java.lang.String msg, float expected, float actual)
public static void assertEquals(java.lang.String msg, double expected, double actual, double delta)
public static void assertEquals(double expected, double actual, double delta)
public static void assertEquals(java.lang.String msg, float expected, float actual, float delta)
public static void assertEquals(float expected, float actual, float delta)
public static void assertArrayEquals(byte[] expected, byte[] actual)
public static void assertNotNull(java.lang.String msg, java.lang.Object o)
public static void assertNotNull(java.lang.Object o)
public static void assertNull(java.lang.String msg, java.lang.Object o)
public static void assertNull(java.lang.Object o)
public static void assertSame(java.lang.String msg, java.lang.Object expected, java.lang.Object actual)
public static void assertSame(java.lang.Object expected, java.lang.Object actual)
public static void assertFalse(java.lang.String msg, boolean cond)
public static void assertFalse(boolean cond)
public static void assertTrue(java.lang.String msg, boolean cond)
public static void assertTrue(boolean cond)