public class Verify extends Object
Modifier and Type | Field and Description |
---|---|
static int |
FINE |
static int |
FINER |
static int |
FINEST |
static int |
INFO |
static int |
SEVERE |
static int |
WARNING |
Constructor and Description |
---|
Verify() |
Modifier and Type | Method and Description |
---|---|
static void |
addComment(String s)
Adds a comment to the error trace, which will be printed and saved.
|
static void |
addElementAttribute(Object arr,
int idx,
int val) |
static void |
addFieldAttribute(Object o,
String fieldName,
int val) |
static void |
addLocalAttribute(String varName,
int val) |
static void |
addObjectAttribute(Object o,
int val) |
static void |
assertTrue(boolean cond)
Deprecated.
use 'assert' directly
|
static void |
assertTrue(String s,
boolean cond)
Deprecated.
use "assert cond : msg"
|
static void |
atLabel(int label) |
static void |
atLabel(String label) |
static void |
beginAtomic()
Marks the beginning of an atomic block.
|
static void |
boring(boolean cond) |
static void |
breakTransition() |
static void |
busyWait(long duration) |
static <T> T |
createFromJSON(Class<T> clazz,
String json) |
static long |
currentTimeMillis() |
static void |
endAtomic()
Marks the end of an atomic block.
|
static void |
freezeSharedness(Object o,
boolean freeze) |
static boolean |
getBitInBitSet(int id,
int bit) |
static boolean |
getBoolean()
this is the new boolean choice generator.
|
static boolean |
getBoolean(boolean falseFirst)
new boolean choice generator that also tells jpf which value to
use first by default in a search.
|
static int |
getCounter(int id) |
static double |
getDouble(String key)
this is the API for double value choice generators.
|
static double |
getDoubleFromList(double... values) |
static int |
getElementAttribute(Object arr,
int idx) |
static int[] |
getElementAttributes(Object arr,
int idx) |
static int |
getFieldAttribute(Object o,
String fieldName) |
static int[] |
getFieldAttributes(Object o,
String fieldName) |
static float |
getFloatFromList(float... values) |
static int |
getInt(int min,
int max)
Returns int nondeterministically between (and including) min and max.
|
static int |
getInt(String key)
this is the API for int value choice generators.
|
static int |
getIntFromList(int... values) |
static int |
getLocalAttribute(String varName) |
static int[] |
getLocalAttributes(String varName) |
static long |
getLongFromList(long... values) |
static Object |
getObject(String key) |
static int |
getObjectAttribute(Object o) |
static int[] |
getObjectAttributes(Object o) |
static String |
getProperty(String key) |
static int |
getValue(String key) |
static void |
ignoreIf(boolean cond) |
static int |
incrementCounter(int id) |
static void |
instrumentPoint(String label) |
static void |
instrumentPointDeep(String label) |
static void |
instrumentPointDeepRecur(String label,
int depth) |
static void |
interesting(boolean cond) |
static boolean |
isCalledFromClass(String refClsName) |
static boolean |
isRunningInJPF() |
static boolean |
isShared(Object o) |
static boolean |
isTraceReplay() |
static void |
log(String loggerId,
int logLevel,
String msg) |
static void |
log(String loggerId,
int logLevel,
String format,
Object... args) |
static void |
log(String loggerId,
int logLevel,
String msg,
String arg) |
static void |
print(String... args)
this is to avoid StringBuilders
|
static void |
print(String s) |
static void |
print(String s,
boolean b) |
static void |
print(String s,
int i) |
static void |
println() |
static void |
println(String s) |
static void |
printPathOutput(boolean cond,
String msg) |
static void |
printPathOutput(String msg)
simple debugging aids to imperatively print the current path output of the SUT
(to be used with vm.path_output)
|
static void |
putValue(String key,
int value) |
static int |
random(int max)
Returns a random number between 0 and max inclusive.
|
static boolean |
randomBool()
Returns a random boolean value, true or false.
|
static Object |
randomObject(String type) |
static <T> T |
readObjectFromFile(Class<T> clazz,
String fileName) |
static void |
resetCounter(int id) |
static void |
setBitInBitSet(int id,
int bit,
boolean value) |
static void |
setCounter(int id,
int val) |
static void |
setElementAttribute(Object arr,
int idx,
int val) |
static void |
setFieldAttribute(Object o,
String fieldName,
int val)
note - these are mostly for debugging purposes (to see if attributes get
propagated correctly, w/o having to write a listener), since attributes are
supposed to be created at the native side, and hence can't be accessed from
the application
|
static void |
setLocalAttribute(String varName,
int val) |
static void |
setObjectAttribute(Object o,
int val) |
static void |
setPeerClass(Class<?> cls) |
static void |
setProperties(String... p) |
static void |
setShared(Object o,
boolean isShared) |
static void |
storeTrace(String fileName,
String comment) |
static void |
storeTraceAndTerminate(String fileName,
String comment) |
static void |
storeTraceAndTerminateIf(boolean cond,
String fileName,
String comment) |
static void |
storeTraceIf(boolean cond,
String fileName,
String comment) |
static void |
terminateSearch() |
static boolean |
vmIsMatchingStates()
USE CAREFULLY - returns true if the virtual machine this code is
running under is doing state matching.
|
static void |
writeObjectToFile(Object object,
String fileName) |
public static final int SEVERE
public static final int WARNING
public static final int INFO
public static final int FINE
public static final int FINER
public static final int FINEST
public static void setPeerClass(Class<?> cls)
public static int getCounter(int id)
public static void resetCounter(int id)
public static void setCounter(int id, int val)
public static int incrementCounter(int id)
public static void putValue(String key, int value)
public static int getValue(String key)
public static void setBitInBitSet(int id, int bit, boolean value)
public static boolean getBitInBitSet(int id, int bit)
public static void addComment(String s)
@Deprecated public static void assertTrue(String s, boolean cond)
@Deprecated public static void assertTrue(boolean cond)
public static void atLabel(String label)
public static void atLabel(int label)
public static void beginAtomic()
public static void endAtomic()
public static void boring(boolean cond)
public static void busyWait(long duration)
public static boolean isCalledFromClass(String refClsName)
public static void ignoreIf(boolean cond)
public static void instrumentPoint(String label)
public static void instrumentPointDeep(String label)
public static void instrumentPointDeepRecur(String label, int depth)
public static void interesting(boolean cond)
public static void breakTransition()
public static void printPathOutput(String msg)
public static void printPathOutput(boolean cond, String msg)
public static void print(String s)
public static void println(String s)
public static void print(String s, int i)
public static void print(String s, boolean b)
public static void println()
public static void print(String... args)
public static void setFieldAttribute(Object o, String fieldName, int val)
public static void setLocalAttribute(String varName, int val)
public static int getLocalAttribute(String varName)
public static void addLocalAttribute(String varName, int val)
public static int[] getLocalAttributes(String varName)
public static void setElementAttribute(Object arr, int idx, int val)
public static int getElementAttribute(Object arr, int idx)
public static void addElementAttribute(Object arr, int idx, int val)
public static int[] getElementAttributes(Object arr, int idx)
public static void setObjectAttribute(Object o, int val)
public static int getObjectAttribute(Object o)
public static void addObjectAttribute(Object o, int val)
public static int[] getObjectAttributes(Object o)
public static boolean getBoolean()
public static boolean getBoolean(boolean falseFirst)
public static int getInt(int min, int max)
public static int getIntFromList(int... values)
public static int getInt(String key)
public static double getDouble(String key)
public static double getDoubleFromList(double... values)
public static long getLongFromList(long... values)
public static float getFloatFromList(float... values)
public static int random(int max)
public static boolean randomBool()
public static long currentTimeMillis()
public static boolean isRunningInJPF()
public static boolean vmIsMatchingStates()
Vector v = new Vector();
v.add(obj1);
if (Verify.getBoolean()) {
v.addAll(eleventyBillionObjectCollection);
v.setSize(1);
}
// compare states here
To the programmer, the states are (almost certainly) the same. To
the VM, they could be different (capacity inside the Vector). For
the sake of speed, Vector does not store things canonically, but this
can cause (probably mild) state explosion if matching states. If
you know whether states are being matched, you can choose the right
structure--as long as those structures aren't what you're looking for
bugs in!public static void storeTraceAndTerminateIf(boolean cond, String fileName, String comment)
public static boolean isTraceReplay()
public static boolean isShared(Object o)
public static void setShared(Object o, boolean isShared)
public static void freezeSharedness(Object o, boolean freeze)
public static void terminateSearch()
public static void setProperties(String... p)