public class JPF_gov_nasa_jpf_vm_Verify extends NativePeer
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 |
---|
JPF_gov_nasa_jpf_vm_Verify() |
Modifier and Type | Method and Description |
---|---|
static void |
addComment__Ljava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int stringRef) |
static void |
addElementAttribute__Ljava_lang_Object_2II__V(MJIEnv env,
int clsRef,
int oRef,
int idx,
int attr) |
static void |
addFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2I__V(MJIEnv env,
int clsRef,
int oRef,
int fnRef,
int attr) |
static void |
addLocalAttribute__Ljava_lang_String_2I__V(MJIEnv env,
int clsRef,
int varRef,
int attr) |
static void |
addObjectAttribute__Ljava_lang_Object_2I__V(MJIEnv env,
int clsRef,
int oRef,
int attr) |
static void |
assertTrue__Z__V(MJIEnv env,
int clsObjRef,
boolean b)
deprectated, just use assert
|
static void |
beginAtomic____V(MJIEnv env,
int clsObjRef) |
static void |
breakTransition____V(MJIEnv env,
int clsObjRef) |
static void |
busyWait__J__V(MJIEnv env,
int clsObjRef,
long duration) |
static int |
createFromJSON__Ljava_lang_Class_2Ljava_lang_String_2__Ljava_lang_Object_2(MJIEnv env,
int clsObjRef,
int newObjClsRef,
int jsonStringRef) |
static long |
currentTimeMillis____J(MJIEnv env,
int clsObjRef) |
static void |
endAtomic____V(MJIEnv env,
int clsObjRef) |
static void |
freezeSharedness__Ljava_lang_Object_2Z__V(MJIEnv env,
int clsObjRef,
int objRef,
boolean freeze) |
static boolean |
getBitInBitSet__II__Z(MJIEnv env,
int clsObjRef,
int id,
int bitNum) |
static boolean |
getBoolean____Z(MJIEnv env,
int clsObjRef) |
static boolean |
getBoolean__Z__Z(MJIEnv env,
int clsObjRef,
boolean falseFirst) |
static int |
getCounter__I__I(MJIEnv env,
int clsObjRef,
int counterId) |
static double |
getDouble__Ljava_lang_String_2__D(MJIEnv env,
int clsObjRef,
int idRef) |
static double |
getDoubleFromList___3D__D(MJIEnv env,
int clsObjRef,
int valArrayRef) |
static double |
getDoubleFromList(MJIEnv env,
double[] values) |
static int |
getElementAttribute__Ljava_lang_Object_2I__I(MJIEnv env,
int clsRef,
int oRef,
int idx) |
static int |
getElementAttributes__Ljava_lang_Object_2I___3I(MJIEnv env,
int clsRef,
int oRef,
int idx) |
static int |
getFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2__I(MJIEnv env,
int clsRef,
int oRef,
int fnRef) |
static int |
getFieldAttributes__Ljava_lang_Object_2Ljava_lang_String_2___3I(MJIEnv env,
int clsRef,
int oRef,
int fnRef) |
static float |
getFloatFromList___3F__F(MJIEnv env,
int clsObjRef,
int valArrayRef) |
static float |
getFloatFromList(MJIEnv env,
float[] values) |
static int |
getInt__II__I(MJIEnv env,
int clsObjRef,
int min,
int max) |
static int |
getInt__Ljava_lang_String_2__I(MJIEnv env,
int clsObjRef,
int idRef) |
static int |
getIntFromList___3I__I(MJIEnv env,
int clsObjRef,
int valArrayRef) |
static int |
getLocalAttribute__Ljava_lang_String_2__I(MJIEnv env,
int clsRef,
int varRef) |
static int |
getLocalAttributes__Ljava_lang_String_2___3I(MJIEnv env,
int clsRef,
int varRef) |
static long |
getLongFromList___3J__J(MJIEnv env,
int clsObjRef,
int valArrayRef) |
static int |
getObject__Ljava_lang_String_2__Ljava_lang_Object_2(MJIEnv env,
int clsObjRef,
int idRef) |
static int |
getObjectAttribute__Ljava_lang_Object_2__I(MJIEnv env,
int clsRef,
int oRef) |
static int |
getObjectAttributes__Ljava_lang_Object_2___3I(MJIEnv env,
int clsRef,
int oRef) |
static int |
getProperty__Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int clsObjRef,
int keyRef) |
static String |
getType(int objRef,
MJIEnv env) |
static int |
getValue__Ljava_lang_String_2__I(MJIEnv env,
int clsObjRef,
int keyRef) |
static void |
ignoreIf__Z__V(MJIEnv env,
int clsObjRef,
boolean cond) |
static int |
incrementCounter__I__I(MJIEnv env,
int clsObjRef,
int counterId) |
static boolean |
init(Config conf) |
static void |
interesting__Z__V(MJIEnv env,
int clsObjRef,
boolean cond) |
static boolean |
isCalledFromClass__Ljava_lang_String_2__Z(MJIEnv env,
int clsObjRef,
int clsNameRef) |
static boolean |
isRunningInJPF____Z(MJIEnv env,
int clsObjRef) |
static boolean |
isShared__Ljava_lang_Object_2__Z(MJIEnv env,
int clsObjRef,
int objRef) |
static boolean |
isTraceReplay____Z(MJIEnv env,
int clsObjRef) |
static void |
log__Ljava_lang_String_2ILjava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int loggerIdRef,
int logLevel,
int msgRef) |
static void |
log__Ljava_lang_String_2ILjava_lang_String_2_3Ljava_lang_Object_2__V(MJIEnv env,
int clsObjRef,
int loggerIdRef,
int logLevel,
int fmtRef,
int argsRef) |
static void |
log__Ljava_lang_String_2ILjava_lang_String_2Ljava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int loggerIdRef,
int logLevel,
int arg1Ref,
int arg2Ref) |
static void |
print___3Ljava_lang_String_2__V(MJIEnv env,
int clsRef,
int argsRef) |
static void |
print__Ljava_lang_String_2__V(MJIEnv env,
int clsRef,
int sRef) |
static void |
print__Ljava_lang_String_2I__V(MJIEnv env,
int clsRef,
int sRef,
int val) |
static void |
print__Ljava_lang_String_2Z__V(MJIEnv env,
int clsRef,
int sRef,
boolean val) |
static void |
println____V(MJIEnv env,
int clsRef) |
static void |
println__Ljava_lang_String_2__V(MJIEnv env,
int clsRef,
int sRef) |
static void |
printPathOutput__Ljava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int msgRef) |
static void |
printPathOutput__ZLjava_lang_String_2__V(MJIEnv env,
int clsObjRef,
boolean cond,
int msgRef) |
static void |
putValue__Ljava_lang_String_2I__V(MJIEnv env,
int clsObjRef,
int keyRef,
int val) |
static int |
random__I__I(MJIEnv env,
int clsObjRef,
int x)
deprecated, use getInt
|
static boolean |
randomBool(MJIEnv env,
int clsObjRef)
deprecated, use getBoolean()
|
static int |
readObjectFromFile__Ljava_lang_Class_2Ljava_lang_String_2__Ljava_lang_Object_2(MJIEnv env,
int clsObjRef,
int newObjClsRef,
int fileNameRef) |
static void |
resetCounter__I__V(MJIEnv env,
int clsObjRef,
int counterId) |
static void |
setBitInBitSet__IIZ__V(MJIEnv env,
int clsObjRef,
int id,
int bitNum,
boolean value) |
static void |
setCounter__II__V(MJIEnv env,
int clsObjRef,
int counterId,
int val) |
static void |
setElementAttribute__Ljava_lang_Object_2II__V(MJIEnv env,
int clsRef,
int oRef,
int idx,
int attr) |
static void |
setFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2I__V(MJIEnv env,
int clsRef,
int oRef,
int fnRef,
int attr) |
static void |
setLocalAttribute__Ljava_lang_String_2I__V(MJIEnv env,
int clsRef,
int varRef,
int attr) |
static void |
setObjectAttribute__Ljava_lang_Object_2I__V(MJIEnv env,
int clsRef,
int oRef,
int attr) |
static void |
setProperties___3Ljava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int argRef) |
static void |
setShared__Ljava_lang_Object_2Z__V(MJIEnv env,
int clsObjRef,
int objRef,
boolean isShared) |
static void |
storeTrace__Ljava_lang_String_2Ljava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int filenameRef,
int commentRef) |
static void |
terminateSearch____V(MJIEnv env,
int clsObjRef) |
static boolean |
vmIsMatchingStates____Z(MJIEnv env,
int clsObjRef) |
getInstance, getInstance, getPeerClass, getPeerClassName, initialize, initializePeerClass
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 boolean init(Config conf)
public static int getValue__Ljava_lang_String_2__I(MJIEnv env, int clsObjRef, int keyRef)
public static void putValue__Ljava_lang_String_2I__V(MJIEnv env, int clsObjRef, int keyRef, int val)
public static int getCounter__I__I(MJIEnv env, int clsObjRef, int counterId)
public static void resetCounter__I__V(MJIEnv env, int clsObjRef, int counterId)
public static void setCounter__II__V(MJIEnv env, int clsObjRef, int counterId, int val)
public static int incrementCounter__I__I(MJIEnv env, int clsObjRef, int counterId)
public static void setBitInBitSet__IIZ__V(MJIEnv env, int clsObjRef, int id, int bitNum, boolean value)
public static boolean getBitInBitSet__II__Z(MJIEnv env, int clsObjRef, int id, int bitNum)
public static long currentTimeMillis____J(MJIEnv env, int clsObjRef)
public static void addComment__Ljava_lang_String_2__V(MJIEnv env, int clsObjRef, int stringRef)
public static void assertTrue__Z__V(MJIEnv env, int clsObjRef, boolean b)
public static void beginAtomic____V(MJIEnv env, int clsObjRef)
public static void endAtomic____V(MJIEnv env, int clsObjRef)
public static void busyWait__J__V(MJIEnv env, int clsObjRef, long duration)
public static void ignoreIf__Z__V(MJIEnv env, int clsObjRef, boolean cond)
public static void interesting__Z__V(MJIEnv env, int clsObjRef, boolean cond)
public static void breakTransition____V(MJIEnv env, int clsObjRef)
public static boolean isCalledFromClass__Ljava_lang_String_2__Z(MJIEnv env, int clsObjRef, int clsNameRef)
public static boolean getBoolean____Z(MJIEnv env, int clsObjRef)
public static boolean getBoolean__Z__Z(MJIEnv env, int clsObjRef, boolean falseFirst)
public static int getInt__II__I(MJIEnv env, int clsObjRef, int min, int max)
public static int getIntFromList___3I__I(MJIEnv env, int clsObjRef, int valArrayRef)
public static int getInt__Ljava_lang_String_2__I(MJIEnv env, int clsObjRef, int idRef)
public static long getLongFromList___3J__J(MJIEnv env, int clsObjRef, int valArrayRef)
public static int getObject__Ljava_lang_String_2__Ljava_lang_Object_2(MJIEnv env, int clsObjRef, int idRef)
public static double getDouble__Ljava_lang_String_2__D(MJIEnv env, int clsObjRef, int idRef)
public static double getDoubleFromList(MJIEnv env, double[] values)
public static double getDoubleFromList___3D__D(MJIEnv env, int clsObjRef, int valArrayRef)
public static float getFloatFromList(MJIEnv env, float[] values)
public static float getFloatFromList___3F__F(MJIEnv env, int clsObjRef, int valArrayRef)
public static void print__Ljava_lang_String_2I__V(MJIEnv env, int clsRef, int sRef, int val)
public static void print__Ljava_lang_String_2Z__V(MJIEnv env, int clsRef, int sRef, boolean val)
public static void print___3Ljava_lang_String_2__V(MJIEnv env, int clsRef, int argsRef)
public static void print__Ljava_lang_String_2__V(MJIEnv env, int clsRef, int sRef)
public static void println__Ljava_lang_String_2__V(MJIEnv env, int clsRef, int sRef)
public static void println____V(MJIEnv env, int clsRef)
public static void setObjectAttribute__Ljava_lang_Object_2I__V(MJIEnv env, int clsRef, int oRef, int attr)
public static int getObjectAttribute__Ljava_lang_Object_2__I(MJIEnv env, int clsRef, int oRef)
public static void addObjectAttribute__Ljava_lang_Object_2I__V(MJIEnv env, int clsRef, int oRef, int attr)
public static int getObjectAttributes__Ljava_lang_Object_2___3I(MJIEnv env, int clsRef, int oRef)
public static void setFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2I__V(MJIEnv env, int clsRef, int oRef, int fnRef, int attr)
public static int getFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2__I(MJIEnv env, int clsRef, int oRef, int fnRef)
public static void addFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2I__V(MJIEnv env, int clsRef, int oRef, int fnRef, int attr)
public static int getFieldAttributes__Ljava_lang_Object_2Ljava_lang_String_2___3I(MJIEnv env, int clsRef, int oRef, int fnRef)
public static void setLocalAttribute__Ljava_lang_String_2I__V(MJIEnv env, int clsRef, int varRef, int attr)
public static int getLocalAttribute__Ljava_lang_String_2__I(MJIEnv env, int clsRef, int varRef)
public static void addLocalAttribute__Ljava_lang_String_2I__V(MJIEnv env, int clsRef, int varRef, int attr)
public static int getLocalAttributes__Ljava_lang_String_2___3I(MJIEnv env, int clsRef, int varRef)
public static void setElementAttribute__Ljava_lang_Object_2II__V(MJIEnv env, int clsRef, int oRef, int idx, int attr)
public static int getElementAttribute__Ljava_lang_Object_2I__I(MJIEnv env, int clsRef, int oRef, int idx)
public static void addElementAttribute__Ljava_lang_Object_2II__V(MJIEnv env, int clsRef, int oRef, int idx, int attr)
public static int getElementAttributes__Ljava_lang_Object_2I___3I(MJIEnv env, int clsRef, int oRef, int idx)
public static boolean randomBool(MJIEnv env, int clsObjRef)
public static int random__I__I(MJIEnv env, int clsObjRef, int x)
public static boolean isRunningInJPF____Z(MJIEnv env, int clsObjRef)
public static boolean vmIsMatchingStates____Z(MJIEnv env, int clsObjRef)
public static void storeTrace__Ljava_lang_String_2Ljava_lang_String_2__V(MJIEnv env, int clsObjRef, int filenameRef, int commentRef)
public static void terminateSearch____V(MJIEnv env, int clsObjRef)
public static boolean isTraceReplay____Z(MJIEnv env, int clsObjRef)
public static boolean isShared__Ljava_lang_Object_2__Z(MJIEnv env, int clsObjRef, int objRef)
public static void setShared__Ljava_lang_Object_2Z__V(MJIEnv env, int clsObjRef, int objRef, boolean isShared)
public static void freezeSharedness__Ljava_lang_Object_2Z__V(MJIEnv env, int clsObjRef, int objRef, boolean freeze)
public static void setProperties___3Ljava_lang_String_2__V(MJIEnv env, int clsObjRef, int argRef)
public static int getProperty__Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env, int clsObjRef, int keyRef)
public static void printPathOutput__ZLjava_lang_String_2__V(MJIEnv env, int clsObjRef, boolean cond, int msgRef)
public static void printPathOutput__Ljava_lang_String_2__V(MJIEnv env, int clsObjRef, int msgRef)
public static int createFromJSON__Ljava_lang_Class_2Ljava_lang_String_2__Ljava_lang_Object_2(MJIEnv env, int clsObjRef, int newObjClsRef, int jsonStringRef)
public static int readObjectFromFile__Ljava_lang_Class_2Ljava_lang_String_2__Ljava_lang_Object_2(MJIEnv env, int clsObjRef, int newObjClsRef, int fileNameRef)
public static void log__Ljava_lang_String_2ILjava_lang_String_2__V(MJIEnv env, int clsObjRef, int loggerIdRef, int logLevel, int msgRef)
public static void log__Ljava_lang_String_2ILjava_lang_String_2Ljava_lang_String_2__V(MJIEnv env, int clsObjRef, int loggerIdRef, int logLevel, int arg1Ref, int arg2Ref)
public static void log__Ljava_lang_String_2ILjava_lang_String_2_3Ljava_lang_Object_2__V(MJIEnv env, int clsObjRef, int loggerIdRef, int logLevel, int fmtRef, int argsRef)