| java.lang.Object
 gov.nasa.jpf.jvm.Verify
| Verify | | public class Verify (Code) | | Verify is the programmatic interface of JPF that can be used from inside of
applications. In order to enable programs to run outside of the JPF
environment, we provide (mostly empty) bodies for the methods that are
otherwise intercepted by the native peer class
|
| MAX_COUNTERS | | final static int MAX_COUNTERS(Code) | | |
| counter | | static int[] counter(Code) | | |
| addComment | | public static void addComment(String s)(Code) | | Adds a comment to the error trace, which will be printed and saved.
|
| assertTrue | | public static void assertTrue(String s, boolean cond)(Code) | | |
| assertTrue | | public static void assertTrue(boolean cond)(Code) | | Checks that the condition is true.
|
| atLabel | | public static void atLabel(int label)(Code) | | |
| beginAtomic | | public static void beginAtomic()(Code) | | Marks the beginning of an atomic block.
|
| boring | | public static void boring(boolean cond)(Code) | | |
| busyWait | | public static void busyWait(long duration)(Code) | | |
| currentTimeMillis | | public long currentTimeMillis()(Code) | | |
| dumpState | | public static void dumpState()(Code) | | |
| endAtomic | | public static void endAtomic()(Code) | | Marks the end of an atomic block.
|
| getBoolean | | public static boolean getBoolean()(Code) | | this is the new boolean choice generator. Since there's no real
heuristic involved with boolean values, we skip the id (it's a
hardwired "boolean")
|
| getCounter | | public static int getCounter(int id)(Code) | | |
| getDouble | | public static double getDouble(String key)(Code) | | this is the API for double value choice generators. 'id' is used to identify
both the corresponding ChoiceGenerator subclass, and the application specific
ctor parameters from the normal JPF configuration mechanism
|
| getInt | | public static int getInt(int min, int max)(Code) | | |
| getInt | | public static int getInt(String key)(Code) | | this is the API for int value choice generators. 'id' is used to identify
both the corresponding ChoiceGenerator subclass, and the application specific
ctor parameters from the normal JPF configuration mechanism
|
| ignoreIf | | public static void ignoreIf(boolean cond)(Code) | | |
| incrementCounter | | public static int incrementCounter(int id)(Code) | | |
| instrumentPoint | | public static void instrumentPoint(String label)(Code) | | |
| instrumentPointDeep | | public static void instrumentPointDeep(String label)(Code) | | |
| instrumentPointDeepRecur | | public static void instrumentPointDeepRecur(String label, int depth)(Code) | | |
| interesting | | public static void interesting(boolean cond)(Code) | | |
| isCalledFromClass | | public static boolean isCalledFromClass(String refClsName)(Code) | | |
| random | | public static int random(int max)(Code) | | Returns a random number between 0 and max inclusive.
|
| randomBool | | public static boolean randomBool()(Code) | | Returns a random boolean value, true or false. Note this gets
handled by the native peer, and is just here to enable running
instrumented applications w/o JPF
|
| resetCounter | | public static void resetCounter(int id)(Code) | | |
| setPeerClass | | public static void setPeerClass(Class cls)(Code) | | |
|
|