Package | Description |
---|---|
gov.nasa.jpf.util | |
gov.nasa.jpf.util.json | |
gov.nasa.jpf.util.test | |
gov.nasa.jpf.vm |
Modifier and Type | Method and Description |
---|---|
MethodInfo |
MethodInfoRegistry.getMethodInfo(MJIEnv env,
int objRef,
String fieldName) |
static int |
ObjectConverter.JPFObjectFromJavaObject(MJIEnv env,
Object javaObject)
Create JPF object from Java object
|
Modifier and Type | Method and Description |
---|---|
int |
JSONObject.createArray(MJIEnv env,
ClassInfo ciArray,
Value value,
ChoiceGenerator<?>[] cgs,
String prefix) |
int |
JSONObject.fillObject(MJIEnv env,
ClassInfo ci,
ChoiceGenerator<?>[] cgs,
String prefix) |
Modifier and Type | Method and Description |
---|---|
void |
JPF_gov_nasa_jpf_util_test_TestJPF.$init____V(MJIEnv env,
int objRef) |
int |
JPF_gov_nasa_jpf_util_test_TestJPF.createAndRunJPF__Ljava_lang_StackTraceElement_2_3Ljava_lang_String_2__Lgov_nasa_jpf_JPF_2(MJIEnv env,
int clsObjRef,
int a1,
int a2) |
int |
JPF_gov_nasa_jpf_util_test_TestJPF.deadlock___3Ljava_lang_String_2__Lgov_nasa_jpf_JPF_2(MJIEnv env,
int clsObjRef,
int jpfArgsRef) |
int |
JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF.getProcessId____I(MJIEnv env,
int objRef) |
int |
JPF_gov_nasa_jpf_util_test_TestJPF.getProperty__Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int clsObjRef,
int keyRef) |
boolean |
JPF_gov_nasa_jpf_util_test_TestJPF.isJPFRun____Z(MJIEnv env,
int clsObjRef)
if any of our methods are executed, we know that we already run under JPF
|
boolean |
JPF_gov_nasa_jpf_util_test_TestJPF.isJUnitRun____Z(MJIEnv env,
int clsObjRef) |
boolean |
JPF_gov_nasa_jpf_util_test_TestJPF.isRunTestRun____Z(MJIEnv env,
int clsObjRef) |
int |
JPF_gov_nasa_jpf_util_test_TestJPF.jpfException__Ljava_lang_Class_2_3Ljava_lang_String_2__Lgov_nasa_jpf_JPF_2(MJIEnv env,
int clsObjRef,
int xClsRef,
int jpfArgsRef) |
static boolean |
JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF.mpVerifyAssertionError__I_3Ljava_lang_String_2__Z(MJIEnv env,
int objRef,
int numOfPrc,
int argsRef) |
static boolean |
JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF.mpVerifyAssertionErrorDetails__ILjava_lang_String_2_3Ljava_lang_String_2__Z(MJIEnv env,
int objRef,
int numOfPrc,
int rString1,
int rString2) |
static boolean |
JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF.mpVerifyDeadlock__I_3Ljava_lang_String_2__Z(MJIEnv env,
int objRef,
int numOfPrc,
int argsRef) |
static boolean |
JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF.mpVerifyJPFException__ILgov_nasa_jpf_util_TypeRef_2_3Ljava_lang_String_2__Z(MJIEnv env,
int objRef,
int numOfPrc,
int typeRef,
int argsRef) |
static boolean |
JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF.mpVerifyNoPropertyViolation__I_3Ljava_lang_String_2__Z(MJIEnv env,
int objRef,
int numOfPrc,
int argsRef) |
static boolean |
JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF.mpVerifyPropertyViolation__ILgov_nasa_jpf_util_TypeRef_2_3Ljava_lang_String_2__Z(MJIEnv env,
int objRef,
int numOfPrc,
int typeRef,
int argsRef) |
static boolean |
JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF.mpVerifyUnhandledException__ILjava_lang_String_2_3Ljava_lang_String_2__Z(MJIEnv env,
int objRef,
int numOfPrc,
int clsRef,
int argsRef) |
static boolean |
JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF.mpVerifyUnhandledExceptionDetails__ILjava_lang_String_2Ljava_lang_String_2_3Ljava_lang_String_2__Z(MJIEnv env,
int objRef,
int numOfPrc,
int clsRef,
int details,
int argsRef) |
int |
JPF_gov_nasa_jpf_util_test_TestJPF.noPropertyViolation___3Ljava_lang_String_2__Lgov_nasa_jpf_JPF_2(MJIEnv env,
int clsObjRef,
int jpfArgsRef) |
int |
JPF_gov_nasa_jpf_util_test_TestJPF.propertyViolation__Ljava_lang_Class_2_3Ljava_lang_String_2__Lgov_nasa_jpf_JPF_2(MJIEnv env,
int clsObjRef,
int propClsRef,
int jpfArgsRef) |
void |
JPF_gov_nasa_jpf_util_test_TestJPF.runTestsOfThisClass___3Ljava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int selectedTestsRef) |
int |
JPF_gov_nasa_jpf_util_test_TestJPF.unhandledException__Ljava_lang_String_2Ljava_lang_String_2_3Ljava_lang_String_2__Lgov_nasa_jpf_JPF_2(MJIEnv env,
int clsObjRef,
int xClassNameRef,
int detailsRef,
int jpfArgsRef) |
boolean |
JPF_gov_nasa_jpf_util_test_TestJPF.verifyAssertionError___3Ljava_lang_String_2__Z(MJIEnv env,
int clsObjRef,
int jpfArgsRef) |
boolean |
JPF_gov_nasa_jpf_util_test_TestJPF.verifyAssertionErrorDetails__Ljava_lang_String_2_3Ljava_lang_String_2__Z(MJIEnv env,
int clsObjRef,
int detailsRef,
int jpfArgsRef) |
boolean |
JPF_gov_nasa_jpf_util_test_TestJPF.verifyDeadlock___3Ljava_lang_String_2__Z(MJIEnv env,
int clsObjRef,
int jpfArgsRef) |
boolean |
JPF_gov_nasa_jpf_util_test_TestJPF.verifyJPFException__Lgov_nasa_jpf_util_TypeRef_2_3Ljava_lang_String_2__Z(MJIEnv env,
int clsObjRef,
int xClsRef,
int jpfArgsRef) |
boolean |
JPF_gov_nasa_jpf_util_test_TestJPF.verifyNoPropertyViolation___3Ljava_lang_String_2__Z(MJIEnv env,
int clsObjRef,
int jpfArgsRef) |
boolean |
JPF_gov_nasa_jpf_util_test_TestJPF.verifyPropertyViolation__Lgov_nasa_jpf_util_TypeRef_2_3Ljava_lang_String_2__Z(MJIEnv env,
int clsObjRef,
int propClsRef,
int jpfArgsRef) |
boolean |
JPF_gov_nasa_jpf_util_test_TestJPF.verifyUnhandledException__Ljava_lang_String_2_3Ljava_lang_String_2__Z(MJIEnv env,
int clsObjRef,
int xClassNameRef,
int jpfArgsRef) |
boolean |
JPF_gov_nasa_jpf_util_test_TestJPF.verifyUnhandledExceptionDetails__Ljava_lang_String_2Ljava_lang_String_2_3Ljava_lang_String_2__Z(MJIEnv env,
int clsObjRef,
int xClassNameRef,
int detailsRef,
int jpfArgsRef) |
Modifier and Type | Method and Description |
---|---|
MJIEnv |
ThreadInfo.getEnv() |
MJIEnv |
ThreadInfo.getMJIEnv() |
Modifier and Type | Method and Description |
---|---|
void |
JPF_java_text_Bidi.$clinit____V(MJIEnv env,
int clsObjRef) |
void |
JPF_java_util_concurrent_atomic_AtomicLong.$clinit____V(MJIEnv env,
int rcls) |
void |
JPF_java_lang_Character.$clinit____V(MJIEnv env,
int clsObjRef) |
void |
JPF_java_util_concurrent_atomic_AtomicInteger.$clinit____V(MJIEnv env,
int rcls) |
void |
JPF_java_lang_StringBuffer.$clinit____V(MJIEnv env,
int clsObjRef) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.$init____V(MJIEnv env,
int objref)
these are the native methods we intercept
|
void |
JPF_java_util_Random.$init____V(MJIEnv env,
int objRef) |
void |
JPF_java_lang_ClassLoader.$init____V(MJIEnv env,
int objRef) |
void |
JPF_java_util_Random.$init__J__V(MJIEnv env,
int objRef,
long seedStarter) |
void |
JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.$init__Ljava_lang_Class_2Ljava_lang_Class_2Ljava_lang_String_2__V(MJIEnv env,
int objRef,
int tClsObjRef,
int fClsObjRef,
int fNameRef) |
void |
JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.$init__Ljava_lang_Class_2Ljava_lang_String_2__V(MJIEnv env,
int objRef,
int tClsObjRef,
int fNameRef) |
void |
JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.$init__Ljava_lang_Class_2Ljava_lang_String_2__V(MJIEnv env,
int objRef,
int tClsObjRef,
int fNameRef) |
void |
JPF_java_lang_ClassLoader.$init__Ljava_lang_ClassLoader_2__V(MJIEnv env,
int objRef,
int parentRef) |
double |
JPF_java_lang_Math.abs__D__D(MJIEnv env,
int clsObjRef,
double a) |
float |
JPF_java_lang_Math.abs__F__F(MJIEnv env,
int clsObjRef,
float a) |
int |
JPF_java_lang_Math.abs__I__I(MJIEnv env,
int clsObjRef,
int a) |
long |
JPF_java_lang_Math.abs__J__J(MJIEnv env,
int clsObjRef,
long a) |
double |
JPF_java_lang_Math.acos__D__D(MJIEnv env,
int clsObjRef,
double a) |
static void |
JPF_gov_nasa_jpf_vm_Verify.addComment__Ljava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int stringRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.addElementAttribute__Ljava_lang_Object_2II__V(MJIEnv env,
int clsRef,
int oRef,
int idx,
int attr) |
static void |
JPF_gov_nasa_jpf_vm_Verify.addFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2I__V(MJIEnv env,
int clsRef,
int oRef,
int fnRef,
int attr) |
static void |
JPF_gov_nasa_jpf_vm_Verify.addLocalAttribute__Ljava_lang_String_2I__V(MJIEnv env,
int clsRef,
int varRef,
int attr) |
static void |
JPF_gov_nasa_jpf_vm_Verify.addObjectAttribute__Ljava_lang_Object_2I__V(MJIEnv env,
int clsRef,
int oRef,
int attr) |
void |
JPF_java_lang_Runtime.addShutdownHook__Ljava_lang_Thread_2__V(MJIEnv env,
int objref,
int threadRef) |
void |
JPF_java_net_URLClassLoader.addURL0__Ljava_lang_String_2__V(MJIEnv env,
int objRef,
int urlRef) |
long |
JPF_sun_misc_Unsafe.allocateMemory__J__J(MJIEnv env,
int unsafeRef,
long nBytes) |
int |
JPF_gov_nasa_jpf_AnnotationProxyBase.annotationType____Ljava_lang_Class_2(MJIEnv env,
int objref) |
int |
JPF_java_lang_StringBuffer.append__C__Ljava_lang_StringBuffer_2(MJIEnv env,
int objref,
char c) |
int |
JPF_java_lang_StringBuilder.append__C__Ljava_lang_StringBuilder_2(MJIEnv env,
int objref,
char c) |
int |
JPF_java_lang_StringBuffer.append__D__Ljava_lang_StringBuffer_2(MJIEnv env,
int objref,
double d) |
int |
JPF_java_lang_StringBuilder.append__D__Ljava_lang_StringBuilder_2(MJIEnv env,
int objref,
double d) |
int |
JPF_java_lang_StringBuffer.append__F__Ljava_lang_StringBuffer_2(MJIEnv env,
int objref,
float f) |
int |
JPF_java_lang_StringBuilder.append__F__Ljava_lang_StringBuilder_2(MJIEnv env,
int objref,
float f) |
int |
JPF_java_lang_StringBuffer.append__I__Ljava_lang_StringBuffer_2(MJIEnv env,
int objref,
int i) |
int |
JPF_java_lang_StringBuilder.append__I__Ljava_lang_StringBuilder_2(MJIEnv env,
int objref,
int i) |
int |
JPF_java_lang_StringBuffer.append__J__Ljava_lang_StringBuffer_2(MJIEnv env,
int objref,
long l) |
int |
JPF_java_lang_StringBuilder.append__J__Ljava_lang_StringBuilder_2(MJIEnv env,
int objref,
long l) |
int |
JPF_java_lang_StringBuffer.append__Ljava_lang_String_2__Ljava_lang_StringBuffer_2(MJIEnv env,
int objref,
int sref) |
int |
JPF_java_lang_StringBuilder.append__Ljava_lang_String_2__Ljava_lang_StringBuilder_2(MJIEnv env,
int objref,
int sref) |
int |
JPF_java_lang_StringBuffer.append__Z__Ljava_lang_StringBuffer_2(MJIEnv env,
int objref,
boolean b) |
int |
JPF_java_lang_StringBuilder.append__Z__Ljava_lang_StringBuilder_2(MJIEnv env,
int objref,
boolean b) |
int |
JPF_sun_misc_Unsafe.arrayBaseOffset__Ljava_lang_Class_2__I(MJIEnv env,
int unsafeRef,
int clazz) |
void |
JPF_java_lang_System.arraycopy__Ljava_lang_Object_2ILjava_lang_Object_2II__V(MJIEnv env,
int clsObjRef,
int srcArrayRef,
int srcIdx,
int dstArrayRef,
int dstIdx,
int length) |
int |
JPF_sun_misc_Unsafe.arrayIndexScale__Ljava_lang_Class_2__I(MJIEnv env,
int unsafeRef,
int clazz) |
double |
JPF_java_lang_Math.asin__D__D(MJIEnv env,
int clsObjRef,
double a) |
static void |
JPF_gov_nasa_jpf_vm_Verify.assertTrue__Z__V(MJIEnv env,
int clsObjRef,
boolean b)
deprectated, just use assert
|
double |
JPF_java_lang_Math.atan__D__D(MJIEnv env,
int clsObjRef,
double a) |
double |
JPF_java_lang_Math.atan2__DD__D(MJIEnv env,
int clsObjRef,
double a,
double b) |
int |
JPF_java_io_FileDescriptor.available____I(MJIEnv env,
int objref) |
int |
JPF_java_lang_Runtime.availableProcessors____I(MJIEnv env,
int objref) |
static void |
JPF_gov_nasa_jpf_vm_Verify.beginAtomic____V(MJIEnv env,
int clsObjRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.breakTransition____V(MJIEnv env,
int clsObjRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.busyWait__J__V(MJIEnv env,
int clsObjRef,
long duration) |
void |
JPF_java_io_ObjectInputStream.bytesToDoubles___3BI_3DII__(MJIEnv env,
int clsRef,
int baRef,
int bOff,
int daRef,
int dOff,
int nDoubles) |
void |
JPF_java_io_ObjectInputStream.bytesToFloats___3BI_3FII__(MJIEnv env,
int clsRef,
int baRef,
int bOff,
int faRef,
int fOff,
int nFloats) |
boolean |
JPF_java_io_File.canRead____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_io_File.canWrite____Z(MJIEnv env,
int objref) |
double |
JPF_java_lang_Math.ceil__D__D(MJIEnv env,
int clsObjRef,
double a) |
char |
JPF_java_lang_String.charAt__I__C(MJIEnv env,
int objRef,
int index) |
protected static boolean |
JPF_java_lang_ClassLoader.check(MJIEnv env,
String cname,
byte[] buffer,
int offset,
int length) |
protected static void |
JPF_java_lang_ClassLoader.checkData(MJIEnv env,
byte[] buffer,
int offset,
int length) |
protected static void |
JPF_java_lang_ClassLoader.checkForIllegalName(MJIEnv env,
String name) |
protected static void |
JPF_java_lang_ClassLoader.checkForProhibitedPkg(MJIEnv env,
String name) |
void |
JPF_java_lang_ClassLoader.clearAssertionStatus____V(MJIEnv env,
int objRef) |
int |
JPF_java_lang_Object.clone____Ljava_lang_Object_2(MJIEnv env,
int objref) |
void |
JPF_java_io_FileDescriptor.close0(MJIEnv env,
int objref) |
int |
JPF_java_lang_String.codePointAt__I__I(MJIEnv env,
int objRef,
int index) |
int |
JPF_java_lang_String.codePointBefore__I__I(MJIEnv env,
int objRef,
int index) |
int |
JPF_java_lang_String.codePointCount__II__I(MJIEnv env,
int objRef,
int beginIndex,
int endIndex) |
boolean |
JPF_java_util_concurrent_atomic_AtomicInteger.compareAndSet__II__Z(MJIEnv env,
int objRef,
int expect,
int update) |
boolean |
JPF_java_util_concurrent_atomic_AtomicLong.compareAndSet__JJ__Z(MJIEnv env,
int objRef,
long expect,
long update) |
boolean |
JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.compareAndSet__Ljava_lang_Object_2II__Z(MJIEnv env,
int objRef,
int tRef,
int fExpect,
int fUpdate) |
boolean |
JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.compareAndSet__Ljava_lang_Object_2JJ__Z(MJIEnv env,
int objRef,
int tRef,
long fExpect,
long fUpdate) |
boolean |
JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.compareAndSet__Ljava_lang_Object_2Ljava_lang_Object_2Ljava_lang_Object_2__Z(MJIEnv env,
int objRef,
int tRef,
int fExpect,
int fUpdate) |
boolean |
JPF_java_util_concurrent_atomic_AtomicIntegerArray.compareAndSetNative__III__Z(MJIEnv env,
int objRef,
int index,
int expect,
int update) |
boolean |
JPF_java_util_concurrent_atomic_AtomicLongArray.compareAndSetNative__IJJ__Z(MJIEnv env,
int objRef,
int index,
long expect,
long update) |
boolean |
JPF_java_util_concurrent_atomic_AtomicReferenceArray.compareAndSetNative__ILjava_lang_Object_2Ljava_lang_Object_2__Z(MJIEnv env,
int objRef,
int index,
int fExpect,
int fUpdate) |
boolean |
JPF_sun_misc_Unsafe.compareAndSwapInt__Ljava_lang_Object_2JII__Z(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
int expect,
int update) |
boolean |
JPF_sun_misc_Unsafe.compareAndSwapLong__Ljava_lang_Object_2JJJ__Z(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
long expect,
long update) |
boolean |
JPF_sun_misc_Unsafe.compareAndSwapObject__Ljava_lang_Object_2JLjava_lang_Object_2Ljava_lang_Object_2__Z(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
int expectRef,
int updateRef) |
int |
JPF_java_lang_String.compareTo__Ljava_lang_String_2__I(MJIEnv env,
int objRef,
int anotherStringRef) |
int |
JPF_java_lang_String.concat__Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int objRef,
int strRef) |
double |
JPF_java_lang_Math.cos__D__D(MJIEnv env,
int clsObjRef,
double a) |
int |
JPF_java_lang_Thread.countStackFrames____I(MJIEnv env,
int objref) |
int |
JPF_java_util_TimeZone.createDefaultZone____Ljava_util_TimeZone_2(MJIEnv env,
int clsObjRef) |
static int |
JPF_gov_nasa_jpf_vm_Verify.createFromJSON__Ljava_lang_Class_2Ljava_lang_String_2__Ljava_lang_Object_2(MJIEnv env,
int clsObjRef,
int newObjClsRef,
int jsonStringRef) |
boolean |
JPF_java_io_File.createNewFile____Z(MJIEnv env,
int objref) |
static int |
JPF_java_lang_ClassLoader.createPackageObject(MJIEnv env,
ClassInfo pkgClass,
String pkgName,
ClassLoaderInfo cl) |
int |
JPF_java_lang_Throwable.createStackTrace_____3Ljava_lang_StackTraceElement_2(MJIEnv env,
int objref)
return array of StackTraceElement elements from the snapshot stored in the Throwable
|
int |
JPF_java_lang_System.createSystemErr____Ljava_io_PrintStream_2(MJIEnv env,
int clsObjRef) |
int |
JPF_java_lang_System.createSystemOut____Ljava_io_PrintStream_2(MJIEnv env,
int clsObjRef) |
int |
JPF_java_lang_Thread.currentThread____Ljava_lang_Thread_2(MJIEnv env,
int clsObjRef) |
long |
JPF_java_lang_System.currentTimeMillis____J(MJIEnv env,
int clsObjRef) |
static long |
JPF_gov_nasa_jpf_vm_Verify.currentTimeMillis____J(MJIEnv env,
int clsObjRef) |
int |
JPF_java_io_InputStreamReader.decode___3BI_3CIZ__I(MJIEnv env,
int objref,
int bref,
int len,
int cref,
int off,
boolean endOfInput) |
int |
JPF_java_lang_StringCoding.decode___3BII___3C(MJIEnv env,
int clsObjRef,
int bref,
int off,
int len) |
int |
JPF_java_io_InputStreamReader.decode__IZ__I(MJIEnv env,
int objref,
int b,
boolean endOfInput) |
int |
JPF_java_net_URLDecoder.decode__Ljava_lang_String_2Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int clsObjRef,
int sRef,
int encRef) |
int |
JPF_java_lang_ClassLoader.defineClass0__Ljava_lang_String_2_3BII__Ljava_lang_Class_2(MJIEnv env,
int objRef,
int nameRef,
int bufferRef,
int offset,
int length) |
int |
JPF_java_lang_reflect_Proxy.defineClass0(MJIEnv env,
int clsObjRef,
int classLoaderRef,
int nameRef,
int bufferRef,
int offset,
int length) |
boolean |
JPF_java_io_File.delete____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_lang_Class.desiredAssertionStatus____Z(MJIEnv env,
int robj) |
int |
JPF_java_security_MessageDigest.digest___3B___3B(MJIEnv env,
int objRef,
int inputRef) |
int |
JPF_java_lang_Character.digit__CI__I(MJIEnv env,
int clsObjRef,
char c,
int radix) |
void |
JPF_java_io_ObjectOutputStream.doublesToBytes___3DI_3BII__(MJIEnv env,
int clsRef,
int daRef,
int dOff,
int baRef,
int bOff,
int nDoubles) |
long |
JPF_java_lang_Double.doubleToLongBits__D__J(MJIEnv env,
int rcls,
double v0) |
long |
JPF_java_lang_Double.doubleToRawLongBits__D__J(MJIEnv env,
int rcls,
double v0) |
void |
JPF_java_lang_Thread.dumpStack____V(MJIEnv env,
int clsObjRef) |
int |
JPF_java_lang_StringCoding.encode___3CII___3B(MJIEnv env,
int clsObjRef,
int cref,
int off,
int len) |
int |
JPF_java_io_OutputStreamWriter.encode___3CII_3B__I(MJIEnv env,
int objref,
int cref,
int off,
int len,
int bref) |
int |
JPF_java_io_OutputStreamWriter.encode__C_3B__I(MJIEnv env,
int objref,
char c,
int bufref) |
int |
JPF_java_io_OutputStreamWriter.encode__Ljava_lang_String_2II_3B__I(MJIEnv env,
int objref,
int sref,
int off,
int len,
int bref) |
int |
JPF_java_net_URLEncoder.encode__Ljava_lang_String_2Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int clsObjRef,
int sRef,
int encRef) |
int |
JPF_java_util_regex_Matcher.end__I__I(MJIEnv env,
int objref,
int group) |
static void |
JPF_gov_nasa_jpf_vm_Verify.endAtomic____V(MJIEnv env,
int clsObjRef) |
void |
JPF_sun_misc_Unsafe.ensureClassInitialized__Ljava_lang_Class_2__V(MJIEnv env,
int unsafeRef,
int clsObjRef) |
boolean |
JPF_java_lang_reflect_Field.equals__Ljava_lang_Object_2__Z(MJIEnv env,
int objRef,
int fobjRef) |
boolean |
JPF_java_lang_reflect_Constructor.equals__Ljava_lang_Object_2__Z(MJIEnv env,
int objRef,
int mthRef) |
boolean |
JPF_java_lang_reflect_Method.equals__Ljava_lang_Object_2__Z(MJIEnv env,
int objRef,
int mthRef) |
boolean |
JPF_java_lang_String.equals__Ljava_lang_Object_2__Z(MJIEnv env,
int objRef,
int argRef) |
boolean |
JPF_java_lang_String.equals0___3C_3CI__Z(MJIEnv env,
int clsObjRef,
int charsRef1,
int charsRef2,
int len) |
boolean |
JPF_java_lang_String.equalsIgnoreCase__Ljava_lang_String_2__Z(MJIEnv env,
int objref,
int anotherString) |
void |
JPF_gov_nasa_jpf_tools_MethodTester.error__Ljava_lang_String_2__V(MJIEnv env,
int objRef,
int msgRef) |
boolean |
JPF_java_io_File.exists____Z(MJIEnv env,
int objref) |
void |
JPF_java_lang_System.exit__I__V(MJIEnv env,
int clsObjRef,
int ret) |
double |
JPF_java_lang_Math.exp__D__D(MJIEnv env,
int clsObjRef,
double a) |
int |
JPF_sun_misc_Unsafe.fieldOffset__Ljava_lang_reflect_Field_2__I(MJIEnv env,
int unsafeRef,
int fieldRef)
we don't really return an offset here, since that would be useless.
|
int |
JPF_java_lang_Throwable.fillInStackTrace____Ljava_lang_Throwable_2(MJIEnv env,
int objref) |
void |
JPF_java_security_MessageDigest.finalize____(MJIEnv env,
int objRef) |
boolean |
JPF_java_util_regex_Matcher.find____Z(MJIEnv env,
int objref) |
int |
JPF_java_net_URLClassLoader.findClass__Ljava_lang_String_2__Ljava_lang_Class_2(MJIEnv env,
int objRef,
int nameRef) |
int |
JPF_java_lang_ClassLoader.findLoadedClass__Ljava_lang_String_2__Ljava_lang_Class_2(MJIEnv env,
int objRef,
int nameRef) |
int |
JPF_java_net_URLClassLoader.findResource0__Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int objRef,
int resRef) |
int |
JPF_java_net_URLClassLoader.findResources0__Ljava_lang_String_2___3Ljava_lang_String_2(MJIEnv env,
int objRef,
int resRef) |
int |
JPF_java_lang_ClassLoader.findSystemClass__Ljava_lang_String_2__Ljava_lang_Class_2(MJIEnv env,
int objRef,
int nameRef) |
int |
JPF_java_lang_Float.floatToIntBits__F__I(MJIEnv env,
int rcls,
float v0) |
int |
JPF_java_lang_Float.floatToRawIntBits__F__I(MJIEnv env,
int rcls,
float v0) |
double |
JPF_java_lang_Math.floor__D__D(MJIEnv env,
int clsObjRef,
double a) |
char |
JPF_java_lang_Character.forDigit__II__C(MJIEnv env,
int clsObjRef,
int digit,
int radix) |
int |
JPF_java_text_DecimalFormat.format__D__Ljava_lang_String_2(MJIEnv env,
int objref,
double number) |
int |
JPF_java_text_DecimalFormat.format__J__Ljava_lang_String_2(MJIEnv env,
int objref,
long number) |
int |
JPF_java_lang_String.format__Ljava_lang_String_2_3Ljava_lang_Object_2__Ljava_lang_String_2(MJIEnv env,
int clsObjRef,
int fmtRef,
int argRef) |
int |
JPF_java_text_DateFormat.format__Ljava_util_Date_2__Ljava_lang_String_2(MJIEnv env,
int objref,
int dateRef) |
int |
JPF_java_lang_String.format__Ljava_util_Locale_2Ljava_lang_String_2_3Ljava_lang_Object_2__Ljava_lang_String_2(MJIEnv env,
int clsObjRef,
int locRef,
int fmtRef,
int argRef) |
int |
JPF_java_text_SimpleDateFormat.format0(MJIEnv env,
int objref,
long dateTime) |
int |
JPF_java_lang_Class.forName__Ljava_lang_String_2__Ljava_lang_Class_2(MJIEnv env,
int rcls,
int clsNameRef) |
long |
JPF_java_lang_Runtime.freeMemory____J(MJIEnv env,
int objref) |
void |
JPF_sun_misc_Unsafe.freeMemory__J__V(MJIEnv env,
int unsafeRef,
long startAddress) |
static void |
JPF_gov_nasa_jpf_vm_Verify.freezeSharedness__Ljava_lang_Object_2Z__V(MJIEnv env,
int clsObjRef,
int objRef,
boolean freeze) |
void |
JPF_java_lang_System.gc____V(MJIEnv env,
int clsObjRef) |
void |
JPF_java_lang_Runtime.gc____V(MJIEnv env,
int objref) |
int |
JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.get__Ljava_lang_Object_2__I(MJIEnv env,
int objRef,
int tRef) |
long |
JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.get__Ljava_lang_Object_2__J(MJIEnv env,
int objRef,
int tRef) |
int |
JPF_java_lang_reflect_Field.get__Ljava_lang_Object_2__Ljava_lang_Object_2(MJIEnv env,
int objRef,
int fobjRef) |
int |
JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.get__Ljava_lang_Object_2__Ljava_lang_Object_2(MJIEnv env,
int objRef,
int tRef) |
int |
JPF_java_lang_reflect_Array.get__Ljava_lang_Object_2I__Ljava_lang_Object_2(MJIEnv env,
int clsRef,
int aref,
int index) |
int |
JPF_java_io_File.getAbsoluteFile____Ljava_io_File_2(MJIEnv env,
int objref) |
int |
JPF_java_io_File.getAbsolutePath____Ljava_lang_String_2(MJIEnv env,
int objref) |
int |
JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.getAndAdd__Ljava_lang_Object_2I__I(MJIEnv env,
int objRef,
int tRef,
int fDelta) |
long |
JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.getAndAdd__Ljava_lang_Object_2J__J(MJIEnv env,
int objRef,
int tRef,
long fDelta) |
int |
JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.getAndSet__Ljava_lang_Object_2I__I(MJIEnv env,
int objRef,
int tRef,
int fNewValue) |
long |
JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.getAndSet__Ljava_lang_Object_2J__J(MJIEnv env,
int objRef,
int tRef,
long fNewValue) |
int |
JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.getAndSet__Ljava_lang_Object_2Ljava_lang_Object_2__Ljava_lang_Object_2(MJIEnv env,
int objRef,
int tRef,
int fNewValue) |
int |
JPF_java_lang_reflect_Field.getAnnotation__Ljava_lang_Class_2__Ljava_lang_annotation_Annotation_2(MJIEnv env,
int objRef,
int annotationClsRef) |
int |
JPF_java_lang_reflect_Constructor.getAnnotation__Ljava_lang_Class_2__Ljava_lang_annotation_Annotation_2(MJIEnv env,
int objRef,
int annotationClsRef) |
int |
JPF_java_lang_Class.getAnnotation__Ljava_lang_Class_2__Ljava_lang_annotation_Annotation_2(MJIEnv env,
int robj,
int annoClsRef) |
int |
JPF_java_lang_reflect_Method.getAnnotation__Ljava_lang_Class_2__Ljava_lang_annotation_Annotation_2(MJIEnv env,
int mthRef,
int annotationClsRef) |
int |
JPF_java_lang_reflect_Field.getAnnotations_____3Ljava_lang_annotation_Annotation_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_reflect_Constructor.getAnnotations_____3Ljava_lang_annotation_Annotation_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_Class.getAnnotations_____3Ljava_lang_annotation_Annotation_2(MJIEnv env,
int robj) |
int |
JPF_java_lang_reflect_Method.getAnnotations_____3Ljava_lang_annotation_Annotation_2(MJIEnv env,
int mthRef) |
int |
JPF_java_util_TimeZone.getAvailableIDs_____3Ljava_lang_String_2(MJIEnv env,
int clsObjRef) |
int |
JPF_java_util_TimeZone.getAvailableIDs__I___3Ljava_lang_String_2(MJIEnv env,
int clsObjRef,
int rawOffset) |
static boolean |
JPF_gov_nasa_jpf_vm_Verify.getBitInBitSet__II__Z(MJIEnv env,
int clsObjRef,
int id,
int bitNum) |
static boolean |
JPF_gov_nasa_jpf_vm_Verify.getBoolean____Z(MJIEnv env,
int clsObjRef) |
boolean |
JPF_java_lang_reflect_Field.getBoolean__Ljava_lang_Object_2__Z(MJIEnv env,
int objRef,
int fobjRef) |
boolean |
JPF_java_lang_reflect_Array.getBoolean__Ljava_lang_Object_2I__Z(MJIEnv env,
int clsRef,
int aref,
int index) |
boolean |
JPF_sun_misc_Unsafe.getBoolean__Ljava_lang_Object_2J__Z(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
static boolean |
JPF_gov_nasa_jpf_vm_Verify.getBoolean__Z__Z(MJIEnv env,
int clsObjRef,
boolean falseFirst) |
boolean |
JPF_sun_misc_Unsafe.getBooleanVolatile__Ljava_lang_Object_2J__Z(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
byte |
JPF_sun_misc_Unsafe.getByte__J__B(MJIEnv env,
int unsafeRef,
long address) |
byte |
JPF_java_lang_reflect_Field.getByte__Ljava_lang_Object_2__B(MJIEnv env,
int objRef,
int fobjRef) |
static byte |
JPF_java_lang_reflect_Array.getByte__Ljava_lang_Object_2I__B(MJIEnv env,
int clsRef,
int aref,
int index) |
byte |
JPF_sun_misc_Unsafe.getByte__Ljava_lang_Object_2J__B(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
int |
JPF_java_lang_Class.getByteArrayFromResourceStream(MJIEnv env,
int clsRef,
int nameRef)
<2do> needs to load from the classfile location, NOT the MJIEnv (native) class
|
int |
JPF_java_lang_String.getBytes_____3B(MJIEnv env,
int objRef) |
void |
JPF_java_lang_String.getBytes__II_3BI__V(MJIEnv env,
int objRef,
int srcBegin,
int srcEnd,
int dstRef,
int dstBegin) |
int |
JPF_java_lang_String.getBytes__Ljava_lang_String_2___3B(MJIEnv env,
int objRef,
int charSetRef) |
byte |
JPF_sun_misc_Unsafe.getByteVolatile__Ljava_lang_Object_2J__B(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
int |
JPF_sun_reflect_Reflection.getCallerClass__I__Ljava_lang_Class_2(MJIEnv env,
int clsObjRef,
int offset) |
int |
JPF_java_io_File.getCanonicalFile____Ljava_io_File_2(MJIEnv env,
int objref) |
int |
JPF_java_lang_Class.getCanonicalName____Ljava_lang_String_2(MJIEnv env,
int clsRef) |
int |
JPF_java_io_File.getCanonicalPath____Ljava_lang_String_2(MJIEnv env,
int objref) |
char |
JPF_sun_misc_Unsafe.getChar__J__C(MJIEnv env,
int unsafeRef,
long address) |
char |
JPF_java_lang_reflect_Field.getChar__Ljava_lang_Object_2__C(MJIEnv env,
int objRef,
int fobjRef) |
char |
JPF_java_lang_reflect_Array.getChar__Ljava_lang_Object_2I__C(MJIEnv env,
int clsRef,
int aref,
int index) |
char |
JPF_sun_misc_Unsafe.getChar__Ljava_lang_Object_2J__C(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
void |
JPF_java_lang_String.getChars__II_3CI__V(MJIEnv env,
int objRef,
int srcBegin,
int srcEnd,
int dstRef,
int dstBegin) |
char |
JPF_sun_misc_Unsafe.getCharVolatile__Ljava_lang_Object_2J__C(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
int |
JPF_java_lang_Object.getClass____Ljava_lang_Class_2(MJIEnv env,
int objref) |
int |
JPF_java_util_ResourceBundle.getClassContext_____3Ljava_lang_Class_2(MJIEnv env,
int clsRef) |
static int |
JPF_java_lang_Class.getClassObject(MJIEnv env,
ClassInfo ci) |
int |
JPF_java_lang_Class.getComponentType____Ljava_lang_Class_2(MJIEnv env,
int robj) |
int |
JPF_sun_net_www_protocol_http_Handler.getConnectionClass__Ljava_lang_String_2__Ljava_lang_Class_2(MJIEnv env,
int objref,
int surlRef) |
int |
JPF_java_lang_Class.getConstructor___3Ljava_lang_Class_2__Ljava_lang_reflect_Constructor_2(MJIEnv env,
int clsRef,
int argTypesRef) |
int |
JPF_java_lang_Class.getConstructors_____3Ljava_lang_reflect_Constructor_2(MJIEnv env,
int objref) |
int |
JPF_gov_nasa_jpf_CachedROHttpConnection.getContents__Ljava_lang_String_2___3B(MJIEnv env,
int objRef,
int surlRef) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getCounter__I__I(MJIEnv env,
int clsObjRef,
int counterId) |
int |
JPF_java_lang_reflect_Field.getDeclaredAnnotations_____3Ljava_lang_annotation_Annotation_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_reflect_Constructor.getDeclaredAnnotations_____3Ljava_lang_annotation_Annotation_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_Class.getDeclaredAnnotations_____3Ljava_lang_annotation_Annotation_2(MJIEnv env,
int robj) |
int |
JPF_java_lang_reflect_Method.getDeclaredAnnotations_____3Ljava_lang_annotation_Annotation_2(MJIEnv env,
int mthRef) |
int |
JPF_java_lang_Class.getDeclaredClasses(MJIEnv env,
int clsRef) |
int |
JPF_java_lang_Class.getDeclaredConstructor___3Ljava_lang_Class_2__Ljava_lang_reflect_Constructor_2(MJIEnv env,
int clsRef,
int argTypesRef) |
int |
JPF_java_lang_Class.getDeclaredConstructors_____3Ljava_lang_reflect_Constructor_2(MJIEnv env,
int objref) |
int |
JPF_java_lang_Class.getDeclaredField__Ljava_lang_String_2__Ljava_lang_reflect_Field_2(MJIEnv env,
int clsRef,
int nameRef) |
int |
JPF_java_lang_Class.getDeclaredFields_____3Ljava_lang_reflect_Field_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_Class.getDeclaredMethod__Ljava_lang_String_2_3Ljava_lang_Class_2__Ljava_lang_reflect_Method_2(MJIEnv env,
int clsRef,
int nameRef,
int argTypesRef) |
int |
JPF_java_lang_Class.getDeclaredMethods_____3Ljava_lang_reflect_Method_2(MJIEnv env,
int objref) |
int |
JPF_java_io_ObjectStreamClass.getDeclaredSUID__Ljava_lang_Class_2__Ljava_lang_Long_2(MJIEnv env,
int objRef,
int clsRef) |
int |
JPF_java_lang_reflect_Field.getDeclaringClass____Ljava_lang_Class_2(MJIEnv env,
int objref) |
int |
JPF_java_lang_reflect_Constructor.getDeclaringClass____Ljava_lang_Class_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_Class.getDeclaringClass____Ljava_lang_Class_2(MJIEnv env,
int clsRef) |
int |
JPF_java_lang_reflect_Method.getDeclaringClass____Ljava_lang_Class_2(MJIEnv env,
int objRef) |
int |
JPF_java_util_Locale.getDisplayCountry__Ljava_util_Locale_2__Ljava_lang_String_2(MJIEnv env,
int objref,
int locref) |
int |
JPF_java_util_Locale.getDisplayLanguage__Ljava_util_Locale_2__Ljava_lang_String_2(MJIEnv env,
int objref,
int locref) |
int |
JPF_java_util_Locale.getDisplayName__Ljava_util_Locale_2__Ljava_lang_String_2(MJIEnv env,
int objref,
int locref) |
int |
JPF_java_util_TimeZone.getDisplayName__ZILjava_util_Locale_2__Ljava_lang_String_2(MJIEnv env,
int objRef,
boolean daylight,
int style,
int localeRef) |
int |
JPF_java_util_Locale.getDisplayVariant__Ljava_util_Locale_2__Ljava_lang_String_2(MJIEnv env,
int objref,
int locref) |
double |
JPF_java_lang_reflect_Field.getDouble__Ljava_lang_Object_2__D(MJIEnv env,
int objRef,
int fobjRef) |
double |
JPF_java_lang_reflect_Array.getDouble__Ljava_lang_Object_2I__D(MJIEnv env,
int clsRef,
int aref,
int index) |
double |
JPF_sun_misc_Unsafe.getDouble__Ljava_lang_Object_2J__D(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
static double |
JPF_gov_nasa_jpf_vm_Verify.getDouble__Ljava_lang_String_2__D(MJIEnv env,
int clsObjRef,
int idRef) |
static double |
JPF_gov_nasa_jpf_vm_Verify.getDoubleFromList___3D__D(MJIEnv env,
int clsObjRef,
int valArrayRef) |
static double |
JPF_gov_nasa_jpf_vm_Verify.getDoubleFromList(MJIEnv env,
double[] values) |
double |
JPF_sun_misc_Unsafe.getDoubleVolatile__Ljava_lang_Object_2J__D(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
int |
JPF_java_util_TimeZone.getDSTSavings____I(MJIEnv env,
int objRef) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getElementAttribute__Ljava_lang_Object_2I__I(MJIEnv env,
int clsRef,
int oRef,
int idx) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getElementAttributes__Ljava_lang_Object_2I___3I(MJIEnv env,
int clsRef,
int oRef,
int idx) |
int |
JPF_java_lang_Class.getEnclosingClass____Ljava_lang_Class_2(MJIEnv env,
int clsRef) |
int |
JPF_java_lang_Class.getEnclosingConstructor____Ljava_lang_reflect_Constructor_2(MJIEnv env,
int robj) |
int |
JPF_java_lang_Class.getEnclosingMethod____Ljava_lang_reflect_Method_2(MJIEnv env,
int robj) |
int |
JPF_java_lang_Class.getEnumConstants(MJIEnv env,
int clsRef) |
int |
JPF_java_lang_System.getenv__Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int clsObjRef,
int keyRef) |
int |
JPF_java_lang_reflect_Method.getExceptionTypes_____3Ljava_lang_Class_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_Class.getField__Ljava_lang_String_2__Ljava_lang_reflect_Field_2(MJIEnv env,
int clsRef,
int nameRef) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2__I(MJIEnv env,
int clsRef,
int oRef,
int fnRef) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getFieldAttributes__Ljava_lang_Object_2Ljava_lang_String_2___3I(MJIEnv env,
int clsRef,
int oRef,
int fnRef) |
int |
JPF_java_lang_Class.getFields_____3Ljava_lang_reflect_Field_2(MJIEnv env,
int clsRef) |
float |
JPF_java_lang_reflect_Field.getFloat__Ljava_lang_Object_2__F(MJIEnv env,
int objRef,
int fobjRef) |
float |
JPF_java_lang_reflect_Array.getFloat__Ljava_lang_Object_2I__F(MJIEnv env,
int clsRef,
int aref,
int index) |
float |
JPF_sun_misc_Unsafe.getFloat__Ljava_lang_Object_2J__F(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
static float |
JPF_gov_nasa_jpf_vm_Verify.getFloatFromList___3F__F(MJIEnv env,
int clsObjRef,
int valArrayRef) |
static float |
JPF_gov_nasa_jpf_vm_Verify.getFloatFromList(MJIEnv env,
float[] values) |
float |
JPF_sun_misc_Unsafe.getFloatVolatile__Ljava_lang_Object_2J__F(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
long |
JPF_java_lang_Thread.getId____J(MJIEnv env,
int objref) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getInt__II__I(MJIEnv env,
int clsObjRef,
int min,
int max) |
int |
JPF_sun_misc_Unsafe.getInt__J__I(MJIEnv env,
int unsafeRef,
long address) |
int |
JPF_java_lang_reflect_Field.getInt__Ljava_lang_Object_2__I(MJIEnv env,
int objRef,
int fobjRef) |
int |
JPF_java_lang_reflect_Array.getInt__Ljava_lang_Object_2I__I(MJIEnv env,
int clsRef,
int aref,
int index) |
int |
JPF_sun_misc_Unsafe.getInt__Ljava_lang_Object_2J__I(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getInt__Ljava_lang_String_2__I(MJIEnv env,
int clsObjRef,
int idRef) |
int |
JPF_java_lang_Class.getInterfaces_____3Ljava_lang_Class_2(MJIEnv env,
int clsRef) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getIntFromList___3I__I(MJIEnv env,
int clsObjRef,
int valArrayRef) |
int |
JPF_sun_misc_Unsafe.getIntVolatile__Ljava_lang_Object_2J__I(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
int |
JPF_java_util_Locale.getISO3Country____Ljava_lang_String_2(MJIEnv env,
int objref) |
int |
JPF_java_util_Locale.getISO3Language____Ljava_lang_String_2(MJIEnv env,
int objref) |
int |
JPF_java_util_Locale.getISOCountries_____3Ljava_lang_String_2(MJIEnv env,
int clsref) |
int |
JPF_java_util_Locale.getISOLanguages_____3Ljava_lang_String_2(MJIEnv env,
int clsref) |
int |
JPF_java_lang_System.getKeyValuePairs_____3Ljava_lang_String_2(MJIEnv env,
int clsObjRef) |
int |
JPF_java_lang_reflect_Array.getLength__Ljava_lang_Object_2__I(MJIEnv env,
int clsObjRef,
int objRef) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getLocalAttribute__Ljava_lang_String_2__I(MJIEnv env,
int clsRef,
int varRef) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getLocalAttributes__Ljava_lang_String_2___3I(MJIEnv env,
int clsRef,
int varRef) |
int |
JPF_java_util_logging_Level.getLocalizedName____Ljava_lang_String_2(MJIEnv env,
int objRef) |
long |
JPF_sun_misc_Unsafe.getLong__J__J(MJIEnv env,
int unsafeRef,
long address) |
long |
JPF_java_lang_reflect_Field.getLong__Ljava_lang_Object_2__J(MJIEnv env,
int objRef,
int fobjRef) |
long |
JPF_java_lang_reflect_Array.getLong__Ljava_lang_Object_2I__J(MJIEnv env,
int clsRef,
int aref,
int index) |
long |
JPF_sun_misc_Unsafe.getLong__Ljava_lang_Object_2J__J(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
static long |
JPF_gov_nasa_jpf_vm_Verify.getLongFromList___3J__J(MJIEnv env,
int clsObjRef,
int valArrayRef) |
long |
JPF_sun_misc_Unsafe.getLongVolatile__Ljava_lang_Object_2J__J(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
int |
JPF_java_lang_Class.getMethod__Ljava_lang_String_2_3Ljava_lang_Class_2__Ljava_lang_reflect_Method_2(MJIEnv env,
int clsRef,
int nameRef,
int argTypesRef) |
static MethodInfo |
JPF_java_lang_reflect_Method.getMethodInfo(MJIEnv env,
int objRef) |
int |
JPF_java_lang_Class.getMethods_____3Ljava_lang_reflect_Method_2(MJIEnv env,
int objref) |
int |
JPF_java_lang_reflect_Field.getModifiers____I(MJIEnv env,
int objRef) |
int |
JPF_java_lang_reflect_Constructor.getModifiers____I(MJIEnv env,
int objRef) |
int |
JPF_java_lang_Class.getModifiers____I(MJIEnv env,
int clsRef) |
int |
JPF_java_lang_reflect_Method.getModifiers____I(MJIEnv env,
int objRef) |
int |
JPF_java_lang_reflect_Field.getName____Ljava_lang_String_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_reflect_Constructor.getName____Ljava_lang_String_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_reflect_Method.getName____Ljava_lang_String_2(MJIEnv env,
int objRef) |
int |
JPF_java_util_concurrent_atomic_AtomicIntegerArray.getNative__I__I(MJIEnv env,
int objRef,
int index) |
long |
JPF_java_util_concurrent_atomic_AtomicLongArray.getNative__I__J(MJIEnv env,
int objRef,
int index) |
int |
JPF_java_util_concurrent_atomic_AtomicReferenceArray.getNative__I__Ljava_lang_Object_2(MJIEnv env,
int objRef,
int index) |
int |
JPF_java_lang_Character.getNumericValue__C__I(MJIEnv env,
int clsObjRef,
char c) |
int |
JPF_sun_misc_Unsafe.getObject__Ljava_lang_Object_2J__Ljava_lang_Object_2(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getObject__Ljava_lang_String_2__Ljava_lang_Object_2(MJIEnv env,
int clsObjRef,
int idRef) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getObjectAttribute__Ljava_lang_Object_2__I(MJIEnv env,
int clsRef,
int oRef) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getObjectAttributes__Ljava_lang_Object_2___3I(MJIEnv env,
int clsRef,
int oRef) |
int |
JPF_sun_misc_Unsafe.getObjectVolatile__Ljava_lang_Object_2J__Ljava_lang_Object_2(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
int |
JPF_java_util_TimeZone.getOffset__IIIIII__I(MJIEnv env,
int objRef,
int era,
int year,
int month,
int day,
int dayOfWeek,
int milliseconds) |
int |
JPF_gov_nasa_jpf_DelegatingTimeZone.getOffset__IIIIII__I(MJIEnv env,
int objRef,
int era,
int year,
int month,
int day,
int dayOfWeek,
int milliseconds) |
int |
JPF_java_util_TimeZone.getOffset__J__I(MJIEnv env,
int objRef,
long date) |
int |
JPF_java_util_TimeZone.getOffsets__J_3I__I(MJIEnv env,
int objRef,
long date,
int offsetsRef) |
int |
JPF_java_lang_ClassLoader.getPackage__Ljava_lang_String_2__Ljava_lang_Package_2(MJIEnv env,
int objRef,
int nameRef) |
int |
JPF_java_lang_ClassLoader.getPackages_____3Ljava_lang_Package_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_reflect_Constructor.getParameterAnnotations_____3_3Ljava_lang_annotation_Annotation_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_reflect_Method.getParameterAnnotations_____3_3Ljava_lang_annotation_Annotation_2(MJIEnv env,
int mthRef) |
int |
JPF_java_lang_reflect_Constructor.getParameterTypes_____3Ljava_lang_Class_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_reflect_Method.getParameterTypes_____3Ljava_lang_Class_2(MJIEnv env,
int objRef) |
int |
JPF_java_io_File.getParentFile____Ljava_io_File_2(MJIEnv env,
int objref) |
int |
JPF_java_lang_Class.getPrimitiveClass__Ljava_lang_String_2__Ljava_lang_Class_2(MJIEnv env,
int rcls,
int stringRef) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getProperty__Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int clsObjRef,
int keyRef) |
int |
JPF_java_lang_Class.getResolvedName__Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int robj,
int resRef)
Append the package name prefix of the class represented by robj, if the name is not
absolute.
|
int |
JPF_java_lang_ClassLoader.getResource0__Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int objRef,
int resRef) |
int |
JPF_java_lang_ClassLoader.getResources0__Ljava_lang_String_2___3Ljava_lang_String_2(MJIEnv env,
int objRef,
int resRef) |
int |
JPF_java_lang_reflect_Method.getReturnType____Ljava_lang_Class_2(MJIEnv env,
int objRef) |
short |
JPF_java_lang_reflect_Field.getShort__Ljava_lang_Object_2__S(MJIEnv env,
int objRef,
int fobjRef) |
short |
JPF_java_lang_reflect_Array.getShort__Ljava_lang_Object_2I__S(MJIEnv env,
int clsRef,
int aref,
int index) |
short |
JPF_sun_misc_Unsafe.getShort__Ljava_lang_Object_2J__S(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
short |
JPF_sun_misc_Unsafe.getShortVolatile__Ljava_lang_Object_2J__S(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset) |
int |
JPF_java_lang_Throwable.getStackTraceAsString____Ljava_lang_String_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_Thread.getState0____I(MJIEnv env,
int objref) |
int |
JPF_java_lang_Class.getSuperclass____Ljava_lang_Class_2(MJIEnv env,
int robj) |
int |
JPF_java_lang_ClassLoader.getSystemClassLoader____Ljava_lang_ClassLoader_2(MJIEnv env,
int clsObjRef) |
int |
JPF_java_util_TimeZone.getTimeZone__Ljava_lang_String_2__Ljava_util_TimeZone_2(MJIEnv env,
int clsObjRef,
int idRef) |
int |
JPF_java_lang_reflect_Field.getType____Ljava_lang_Class_2(MJIEnv env,
int objRef)
>2do> that doesn't take care of class init yet
|
int |
JPF_java_lang_Character.getType__C__I(MJIEnv env,
int clsObjRef,
char c) |
static String |
JPF_gov_nasa_jpf_vm_Verify.getType(int objRef,
MJIEnv env) |
int |
JPF_sun_misc_Unsafe.getUnsafe____Lsun_misc_Unsafe_2(MJIEnv env,
int clsRef) |
int |
JPF_java_io_File.getURISpec____Ljava_lang_String_2(MJIEnv env,
int objref) |
int |
JPF_java_io_File.getURLSpec____Ljava_lang_String_2(MJIEnv env,
int objref) |
static int |
JPF_gov_nasa_jpf_vm_Verify.getValue__Ljava_lang_String_2__I(MJIEnv env,
int clsObjRef,
int keyRef) |
int |
JPF_java_util_regex_Matcher.group__I__Ljava_lang_String_2(MJIEnv env,
int objref,
int i) |
int |
JPF_java_util_regex_Matcher.groupCount____I(MJIEnv env,
int objref) |
boolean |
JPF_java_util_regex_Matcher.hasAnchoringBounds____Z(MJIEnv env,
int objref) |
int |
JPF_java_lang_reflect_Field.hashCode____I(MJIEnv env,
int objRef) |
int |
JPF_java_lang_reflect_Constructor.hashCode____I(MJIEnv env,
int objRef) |
int |
JPF_java_lang_reflect_Method.hashCode____I(MJIEnv env,
int objRef) |
int |
JPF_java_lang_String.hashCode____I(MJIEnv env,
int objref) |
int |
JPF_java_lang_Object.hashCode____I(MJIEnv env,
int objref) |
boolean |
JPF_java_io_ObjectStreamClass.hasStaticInitializer__Ljava_lang_Class_2__Z(MJIEnv env,
int objRef,
int clsRef) |
boolean |
JPF_java_util_regex_Matcher.hasTransparentBounds____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_util_regex_Matcher.hitEnd____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_lang_Thread.holdsLock__Ljava_lang_Object_2__Z(MJIEnv env,
int clsObjRef,
int objref) |
int |
JPF_java_lang_System.identityHashCode__Ljava_lang_Object_2__I(MJIEnv env,
int clsObjRef,
int objref) |
static void |
JPF_gov_nasa_jpf_vm_Verify.ignoreIf__Z__V(MJIEnv env,
int clsObjRef,
boolean cond) |
static int |
JPF_gov_nasa_jpf_vm_Verify.incrementCounter__I__I(MJIEnv env,
int clsObjRef,
int counterId) |
boolean |
JPF_java_util_TimeZone.inDaylightTime__J__Z(MJIEnv env,
int objRef,
long time) |
boolean |
JPF_gov_nasa_jpf_DelegatingTimeZone.inDaylightTime__J__Z(MJIEnv env,
int objRef,
long time) |
int |
JPF_java_lang_String.indexOf__I__I(MJIEnv env,
int objref,
int c) |
int |
JPF_java_lang_String.indexOf__II__I(MJIEnv env,
int objref,
int c,
int fromIndex) |
int |
JPF_java_lang_String.indexOf__Ljava_lang_String_2__I(MJIEnv env,
int objref,
int str) |
int |
JPF_java_lang_String.indexOf__Ljava_lang_String_2I__I(MJIEnv env,
int objref,
int str,
int fromIndex) |
int |
JPF_java_lang_String.init___3BII__Ljava_lang_String_2(MJIEnv env,
int objRef,
int bytesRef,
int offset,
int length) |
int |
JPF_java_lang_String.init___3BIII__Ljava_lang_String_2(MJIEnv env,
int objRef,
int asciiRef,
int hibyte,
int offset,
int count) |
int |
JPF_java_lang_String.init___3BIILjava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int objRef,
int bytesRef,
int offset,
int length,
int charsetNameRef) |
int |
JPF_java_lang_String.init___3CII__Ljava_lang_String_2(MJIEnv env,
int objRef,
int valueRef,
int offset,
int count) |
int |
JPF_java_lang_String.init___3III__Ljava_lang_String_2(MJIEnv env,
int objRef,
int codePointsRef,
int offset,
int count) |
void |
JPF_java_text_DecimalFormat.init0____V(MJIEnv env,
int objref) |
void |
JPF_java_text_SimpleDateFormat.init0____V(MJIEnv env,
int objref) |
void |
JPF_java_text_DecimalFormat.init0__I__V(MJIEnv env,
int objref,
int style) |
void |
JPF_java_text_SimpleDateFormat.init0__II__V(MJIEnv env,
int objref,
int timeStyle,
int dateStyle) |
int |
JPF_java_security_MessageDigest.init0__Ljava_lang_String_2__I(MJIEnv env,
int objRef,
int algRef) |
void |
JPF_java_text_DecimalFormat.init0__Ljava_lang_String_2__V(MJIEnv env,
int objref,
int patternref) |
void |
JPF_java_text_SimpleDateFormat.init0__Ljava_lang_String_2__V(MJIEnv env,
int objref,
int patternref) |
void |
JPF_java_lang_Thread.init0__Ljava_lang_ThreadGroup_2Ljava_lang_Runnable_2Ljava_lang_String_2J__V(MJIEnv env,
int objRef,
int groupRef,
int runnableRef,
int nameRef,
long stackSize)
This method is the common initializer for all Thread ctors, and the only
single location where we can init our ThreadInfo, but it is PRIVATE
|
void |
JPF_sun_misc_VM.initialize____V(MJIEnv env,
int clsObjRef) |
void |
JPF_java_text_DecimalFormatSymbols.initialize__Ljava_util_Locale_2__V(MJIEnv env,
int objRef,
int localeRef) |
void |
JPF_java_text_DateFormatSymbols.initializeData__Ljava_util_Locale_2__V(MJIEnv env,
int objRef,
int localeRef) |
void |
JPF_java_io_ObjectStreamClass.initNative____V(MJIEnv env,
int clsObjRef) |
float |
JPF_java_lang_Float.intBitsToFloat__I__F(MJIEnv env,
int rcls,
int v0) |
static void |
JPF_gov_nasa_jpf_vm_Verify.interesting__Z__V(MJIEnv env,
int clsObjRef,
boolean cond) |
int |
JPF_java_lang_String.intern____Ljava_lang_String_2(MJIEnv env,
int robj) |
void |
JPF_java_lang_Thread.interrupt____V(MJIEnv env,
int objref) |
boolean |
JPF_java_lang_Thread.interrupted____Z(MJIEnv env,
int clsObjRef) |
int |
JPF_java_lang_reflect_Method.invoke__Ljava_lang_Object_2_3Ljava_lang_Object_2__Ljava_lang_Object_2(MJIEnv env,
int mthRef,
int objRef,
int argsRef) |
boolean |
JPF_java_io_File.isAbsolute____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_lang_Thread.isAlive____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_lang_Class.isAnnotation____Z(MJIEnv env,
int clsObjRef) |
boolean |
JPF_java_lang_Class.isAnnotationPresent__Ljava_lang_Class_2__Z(MJIEnv env,
int clsObjRef,
int annoClsObjRef) |
boolean |
JPF_java_lang_Class.isAnonymousClass____Z(MJIEnv env,
int robj) |
boolean |
JPF_java_lang_Class.isArray____Z(MJIEnv env,
int robj) |
boolean |
JPF_java_lang_Class.isAssignableFrom__Ljava_lang_Class_2__Z(MJIEnv env,
int rcls,
int r1) |
static boolean |
JPF_gov_nasa_jpf_vm_Verify.isCalledFromClass__Ljava_lang_String_2__Z(MJIEnv env,
int clsObjRef,
int clsNameRef) |
boolean |
JPF_java_lang_Character.isDefined__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Character.isDigit__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_io_File.isDirectory____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_lang_Class.isEnum____Z(MJIEnv env,
int robj) |
boolean |
JPF_java_io_File.isFile____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_text_DecimalFormat.isGroupingUsed____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_lang_Character.isIdentifierIgnorable__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Double.isInfinite__D__Z(MJIEnv env,
int rcls,
double v) |
boolean |
JPF_java_lang_Float.isInfinite__F__Z(MJIEnv env,
int rcls,
float v) |
boolean |
JPF_java_lang_Class.isInstance__Ljava_lang_Object_2__Z(MJIEnv env,
int robj,
int r1) |
boolean |
JPF_java_lang_Class.isInterface____Z(MJIEnv env,
int robj) |
boolean |
JPF_java_lang_Thread.isInterrupted____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_lang_Character.isISOControl__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Character.isJavaIdentifierPart__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Character.isJavaIdentifierStart__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Character.isJavaLetter__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Character.isJavaLetterOrDigit__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Character.isLetter__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Character.isLetterOrDigit__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Class.isLocalClass____Z(MJIEnv env,
int robj) |
boolean |
JPF_java_lang_Character.isLowerCase__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Class.isMemberClass____Z(MJIEnv env,
int robj) |
boolean |
JPF_java_lang_Double.isNaN__D__Z(MJIEnv env,
int rcls,
double v) |
boolean |
JPF_java_lang_Float.isNaN__F__Z(MJIEnv env,
int rcls,
float v) |
boolean |
JPF_java_text_DecimalFormat.isParseIntegerOnly____Z(MJIEnv env,
int objref) |
static boolean |
JPF_gov_nasa_jpf_vm_Verify.isRunningInJPF____Z(MJIEnv env,
int clsObjRef) |
static boolean |
JPF_gov_nasa_jpf_vm_Verify.isShared__Ljava_lang_Object_2__Z(MJIEnv env,
int clsObjRef,
int objRef) |
boolean |
JPF_java_lang_Character.isSpace__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Character.isSpaceChar__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_reflect_Field.isSynthetic____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_lang_Character.isTitleCase__C__Z(MJIEnv env,
int clsObjRef,
char c) |
static boolean |
JPF_gov_nasa_jpf_vm_Verify.isTraceReplay____Z(MJIEnv env,
int clsObjRef) |
boolean |
JPF_java_lang_Character.isUnicodeIdentifierPart__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Character.isUnicodeIdentifierStart__C__Z(MJIEnv env,
int clsObjRef,
char c) |
protected boolean |
NativeMethodInfo.isUnsatisfiedLinkError(MJIEnv env) |
boolean |
JPF_java_lang_Character.isUpperCase__C__Z(MJIEnv env,
int clsObjRef,
char c) |
boolean |
JPF_java_lang_Character.isWhitespace__C__Z(MJIEnv env,
int clsObjRef,
char c) |
void |
JPF_java_lang_Thread.join____V(MJIEnv env,
int objref) |
void |
JPF_java_lang_Thread.join__J__V(MJIEnv env,
int objref,
long millis) |
void |
JPF_java_lang_Thread.join__JI__V(MJIEnv env,
int objref,
long millis,
int nanos) |
int |
JPF_java_lang_String.lastIndexOf__I__I(MJIEnv env,
int objref,
int c) |
int |
JPF_java_lang_String.lastIndexOf__II__I(MJIEnv env,
int objref,
int c,
int fromIndex) |
int |
JPF_java_lang_String.lastIndexOf__Ljava_lang_String_2I__I(MJIEnv env,
int objref,
int str,
int fromIndex) |
int |
JPF_java_io_ObjectInputStream.latestUserDefinedLoader____Ljava_lang_ClassLoader_2(MJIEnv env,
int clsRef) |
void |
JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.lazySet__Ljava_lang_Object_2I__(MJIEnv env,
int objRef,
int tRef,
int fNewValue) |
void |
JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.lazySet__Ljava_lang_Object_2J__(MJIEnv env,
int objRef,
int tRef,
long fNewValue) |
void |
JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.lazySet__Ljava_lang_Object_2Ljava_lang_Object_2__(MJIEnv env,
int objRef,
int tRef,
int fNewValue) |
long |
JPF_java_io_File.length____J(MJIEnv env,
int objref) |
int |
JPF_java_io_File.list_____3Ljava_lang_String_2(MJIEnv env,
int objref) |
int |
JPF_java_io_File.listRoots_____3Ljava_io_File_2(MJIEnv env,
int classRef) |
double |
JPF_java_lang_Math.log__D__D(MJIEnv env,
int clsObjRef,
double a) |
void |
JPF_gov_nasa_jpf_tools_MethodTester.log__Ljava_lang_String_2__V(MJIEnv env,
int objRef,
int msgRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.log__Ljava_lang_String_2ILjava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int loggerIdRef,
int logLevel,
int msgRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.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 |
JPF_gov_nasa_jpf_vm_Verify.log__Ljava_lang_String_2ILjava_lang_String_2Ljava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int loggerIdRef,
int logLevel,
int arg1Ref,
int arg2Ref) |
double |
JPF_java_lang_Math.log10__D__D(MJIEnv env,
int clsObjRef,
double a) |
double |
JPF_java_lang_Double.longBitsToDouble__J__D(MJIEnv env,
int rcls,
long v0) |
boolean |
JPF_java_util_regex_Matcher.lookingAt____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_util_regex_Matcher.matches____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_lang_String.matches__Ljava_lang_String_2__Z(MJIEnv env,
int objRef,
int regexRef) |
double |
JPF_java_lang_Math.max__DD__D(MJIEnv env,
int clsObjRef,
double a,
double b) |
float |
JPF_java_lang_Math.max__FF__F(MJIEnv env,
int clsObjRef,
float a,
float b) |
int |
JPF_java_lang_Math.max__II__I(MJIEnv env,
int clsObjRef,
int a,
int b) |
long |
JPF_java_lang_Math.max__JJ__J(MJIEnv env,
int clsObjRef,
long a,
long b) |
long |
JPF_java_lang_Runtime.maxMemory____J(MJIEnv env,
int objref) |
double |
JPF_java_lang_Math.min__DD__D(MJIEnv env,
int clsObjRef,
double a,
double b) |
float |
JPF_java_lang_Math.min__FF__F(MJIEnv env,
int clsObjRef,
float a,
float b) |
int |
JPF_java_lang_Math.min__II__I(MJIEnv env,
int clsObjRef,
int a,
int b) |
long |
JPF_java_lang_Math.min__JJ__J(MJIEnv env,
int clsObjRef,
long a,
long b) |
int |
JPF_java_lang_String.MJIcompare__Ljava_lang_String_2Ljava_lang_String_2__I(MJIEnv env,
int clsRef,
int s1Ref,
int s2Ref) |
int |
JPF_java_lang_reflect_Array.multiNewArray__Ljava_lang_Class_2_3I__Ljava_lang_Object_2(MJIEnv env,
int clsRef,
int componentTypeRef,
int dimArrayRef) |
int |
JPF_sun_misc_Hashing.murmur3_32__I_3BII__I(MJIEnv env,
int clsRef,
int seed,
int dataRef,
int offset,
int len) |
int |
JPF_sun_misc_Hashing.murmur3_32__I_3CII__I(MJIEnv env,
int clsRef,
int seed,
int dataRef,
int offset,
int len) |
int |
JPF_sun_misc_Hashing.murmur3_32__I_3III__I(MJIEnv env,
int clsRef,
int seed,
int dataRef,
int offset,
int len) |
long |
JPF_java_lang_System.nanoTime____J(MJIEnv env,
int clsObjRef) |
void |
JPF_java_text_Bidi.nativeBidiChars(MJIEnv env,
int clsObjRef,
int bidiRef,
int textRef,
int textStart,
int embeddingsRef,
int embeddingsStart,
int length,
int flags) |
int |
JPF_java_lang_reflect_Array.newArray__Ljava_lang_Class_2I__Ljava_lang_Object_2(MJIEnv env,
int clsRef,
int componentTypeRef,
int length) |
int |
JPF_sun_reflect_ReflectionFactory.newConstructorForSerialization__Ljava_lang_Class_2Ljava_lang_reflect_Constructor_2__Ljava_lang_reflect_Constructor_2(MJIEnv env,
int objRef,
int clsRef,
int ctorRef) |
int |
JPF_java_lang_Class.newInstance____Ljava_lang_Object_2(MJIEnv env,
int robj)
this is an example of a native method issuing direct calls - otherwise known
as a round trip.
|
int |
JPF_java_lang_reflect_Constructor.newInstance___3Ljava_lang_Object_2__Ljava_lang_Object_2(MJIEnv env,
int mthRef,
int argsRef) |
int |
JPF_gov_nasa_jpf_SerializationConstructor.newInstance___3Ljava_lang_Object_2__Ljava_lang_Object_2(MJIEnv env,
int mthRef,
int argsRef)
create a new instance, but only call the ctor of the first
non-serializable superclass
|
int |
JPF_java_util_Random.next__I__I(MJIEnv env,
int objRef,
int nBits) |
boolean |
JPF_java_util_Random.nextBoolean____Z(MJIEnv env,
int objRef) |
void |
JPF_java_util_Random.nextBytes___3B__V(MJIEnv env,
int objRef,
int dataRef) |
double |
JPF_java_util_Random.nextDouble____D(MJIEnv env,
int objRef) |
float |
JPF_java_util_Random.nextFloat____F(MJIEnv env,
int objRef) |
double |
JPF_java_util_Random.nextGaussian____D(MJIEnv env,
int objRef) |
int |
JPF_java_util_Random.nextInt____I(MJIEnv env,
int objRef) |
int |
JPF_java_util_Random.nextInt__I__I(MJIEnv env,
int objRef,
int n) |
long |
JPF_java_util_Random.nextLong____J(MJIEnv env,
int objRef) |
void |
JPF_java_lang_Object.notify____V(MJIEnv env,
int objref) |
void |
JPF_java_lang_Object.notifyAll____V(MJIEnv env,
int objref) |
long |
JPF_sun_misc_Unsafe.objectFieldOffset__Ljava_lang_reflect_Field_2__J(MJIEnv env,
int unsafeRef,
int fieldRef) |
int |
JPF_java_lang_String.offsetByCodePoints__II__I(MJIEnv env,
int objRef,
int index,
int codePointOffset) |
int |
JPF_java_io_FileDescriptor.open__Ljava_lang_String_2I__I(MJIEnv env,
int objref,
int fnameRef,
int mode) |
void |
JPF_sun_misc_Unsafe.park__ZJ__V(MJIEnv env,
int unsafeRef,
boolean isAbsoluteTime,
long timeout) |
int |
JPF_java_text_DateFormat.parse__Ljava_lang_String_2__Ljava_util_Date_2(MJIEnv env,
int objref,
int strRef) |
int |
JPF_java_text_DecimalFormat.parse__Ljava_lang_String_2Ljava_text_ParsePosition_2__Ljava_lang_Number_2(MJIEnv env,
int objref,
int sourceRef,
int parsePositionRef) |
int |
JPF_java_lang_Integer.parseInt__Ljava_lang_String_2__I(MJIEnv env,
int clsObjRef,
int strRef) |
int |
JPF_java_lang_Integer.parseInt__Ljava_lang_String_2I__I(MJIEnv env,
int clsObjRef,
int strRef,
int radix) |
long |
JPF_java_lang_Long.parseLong__Ljava_lang_String_2__J(MJIEnv env,
int clsObjRef,
int strRef) |
long |
JPF_java_lang_Long.parseLong__Ljava_lang_String_2I__J(MJIEnv env,
int clsObjRef,
int strRef,
int radix) |
short |
JPF_java_lang_Short.parseShort__Ljava_lang_String_2__S(MJIEnv env,
int clsObjRef,
int strRef) |
short |
JPF_java_lang_Short.parseShort__Ljava_lang_String_2I__S(MJIEnv env,
int clsObjRef,
int strRef,
int radix) |
boolean |
JPF_gov_nasa_jpf_test_MemoryGoal.postCheck__Lgov_nasa_jpf_test_TestContext_2Ljava_lang_reflect_Method_2Ljava_lang_Object_2Ljava_lang_Throwable_2__Z(MJIEnv env,
int objRef,
int testContextRef,
int methdRef,
int resultRef,
int exRef) |
double |
JPF_java_lang_Math.pow__DD__D(MJIEnv env,
int clsObjRef,
double a,
double b) |
boolean |
JPF_gov_nasa_jpf_test_MemoryGoal.preCheck__Lgov_nasa_jpf_test_TestContext_2Ljava_lang_reflect_Method_2__Z(MJIEnv env,
int objRef,
int testContextRef,
int methodRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.print___3Ljava_lang_String_2__V(MJIEnv env,
int clsRef,
int argsRef) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.print__C__V(MJIEnv env,
int objref,
char c) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.print__D__V(MJIEnv env,
int objref,
double d) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.print__F__V(MJIEnv env,
int objref,
float f) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.print__I__V(MJIEnv env,
int objref,
int i) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.print__J__V(MJIEnv env,
int objref,
long j) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.print__Ljava_lang_String_2__V(MJIEnv env,
int objRef,
int strRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.print__Ljava_lang_String_2__V(MJIEnv env,
int clsRef,
int sRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.print__Ljava_lang_String_2I__V(MJIEnv env,
int clsRef,
int sRef,
int val) |
static void |
JPF_gov_nasa_jpf_vm_Verify.print__Ljava_lang_String_2Z__V(MJIEnv env,
int clsRef,
int sRef,
boolean val) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.print__Z__V(MJIEnv env,
int objref,
boolean z) |
int |
JPF_gov_nasa_jpf_ConsoleOutputStream.printf__Ljava_lang_String_2_3Ljava_lang_Object_2__Ljava_io_PrintStream_2(MJIEnv env,
int objref,
int fmtRef,
int argRef) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.println____V(MJIEnv env,
int objRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.println____V(MJIEnv env,
int clsRef) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.println__C__V(MJIEnv env,
int objref,
char c) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.println__D__V(MJIEnv env,
int objref,
double d) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.println__F__V(MJIEnv env,
int objref,
float f) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.println__I__V(MJIEnv env,
int objref,
int i) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.println__J__V(MJIEnv env,
int objref,
long j) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.println__Ljava_lang_String_2__V(MJIEnv env,
int objRef,
int strRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.println__Ljava_lang_String_2__V(MJIEnv env,
int clsRef,
int sRef) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.println__Z__V(MJIEnv env,
int objref,
boolean z) |
static void |
JPF_gov_nasa_jpf_vm_Verify.printPathOutput__Ljava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int msgRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.printPathOutput__ZLjava_lang_String_2__V(MJIEnv env,
int clsObjRef,
boolean cond,
int msgRef) |
void |
JPF_java_lang_Throwable.printStackTrace____V(MJIEnv env,
int objRef) |
void |
JPF_sun_misc_Unsafe.putBoolean__Ljava_lang_Object_2JZ__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
boolean val) |
void |
JPF_sun_misc_Unsafe.putBooleanVolatile__Ljava_lang_Object_2JZ__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
boolean val) |
void |
JPF_sun_misc_Unsafe.putByte__JB__V(MJIEnv env,
int unsafeRef,
long address,
byte val) |
void |
JPF_sun_misc_Unsafe.putByte__Ljava_lang_Object_2JB__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
byte val) |
void |
JPF_sun_misc_Unsafe.putByteVolatile__Ljava_lang_Object_2JB__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
byte val) |
void |
JPF_sun_misc_Unsafe.putChar__JC__V(MJIEnv env,
int unsafeRef,
long address,
char val) |
void |
JPF_sun_misc_Unsafe.putChar__Ljava_lang_Object_2JC__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
char val) |
void |
JPF_sun_misc_Unsafe.putCharVolatile__Ljava_lang_Object_2JC__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
char val) |
void |
JPF_sun_misc_Unsafe.putDouble__Ljava_lang_Object_2JD__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
double val) |
void |
JPF_sun_misc_Unsafe.putDoubleVolatile__Ljava_lang_Object_2JD__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
double val) |
void |
JPF_sun_misc_Unsafe.putFloat__Ljava_lang_Object_2JF__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
float val) |
void |
JPF_sun_misc_Unsafe.putFloatVolatile__Ljava_lang_Object_2JF__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
float val) |
void |
JPF_sun_misc_Unsafe.putInt__JI__V(MJIEnv env,
int unsafeRef,
long address,
int val) |
void |
JPF_sun_misc_Unsafe.putInt__Ljava_lang_Object_2JI__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
int val) |
void |
JPF_sun_misc_Unsafe.putIntVolatile__Ljava_lang_Object_2JI__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
int val) |
void |
JPF_sun_misc_Unsafe.putLong__JJ__V(MJIEnv env,
int unsafeRef,
long address,
long val) |
void |
JPF_sun_misc_Unsafe.putLong__Ljava_lang_Object_2JJ__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
long val) |
void |
JPF_sun_misc_Unsafe.putLongVolatile__Ljava_lang_Object_2JJ__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
long val) |
void |
JPF_sun_misc_Unsafe.putObject__Ljava_lang_Object_2JLjava_lang_Object_2__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
int valRef) |
void |
JPF_sun_misc_Unsafe.putObjectVolatile__Ljava_lang_Object_2JLjava_lang_Object_2__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
int valRef) |
void |
JPF_sun_misc_Unsafe.putOrderedInt__Ljava_lang_Object_2JI__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
int val) |
void |
JPF_sun_misc_Unsafe.putOrderedLong__Ljava_lang_Object_2JJ__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
long val) |
void |
JPF_sun_misc_Unsafe.putOrderedObject__Ljava_lang_Object_2JLjava_lang_Object_2__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
int valRef) |
void |
JPF_sun_misc_Unsafe.putShort__Ljava_lang_Object_2JS__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
short val) |
void |
JPF_sun_misc_Unsafe.putShortVolatile__Ljava_lang_Object_2JS__V(MJIEnv env,
int unsafeRef,
int objRef,
long fieldOffset,
short val) |
static void |
JPF_gov_nasa_jpf_vm_Verify.putValue__Ljava_lang_String_2I__V(MJIEnv env,
int clsObjRef,
int keyRef,
int val) |
int |
JPF_java_util_regex_Matcher.quoteReplacement__Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int clsObjref,
int string) |
double |
JPF_java_lang_Math.random____D(MJIEnv env,
int clsObjRef) |
static int |
JPF_gov_nasa_jpf_vm_Verify.random__I__I(MJIEnv env,
int clsObjRef,
int x)
deprecated, use getInt
|
static boolean |
JPF_gov_nasa_jpf_vm_Verify.randomBool(MJIEnv env,
int clsObjRef)
deprecated, use getBoolean()
|
int |
JPF_sun_misc_Hashing.randomHashSeed__Ljava_lang_Object_2__I(MJIEnv env,
int clsRef,
int objRef) |
int |
JPF_java_io_FileDescriptor.read____I(MJIEnv env,
int objref) |
int |
JPF_java_io_RandomAccessFile.read___3BII__I(MJIEnv env,
int this_ptr,
int data_array,
int start,
int len) |
int |
JPF_java_io_FileDescriptor.read___3BII__I(MJIEnv env,
int objref,
int bufref,
int offset,
int len) |
byte |
JPF_java_io_RandomAccessFile.readByte____B(MJIEnv env,
int this_ptr) |
static int |
JPF_gov_nasa_jpf_vm_Verify.readObjectFromFile__Ljava_lang_Class_2Ljava_lang_String_2__Ljava_lang_Object_2(MJIEnv env,
int clsObjRef,
int newObjClsRef,
int fileNameRef) |
int |
JPF_java_util_regex_Matcher.region__II__Ljava_util_regex_Matcher_2(MJIEnv env,
int objref,
int start,
int end) |
int |
JPF_java_util_regex_Matcher.regionEnd____I(MJIEnv env,
int objref) |
boolean |
JPF_java_lang_String.regionMatches__ILjava_lang_String_2II__Z(MJIEnv env,
int objRef,
int toffset,
int otherRef,
int ooffset,
int len) |
boolean |
JPF_java_lang_String.regionMatches__ZILjava_lang_String_2II__Z(MJIEnv env,
int objRef,
boolean ignoreCase,
int toffset,
int otherRef,
int ooffset,
int len) |
int |
JPF_java_util_regex_Matcher.regionStart____I(MJIEnv env,
int objref) |
void |
JPF_java_util_regex_Matcher.register____V(MJIEnv env,
int objref) |
int |
JPF_java_lang_String.replace__CC__Ljava_lang_String_2(MJIEnv env,
int objRef,
char oldChar,
char newChar) |
int |
JPF_java_util_regex_Matcher.replaceAll__Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int objref,
int string) |
int |
JPF_java_lang_String.replaceAll__Ljava_lang_String_2Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int objRef,
int regexRef,
int replacementRef) |
int |
JPF_java_util_regex_Matcher.replaceFirst__Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int objref,
int string) |
int |
JPF_java_lang_String.replaceFirst__Ljava_lang_String_2Ljava_lang_String_2__Ljava_lang_String_2(MJIEnv env,
int objRef,
int regexRef,
int replacementRef) |
boolean |
JPF_java_util_regex_Matcher.requireEnd____Z(MJIEnv env,
int objref) |
boolean |
JPF_java_text_Bidi.requiresBidi(MJIEnv env,
int clsObjRef,
int textRef,
int start,
int limit) |
int |
JPF_java_util_regex_Matcher.reset____Ljava_util_regex_Matcher_2(MJIEnv env,
int objref) |
static void |
JPF_gov_nasa_jpf_vm_Verify.resetCounter__I__V(MJIEnv env,
int clsObjRef,
int counterId) |
void |
JPF_java_lang_Thread.resume____(MJIEnv env,
int threadObjRef) |
double |
JPF_java_lang_Math.rint__D__D(MJIEnv env,
int clsObjRef,
double a) |
long |
JPF_java_lang_Math.round__D__J(MJIEnv env,
int clsObjRef,
double a) |
void |
JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.set__Ljava_lang_Object_2I__(MJIEnv env,
int objRef,
int tRef,
int fNewValue) |
void |
JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.set__Ljava_lang_Object_2J__(MJIEnv env,
int objRef,
int tRef,
long fNewValue) |
void |
JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.set__Ljava_lang_Object_2Ljava_lang_Object_2__(MJIEnv env,
int objRef,
int tRef,
int fNewValue) |
void |
JPF_java_lang_reflect_Field.set__Ljava_lang_Object_2Ljava_lang_Object_2__V(MJIEnv env,
int objRef,
int fobjRef,
int val)
Peer method for the
java.lang.reflect.Field.set method. |
static void |
JPF_gov_nasa_jpf_vm_Verify.setBitInBitSet__IIZ__V(MJIEnv env,
int clsObjRef,
int id,
int bitNum,
boolean value) |
void |
JPF_java_lang_reflect_Array.setBoolean__Ljava_lang_Object_2IZ__V(MJIEnv env,
int clsRef,
int aref,
int index,
boolean val) |
void |
JPF_java_lang_reflect_Field.setBoolean__Ljava_lang_Object_2Z__V(MJIEnv env,
int objRef,
int fobjRef,
boolean val) |
void |
JPF_java_lang_reflect_Field.setByte__Ljava_lang_Object_2B__V(MJIEnv env,
int objRef,
int fobjRef,
byte val) |
void |
JPF_java_lang_reflect_Array.setByte__Ljava_lang_Object_2IB__V(MJIEnv env,
int clsRef,
int aref,
int index,
byte val) |
void |
JPF_java_lang_reflect_Field.setChar__Ljava_lang_Object_2C__V(MJIEnv env,
int objRef,
int fobjRef,
char val) |
void |
JPF_java_lang_reflect_Array.setChar__Ljava_lang_Object_2IC__V(MJIEnv env,
int clsRef,
int aref,
int index,
char val) |
void |
JPF_java_lang_ClassLoader.setClassAssertionStatus__Ljava_lang_String_2Z__V(MJIEnv env,
int objRef,
int strRef,
boolean enabled) |
static void |
JPF_gov_nasa_jpf_vm_Verify.setCounter__II__V(MJIEnv env,
int clsObjRef,
int counterId,
int val) |
void |
JPF_java_lang_Thread.setDaemon0__Z__V(MJIEnv env,
int objref,
boolean isDaemon) |
void |
JPF_java_io_RandomAccessFile.setDataMap____V(MJIEnv env,
int this_ptr) |
void |
JPF_java_lang_ClassLoader.setDefaultAssertionStatus__Z__V(MJIEnv env,
int objRef,
boolean enabled) |
void |
JPF_java_util_TimeZone.setDefaultValues__Ljava_util_TimeZone_2(MJIEnv env,
int clsObjRef,
int tzRef) |
void |
JPF_java_lang_reflect_Field.setDouble__Ljava_lang_Object_2D__V(MJIEnv env,
int objRef,
int fobjRef,
double val) |
void |
JPF_java_lang_reflect_Array.setDouble__Ljava_lang_Object_2ID__V(MJIEnv env,
int clsRef,
int aref,
int index,
double val) |
static void |
JPF_gov_nasa_jpf_vm_Verify.setElementAttribute__Ljava_lang_Object_2II__V(MJIEnv env,
int clsRef,
int oRef,
int idx,
int attr) |
static void |
JPF_gov_nasa_jpf_vm_Verify.setFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2I__V(MJIEnv env,
int clsRef,
int oRef,
int fnRef,
int attr) |
void |
JPF_java_lang_reflect_Field.setFloat__Ljava_lang_Object_2F__V(MJIEnv env,
int objRef,
int fobjRef,
float val) |
void |
JPF_java_lang_reflect_Array.setFloat__Ljava_lang_Object_2IF__V(MJIEnv env,
int clsRef,
int aref,
int index,
float val) |
void |
JPF_java_text_DecimalFormat.setGroupingUsed__Z__V(MJIEnv env,
int objref,
boolean newValue) |
void |
JPF_java_util_TimeZone.setID__Ljava_lang_String_2__V(MJIEnv env,
int objRef,
int idRef) |
void |
JPF_gov_nasa_jpf_DelegatingTimeZone.setID__Ljava_lang_String_2__V(MJIEnv env,
int objRef,
int idRef) |
void |
JPF_java_lang_reflect_Field.setInt__Ljava_lang_Object_2I__V(MJIEnv env,
int objRef,
int fobjRef,
int val) |
void |
JPF_java_lang_reflect_Array.setInt__Ljava_lang_Object_2II__V(MJIEnv env,
int clsRef,
int aref,
int index,
int val) |
void |
JPF_java_io_RandomAccessFile.setLength__J__V(MJIEnv env,
int this_ptr,
long len) |
void |
JPF_java_text_DateFormat.setLenient__Z__V(MJIEnv env,
int objref,
boolean isLenient) |
static void |
JPF_gov_nasa_jpf_vm_Verify.setLocalAttribute__Ljava_lang_String_2I__V(MJIEnv env,
int clsRef,
int varRef,
int attr) |
void |
JPF_java_lang_reflect_Array.setLong__Ljava_lang_Object_2IJ__V(MJIEnv env,
int clsRef,
int aref,
int index,
long val) |
void |
JPF_java_lang_reflect_Field.setLong__Ljava_lang_Object_2J__V(MJIEnv env,
int objRef,
int fobjRef,
long val) |
void |
JPF_java_text_DecimalFormat.setMaximumFractionDigits__I__V(MJIEnv env,
int objref,
int newValue) |
void |
JPF_java_text_DecimalFormat.setMaximumIntegerDigits__I__V(MJIEnv env,
int objref,
int newValue) |
void |
JPF_java_text_DecimalFormat.setMinimumFractionDigits__I__V(MJIEnv env,
int objref,
int newValue) |
void |
JPF_java_text_DecimalFormat.setMinimumIntegerDigits__I__V(MJIEnv env,
int objref,
int newValue) |
void |
JPF_java_lang_Thread.setName0__Ljava_lang_String_2__V(MJIEnv env,
int objref,
int nameRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.setObjectAttribute__Ljava_lang_Object_2I__V(MJIEnv env,
int clsRef,
int oRef,
int attr) |
void |
JPF_java_lang_ClassLoader.setPackageAssertionStatus__Ljava_lang_String_2Z__V(MJIEnv env,
int objRef,
int strRef,
boolean enabled) |
void |
JPF_java_text_DecimalFormat.setParseIntegerOnly__Z__V(MJIEnv env,
int objref,
boolean value) |
void |
JPF_java_lang_Thread.setPriority0__I__V(MJIEnv env,
int objref,
int prio) |
static void |
JPF_gov_nasa_jpf_vm_Verify.setProperties___3Ljava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int argRef) |
void |
JPF_java_util_Random.setSeed__J__V(MJIEnv env,
int objRef,
long seedStarter) |
static void |
JPF_gov_nasa_jpf_vm_Verify.setShared__Ljava_lang_Object_2Z__V(MJIEnv env,
int clsObjRef,
int objRef,
boolean isShared) |
void |
JPF_java_lang_reflect_Array.setShort__Ljava_lang_Object_2IS__V(MJIEnv env,
int clsRef,
int aref,
int index,
short val) |
void |
JPF_java_lang_reflect_Field.setShort__Ljava_lang_Object_2S__V(MJIEnv env,
int objRef,
int fobjRef,
short val) |
void |
JPF_java_text_DateFormat.setTimeZone__Ljava_util_TimeZone_2__V(MJIEnv env,
int objref,
int timeZoneRef) |
void |
JPF_java_util_Calendar.setWeekCountData__Ljava_util_Locale_2__(MJIEnv env,
int objref,
int localeRef) |
double |
JPF_java_lang_Math.sin__D__D(MJIEnv env,
int clsObjRef,
double a) |
long |
JPF_java_io_FileDescriptor.skip__J__J(MJIEnv env,
int objref,
long nBytes) |
void |
JPF_java_lang_Thread.sleep__JI__V(MJIEnv env,
int clsObjRef,
long millis,
int nanos) |
int |
JPF_java_lang_String.split__Ljava_lang_String_2___3Ljava_lang_String_2(MJIEnv env,
int clsObjRef,
int strRef) |
int |
JPF_java_lang_String.split__Ljava_lang_String_2I___3Ljava_lang_String_2(MJIEnv env,
int clsObjRef,
int strRef,
int limit) |
int |
JPF_java_util_regex_Pattern.split0__Ljava_lang_String_2I___3Ljava_lang_String_2(MJIEnv env,
int patRef,
int strRef,
int limit) |
double |
JPF_java_lang_Math.sqrt__D__D(MJIEnv env,
int clsObjRef,
double a) |
void |
JPF_java_lang_Thread.start____V(MJIEnv env,
int objref) |
int |
JPF_java_util_regex_Matcher.start__I__I(MJIEnv env,
int objref,
int group) |
boolean |
JPF_java_lang_String.startsWith__Ljava_lang_String_2__Z(MJIEnv env,
int objRef,
int prefixRef) |
boolean |
JPF_java_lang_String.startsWith__Ljava_lang_String_2I__Z(MJIEnv env,
int objRef,
int prefixRef,
int toffset) |
void |
JPF_java_lang_Thread.stop____V(MJIEnv env,
int threadRef) |
void |
JPF_java_lang_Thread.stop__Ljava_lang_Throwable_2__V(MJIEnv env,
int threadRef,
int throwableRef) |
static void |
JPF_gov_nasa_jpf_vm_Verify.storeTrace__Ljava_lang_String_2Ljava_lang_String_2__V(MJIEnv env,
int clsObjRef,
int filenameRef,
int commentRef) |
int |
JPF_sun_misc_Hashing.stringHash32__Ljava_lang_String_2__I(MJIEnv env,
int clsRef,
int sRef) |
int |
JPF_java_lang_String.substring__I__Ljava_lang_String_2(MJIEnv env,
int objRef,
int beginIndex) |
int |
JPF_java_lang_String.substring__II__Ljava_lang_String_2(MJIEnv env,
int objRef,
int beginIndex,
int endIndex) |
void |
JPF_java_lang_Thread.suspend____(MJIEnv env,
int threadObjRef) |
void |
JPF_java_io_FileDescriptor.sync____(MJIEnv env,
int objref) |
double |
JPF_java_lang_Math.tan__D__D(MJIEnv env,
int clsObjRef,
double a) |
static void |
JPF_gov_nasa_jpf_vm_Verify.terminateSearch____V(MJIEnv env,
int clsObjRef) |
int |
JPF_java_lang_Integer.toBinaryString__I__Ljava_lang_String_2(MJIEnv env,
int objref,
int val) |
int |
JPF_java_lang_Long.toBinaryString__J__Ljava_lang_String_2(MJIEnv env,
int objref,
long val) |
int |
JPF_java_lang_String.toCharArray_____3C(MJIEnv env,
int objref) |
int |
JPF_java_lang_Integer.toHexString__I__Ljava_lang_String_2(MJIEnv env,
int objref,
int val) |
int |
JPF_java_lang_Long.toHexString__J__Ljava_lang_String_2(MJIEnv env,
int objref,
long val) |
int |
JPF_java_lang_String.toLowerCase____Ljava_lang_String_2(MJIEnv env,
int objRef) |
char |
JPF_java_lang_Character.toLowerCase__C__C(MJIEnv env,
int clsObjRef,
char c) |
int |
JPF_java_lang_String.toLowerCase__Ljava_util_Locale_2__Ljava_lang_String_2(MJIEnv env,
int objRef,
int locRef) |
int |
JPF_java_lang_Integer.toOctalString__I__Ljava_lang_String_2(MJIEnv env,
int objref,
int val) |
int |
JPF_java_lang_Long.toOctalString__J__Ljava_lang_String_2(MJIEnv env,
int objref,
long val) |
int |
JPF_java_lang_reflect_Field.toString____Ljava_lang_String_2(MJIEnv env,
int objRef) |
int |
JPF_gov_nasa_jpf_AnnotationProxyBase.toString____Ljava_lang_String_2(MJIEnv env,
int objref) |
int |
JPF_java_lang_reflect_Constructor.toString____Ljava_lang_String_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_Throwable.toString____Ljava_lang_String_2(MJIEnv env,
int objRef) |
int |
JPF_java_util_regex_Matcher.toString____Ljava_lang_String_2(MJIEnv env,
int objref) |
int |
JPF_java_util_Date.toString____Ljava_lang_String_2(MJIEnv env,
int dateRef) |
int |
JPF_java_lang_reflect_Method.toString____Ljava_lang_String_2(MJIEnv env,
int objRef) |
int |
JPF_java_lang_StringBuilder.toString____Ljava_lang_String_2(MJIEnv env,
int objref) |
int |
JPF_java_lang_Object.toString____Ljava_lang_String_2(MJIEnv env,
int objref) |
int |
JPF_java_lang_Double.toString__D__Ljava_lang_String_2(MJIEnv env,
int objref,
double d) |
int |
JPF_java_lang_Integer.toString__I__Ljava_lang_String_2(MJIEnv env,
int objref,
int val) |
int |
JPF_java_lang_Integer.toString__II__Ljava_lang_String_2(MJIEnv env,
int objref,
int val,
int radix) |
int |
JPF_java_lang_Long.toString__J__Ljava_lang_String_2(MJIEnv env,
int objref,
long val) |
int |
JPF_java_lang_Long.toString__JI__Ljava_lang_String_2(MJIEnv env,
int objref,
long val,
int radix) |
int |
JPF_java_lang_Short.toString__S__Ljava_lang_String_2(MJIEnv env,
int objref,
short val) |
long |
JPF_java_lang_Runtime.totalMemory____J(MJIEnv env,
int objref) |
char |
JPF_java_lang_Character.toTitleCase__C__C(MJIEnv env,
int clsObjRef,
char c) |
int |
JPF_java_lang_String.toUpperCase____Ljava_lang_String_2(MJIEnv env,
int objRef) |
char |
JPF_java_lang_Character.toUpperCase__C__C(MJIEnv env,
int clsObjRef,
char c) |
int |
JPF_java_lang_String.toUpperCase__Ljava_util_Locale_2__Ljava_lang_String_2(MJIEnv env,
int objRef,
int locRef) |
int |
JPF_java_lang_String.trim____Ljava_lang_String_2(MJIEnv env,
int objRef) |
void |
JPF_sun_misc_Unsafe.unpark__Ljava_lang_Object_2__V(MJIEnv env,
int unsafeRef,
int objRef) |
int |
JPF_java_util_regex_Matcher.useAnchoringBounds__Z__Ljava_util_regex_Matcher_2(MJIEnv env,
int objref,
boolean b) |
boolean |
JPF_java_util_TimeZone.useDaylightTime____Z(MJIEnv env,
int objRef) |
boolean |
JPF_gov_nasa_jpf_DelegatingTimeZone.useDaylightTime____Z(MJIEnv env,
int objRef) |
int |
JPF_java_util_regex_Matcher.useTransparentBounds__Z__Ljava_util_regex_Matcher_2(MJIEnv env,
int objref,
boolean b) |
int |
JPF_java_lang_Byte.valueOf__B__Ljava_lang_Byte_2(MJIEnv env,
int clsRef,
byte val) |
int |
JPF_java_lang_Character.valueOf__C__Ljava_lang_Character_2(MJIEnv env,
int clsRef,
char val) |
int |
JPF_java_lang_String.valueOf__D__Ljava_lang_String_2(MJIEnv env,
int clsref,
double d) |
int |
JPF_java_lang_String.valueOf__F__Ljava_lang_String_2(MJIEnv env,
int clsref,
float f) |
int |
JPF_java_lang_Integer.valueOf__I__Ljava_lang_Integer_2(MJIEnv env,
int clsRef,
int val) |
int |
JPF_java_lang_String.valueOf__I__Ljava_lang_String_2(MJIEnv env,
int clsref,
int i) |
int |
JPF_java_lang_Long.valueOf__J__Ljava_lang_Long_2(MJIEnv env,
int clsRef,
long val) |
int |
JPF_java_lang_String.valueOf__J__Ljava_lang_String_2(MJIEnv env,
int clsref,
long l) |
int |
JPF_java_lang_Short.valueOf__S__Ljava_lang_Short_2(MJIEnv env,
int clsRef,
short val) |
int |
JPF_java_lang_Boolean.valueOf__Z__Ljava_lang_Boolean_2(MJIEnv env,
int clsRef,
boolean val) |
static boolean |
JPF_gov_nasa_jpf_vm_Verify.vmIsMatchingStates____Z(MJIEnv env,
int clsObjRef) |
void |
JPF_java_lang_Object.wait____V(MJIEnv env,
int objref) |
void |
JPF_java_lang_Object.wait__J__V(MJIEnv env,
int objref,
long timeout) |
void |
JPF_java_lang_Object.wait__JI__V(MJIEnv env,
int objref,
long timeout,
int nanos) |
boolean |
JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.weakCompareAndSet__Ljava_lang_Object_2II__Z(MJIEnv env,
int objRef,
int tRef,
int fExpect,
int fUpdate) |
boolean |
JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.weakCompareAndSet__Ljava_lang_Object_2JJ__Z(MJIEnv env,
int objRef,
int tRef,
long fExpect,
long fUpdate) |
boolean |
JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.weakCompareAndSet__Ljava_lang_Object_2Ljava_lang_Object_2Ljava_lang_Object_2__Z(MJIEnv env,
int objRef,
int tRef,
int fExpect,
int fUpdate) |
void |
JPF_java_io_FileDescriptor.write___3BII__(MJIEnv env,
int objref,
int bref,
int offset,
int len) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.write___3BII__V(MJIEnv env,
int objRef,
int bufRef,
int off,
int len) |
void |
JPF_java_io_RandomAccessFile.write___3BII__V(MJIEnv env,
int this_ptr,
int data_array,
int start,
int len)
This is a bit lame doing it this way, but it is easy.
|
void |
JPF_java_io_FileDescriptor.write__I__(MJIEnv env,
int objref,
int b) |
void |
JPF_gov_nasa_jpf_ConsoleOutputStream.write__I__V(MJIEnv env,
int objRef,
int b) |
void |
JPF_java_io_RandomAccessFile.writeByte__I__V(MJIEnv env,
int this_ptr,
int data) |
void |
JPF_java_lang_Thread.yield____V(MJIEnv env,
int clsObjRef) |