public class MJIEnv extends Object
Modifier and Type | Field and Description |
---|---|
static int |
NULL |
Modifier and Type | Method and Description |
---|---|
void |
addElementAttr(int objref,
int idx,
Object a) |
void |
addFieldAttr(int objref,
String fname,
Object a) |
void |
addListener(JPFListener l) |
void |
addObjectAttr(int objref,
Object a) |
boolean |
canLock(int objref) |
long |
currentTimeMillis() |
String |
format(int fmtRef,
int argRef) |
String |
format(Locale l,
int fmtRef,
int argRef) |
void |
gc() |
Object[] |
getArgAttributes()
return attr list of all arguments.
|
Object[] |
getArgumentArray(int argRef) |
int |
getArrayLength(int objref) |
String |
getArrayType(int objref) |
int |
getArrayTypeSize(int objref) |
boolean |
getBooleanArrayElement(int objref,
int index) |
boolean[] |
getBooleanArrayObject(int objref) |
boolean |
getBooleanField(int objref,
String fname) |
Boolean |
getBooleanObject(int objref) |
boolean |
getBooleanValue(int objref) |
byte |
getByteArrayElement(int objref,
int index) |
byte[] |
getByteArrayObject(int objref) |
byte |
getByteField(int objref,
String fname) |
Byte |
getByteObject(int objref) |
byte |
getByteValue(int objref) |
StackFrame |
getCallerStackFrame() |
char |
getCharArrayElement(int objref,
int index) |
char[] |
getCharArrayObject(int objref) |
char |
getCharField(int objref,
String fname) |
Character |
getCharObject(int objref) |
char |
getCharValue(int objref) |
ChoiceGenerator<?> |
getChoiceGenerator() |
ClassInfo |
getClassInfo(int objref) |
ClassLoaderInfo |
getClassLoaderInfo(int clObjRef)
It returns the ClassLoaderInfo corresponding to the given classloader object
reference
|
String |
getClassName(int objref) |
Config |
getConfig() |
Date |
getDateObject(int objref) |
int |
getDeclaredIntField(int objref,
String refType,
String fname) |
double |
getDoubleArrayElement(int objref,
int index) |
double[] |
getDoubleArrayObject(int objref) |
double |
getDoubleField(int objref,
String fname) |
Double |
getDoubleObject(int objref) |
double |
getDoubleValue(int objref) |
Object |
getElementAttr(int objref,
int idx)
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
<T> T |
getElementAttr(int objref,
int idx,
Class<T> attrType)
this only returns the first attr of this type, there can be more
if you don't use client private types or the provided type is too general
|
ElementInfo |
getElementInfo(int objref) |
Object |
getFieldAttr(int objref,
String fname)
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
<T> T |
getFieldAttr(int objref,
String fname,
Class<T> attrType)
this only returns the first attr of this type, there can be more
if you don't use client private types or the provided type is too general
|
float |
getFloatArrayElement(int objref,
int index) |
float[] |
getFloatArrayObject(int objref) |
float |
getFloatField(int objref,
String fname) |
Float |
getFloatObject(int objref) |
float |
getFloatValue(int objref) |
Heap |
getHeap() |
Instruction |
getInstruction() |
int |
getIntArrayElement(int objref,
int index) |
int[] |
getIntArrayObject(int objref) |
Integer |
getIntegerObject(int objref) |
int |
getIntField(int objref,
String fname) |
int |
getIntValue(int objref) |
JPF |
getJPF() |
KernelState |
getKernelState() |
ThreadInfo |
getLiveThreadInfoForId(int id) |
ThreadInfo |
getLiveThreadInfoForObjRef(int id) |
ThreadInfo[] |
getLiveThreads() |
long |
getLongArrayElement(int objref,
int index) |
long[] |
getLongArrayObject(int objref) |
long |
getLongField(int objref,
String fname) |
Long |
getLongObject(int objref) |
long |
getLongValue(int objref) |
MethodInfo |
getMethodInfo() |
StackFrame |
getModifiableCallerStackFrame() |
ElementInfo |
getModifiableElementInfo(int objref) |
Object |
getObjectAttr(int objref)
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
<T> T |
getObjectAttr(int objref,
Class<T> attrType)
this only returns the first attr of this type, there can be more
if you don't use client private types or the provided type is too general
|
int |
getReferenceArrayElement(int objref,
int index) |
int[] |
getReferenceArrayObject(int objref) |
int |
getReferenceField(int objref,
FieldInfo fi) |
int |
getReferenceField(int objref,
String fname) |
ClassInfo |
getReferredClassInfo(int clsObjRef) |
Object |
getReturnAttribute() |
SchedulerFactory |
getSchedulerFactory() |
short |
getShortArrayElement(int objref,
int index) |
short[] |
getShortArrayObject(int objref) |
short |
getShortField(int objref,
String fname) |
Short |
getShortObject(int objref) |
short |
getShortValue(int objref) |
int |
getStateId() |
boolean |
getStaticBooleanField(String clsName,
String fname) |
byte |
getStaticByteField(String clsName,
String fname) |
char |
getStaticCharField(String clsName,
String fname) |
double |
getStaticDoubleField(ClassInfo ci,
String fname) |
double |
getStaticDoubleField(int clsObjRef,
String fname) |
double |
getStaticDoubleField(String clsName,
String fname) |
float |
getStaticFloatField(String clsName,
String fname) |
int |
getStaticIntField(ClassInfo ci,
String fname) |
int |
getStaticIntField(int clsObjRef,
String fname) |
int |
getStaticIntField(String clsName,
String fname) |
long |
getStaticLongField(ClassInfo ci,
String fname) |
long |
getStaticLongField(int clsRef,
String fname) |
long |
getStaticLongField(String clsName,
String fname) |
int |
getStaticReferenceField(ClassInfo ci,
String fname) |
int |
getStaticReferenceField(int clsObjRef,
String fname) |
int |
getStaticReferenceField(String clsName,
String fname) |
short |
getStaticShortField(String clsName,
String fname) |
String[] |
getStringArrayObject(int aRef) |
char[] |
getStringChars(int objRef) |
String |
getStringField(int objref,
String fname) |
String |
getStringObject(int objRef)
turn JPF String object into a VM String object
(this is a method available for non gov..jvm NativePeer classes)
|
ClassLoaderInfo |
getSystemClassLoaderInfo() |
SystemState |
getSystemState() |
ThreadInfo |
getThreadInfo() |
ThreadInfo |
getThreadInfoForId(int id)
NOTE - callers have to be prepared this might return null in case
the thread got already terminated
|
ThreadInfo |
getThreadInfoForObjRef(int id)
NOTE - callers have to be prepared this might return null in case
the thread got already terminated
|
String |
getTypeName(int objref) |
VM |
getVM() |
void |
handleClinitRequest(ClassInfo ci) |
boolean |
hasElementAttr(int objref,
Class<?> type) |
boolean |
hasElementdAttr(int objref) |
boolean |
hasException() |
boolean |
hasFieldAttr(int objref) |
boolean |
hasFieldAttr(int objref,
Class<?> type) |
boolean |
hasObjectAttr(int objref) |
boolean |
hasObjectAttr(int objref,
Class<?> type) |
boolean |
hasPendingInterrupt() |
void |
ignoreTransition() |
boolean |
isArray(int objref) |
boolean |
isBigEndianPlatform() |
boolean |
isInstanceOf(int objref,
String clsName) |
boolean |
isInvocationRepeated() |
boolean |
isSchedulingRelevantObject(int objref) |
long |
nanoTime() |
int |
newBoolean(boolean b) |
int |
newBooleanArray(int size) |
int |
newByte(byte b) |
int |
newByteArray(byte[] buf) |
int |
newByteArray(int size) |
int |
newCharacter(char c) |
int |
newCharArray(char[] buf) |
int |
newCharArray(int size) |
int |
newDouble(double d) |
int |
newDoubleArray(double[] buf) |
int |
newDoubleArray(int size) |
int |
newFloat(float f) |
int |
newFloatArray(float[] buf) |
int |
newFloatArray(int size) |
int |
newIntArray(int size) |
int |
newIntArray(int[] buf) |
int |
newInteger(int n) |
int |
newLong(long l) |
int |
newLongArray(int size) |
int |
newLongArray(long[] buf) |
int |
newObject(ClassInfo ci)
check if the ClassInfo is properly initialized
if yes, create a new instance of it but don't call any ctor
if no, throw a ClinitRequired exception
|
int |
newObject(String clsName) |
int |
newObjectArray(String elementClsName,
int size) |
int |
newObjectOfUncheckedClass(ClassInfo ci)
this creates a new object without checking if the ClassInfo needs
initialization.
|
int |
newShort(short s) |
int |
newShortArray(int size) |
int |
newShortArray(short[] buf) |
int |
newString(int arrayRef) |
int |
newString(String s) |
int |
newStringArray(String[] a) |
void |
notify(ElementInfo ei) |
void |
notify(int objref) |
void |
notifyAll(ElementInfo ei) |
void |
notifyAll(int objref) |
int |
peekException() |
int |
popException() |
void |
registerPinDown(int objref) |
void |
releasePinDown(int objref) |
void |
removeListener(JPFListener l) |
void |
repeatInvocation()
repeat execution of the instruction that caused a native method call
NOTE - this does NOT mean it's the NEXT executed insn, since the native method
might have pushed direct call frames on the stack before asking us to repeat it.
|
boolean |
requiresClinitExecution(ClassInfo ci)
use this whenever a peer performs an operation on a class that might not be initialized yet
Do a repeatInvocation() in this case
|
void |
setBooleanArrayElement(int objref,
int index,
boolean value) |
void |
setBooleanField(int objref,
String fname,
boolean val) |
void |
setByteArrayElement(int objref,
int index,
byte value) |
void |
setByteField(int objref,
String fname,
byte val) |
void |
setCharArrayElement(int objref,
int index,
char value) |
void |
setCharField(int objref,
String fname,
char val) |
void |
setDeclaredIntField(int objref,
String refType,
String fname,
int val) |
void |
setDeclaredReferenceField(int objref,
String refType,
String fname,
int val) |
void |
setDoubleArrayElement(int objref,
int index,
double value) |
void |
setDoubleField(int objref,
String fname,
double val) |
void |
setElementAttr(int objref,
int idx,
Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
setFieldAttr(int objref,
String fname,
Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
setFloatArrayElement(int objref,
int index,
float value) |
void |
setFloatField(int objref,
String fname,
float val) |
void |
setIntArrayElement(int objref,
int index,
int value) |
void |
setIntField(int objref,
String fname,
int val) |
void |
setLongArrayElement(int objref,
int index,
long value) |
void |
setLongField(int objref,
String fname,
long val) |
void |
setMandatoryNextChoiceGenerator(ChoiceGenerator<?> cg,
String failMsg) |
boolean |
setNextChoiceGenerator(ChoiceGenerator<?> cg) |
void |
setObjectAttr(int objref,
Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
setReferenceArrayElement(int objref,
int index,
int eRef) |
void |
setReferenceField(int objref,
String fname,
int ref) |
void |
setReturnAttribute(Object attr) |
void |
setShortArrayElement(int objref,
int index,
short value) |
void |
setShortField(int objref,
String fname,
short val) |
void |
setStaticBooleanField(int clsObjRef,
String fname,
boolean val) |
void |
setStaticBooleanField(String clsName,
String fname,
boolean value) |
void |
setStaticByteField(String clsName,
String fname,
byte value) |
void |
setStaticCharField(String clsName,
String fname,
char value) |
void |
setStaticDoubleField(String clsName,
String fname,
double val) |
void |
setStaticFloatField(String clsName,
String fname,
float val) |
void |
setStaticIntField(int clsObjRef,
String fname,
int val) |
void |
setStaticIntField(String clsName,
String fname,
int val) |
void |
setStaticLongField(int clsObjRef,
String fname,
long val) |
void |
setStaticLongField(String clsName,
String fname,
long value) |
void |
setStaticReferenceField(int clsObjRef,
String fname,
int objref) |
void |
setStaticReferenceField(String clsName,
String fname,
int objref) |
void |
stopThread() |
void |
stopThreadWithException(int xRef) |
void |
throwAssertion(String details) |
void |
throwException(int xRef) |
void |
throwException(String clsName) |
void |
throwException(String clsName,
String details) |
void |
throwInterrupt() |
int |
valueOfBoolean(boolean b) |
int |
valueOfByte(byte b) |
int |
valueOfCharacter(char c) |
int |
valueOfInteger(int i) |
int |
valueOfLong(long l) |
int |
valueOfShort(short s) |
public static final int NULL
public VM getVM()
public JPF getJPF()
public boolean isBigEndianPlatform()
public void addListener(JPFListener l)
public void removeListener(JPFListener l)
public Config getConfig()
public void gc()
public void ignoreTransition()
public boolean isArray(int objref)
public int getArrayLength(int objref)
public String getArrayType(int objref)
public int getArrayTypeSize(int objref)
public boolean hasObjectAttr(int objref)
public boolean hasObjectAttr(int objref, Class<?> type)
public Object getObjectAttr(int objref)
public void setObjectAttr(int objref, Object a)
public void addObjectAttr(int objref, Object a)
public <T> T getObjectAttr(int objref, Class<T> attrType)
public boolean hasFieldAttr(int objref)
public boolean hasFieldAttr(int objref, Class<?> type)
public Object getFieldAttr(int objref, String fname)
public void setFieldAttr(int objref, String fname, Object a)
public <T> T getFieldAttr(int objref, String fname, Class<T> attrType)
public boolean hasElementdAttr(int objref)
public boolean hasElementAttr(int objref, Class<?> type)
public Object getElementAttr(int objref, int idx)
public void setElementAttr(int objref, int idx, Object a)
public void addElementAttr(int objref, int idx, Object a)
public <T> T getElementAttr(int objref, int idx, Class<T> attrType)
public void setBooleanField(int objref, String fname, boolean val)
public boolean getBooleanField(int objref, String fname)
public boolean getBooleanArrayElement(int objref, int index)
public void setBooleanArrayElement(int objref, int index, boolean value)
public void setByteField(int objref, String fname, byte val)
public byte getByteField(int objref, String fname)
public void setCharField(int objref, String fname, char val)
public char getCharField(int objref, String fname)
public void setDoubleField(int objref, String fname, double val)
public double getDoubleField(int objref, String fname)
public void setFloatField(int objref, String fname, float val)
public float getFloatField(int objref, String fname)
public void setByteArrayElement(int objref, int index, byte value)
public byte getByteArrayElement(int objref, int index)
public void setCharArrayElement(int objref, int index, char value)
public void setIntArrayElement(int objref, int index, int value)
public void setShortArrayElement(int objref, int index, short value)
public void setFloatArrayElement(int objref, int index, float value)
public float getFloatArrayElement(int objref, int index)
public double getDoubleArrayElement(int objref, int index)
public void setDoubleArrayElement(int objref, int index, double value)
public short getShortArrayElement(int objref, int index)
public int getIntArrayElement(int objref, int index)
public char getCharArrayElement(int objref, int index)
public void setIntField(int objref, String fname, int val)
public void setDeclaredIntField(int objref, String refType, String fname, int val)
public int getIntField(int objref, String fname)
public void setDeclaredReferenceField(int objref, String refType, String fname, int val)
public void setReferenceField(int objref, String fname, int ref)
public int getReferenceField(int objref, String fname)
public int getReferenceField(int objref, FieldInfo fi)
public boolean getBooleanValue(int objref)
public byte getByteValue(int objref)
public char getCharValue(int objref)
public short getShortValue(int objref)
public int getIntValue(int objref)
public long getLongValue(int objref)
public float getFloatValue(int objref)
public double getDoubleValue(int objref)
public void setLongArrayElement(int objref, int index, long value)
public long getLongArrayElement(int objref, int index)
public void setLongField(int objref, String fname, long val)
public long getLongField(int objref, String fname)
public void setReferenceArrayElement(int objref, int index, int eRef)
public int getReferenceArrayElement(int objref, int index)
public void setShortField(int objref, String fname, short val)
public short getShortField(int objref, String fname)
public String getTypeName(int objref)
public boolean isInstanceOf(int objref, String clsName)
public void setStaticBooleanField(String clsName, String fname, boolean value)
public void setStaticBooleanField(int clsObjRef, String fname, boolean val)
public double getStaticDoubleField(int clsObjRef, String fname)
public void setStaticIntField(int clsObjRef, String fname, int val)
public int getStaticIntField(int clsObjRef, String fname)
public void setStaticLongField(int clsObjRef, String fname, long val)
public long getStaticLongField(int clsRef, String fname)
public void setStaticReferenceField(String clsName, String fname, int objref)
public void setStaticReferenceField(int clsObjRef, String fname, int objref)
public int getStaticReferenceField(int clsObjRef, String fname)
public char[] getStringChars(int objRef)
public String getStringObject(int objRef)
public String[] getStringArrayObject(int aRef)
public Date getDateObject(int objref)
public Object[] getArgumentArray(int argRef)
public Boolean getBooleanObject(int objref)
public Byte getByteObject(int objref)
public Character getCharObject(int objref)
public Short getShortObject(int objref)
public Integer getIntegerObject(int objref)
public Long getLongObject(int objref)
public Float getFloatObject(int objref)
public Double getDoubleObject(int objref)
public byte[] getByteArrayObject(int objref)
public char[] getCharArrayObject(int objref)
public short[] getShortArrayObject(int objref)
public int[] getIntArrayObject(int objref)
public long[] getLongArrayObject(int objref)
public float[] getFloatArrayObject(int objref)
public double[] getDoubleArrayObject(int objref)
public boolean[] getBooleanArrayObject(int objref)
public int[] getReferenceArrayObject(int objref)
public boolean isSchedulingRelevantObject(int objref)
public boolean canLock(int objref)
public int newBooleanArray(int size)
public int newByteArray(int size)
public int newByteArray(byte[] buf)
public int newCharArray(int size)
public int newCharArray(char[] buf)
public int newShortArray(int size)
public int newShortArray(short[] buf)
public int newDoubleArray(int size)
public int newDoubleArray(double[] buf)
public int newFloatArray(int size)
public int newFloatArray(float[] buf)
public int newIntArray(int size)
public int newIntArray(int[] buf)
public int newLongArray(int size)
public int newLongArray(long[] buf)
public int newObjectArray(String elementClsName, int size)
public int newObject(ClassInfo ci)
public int newObjectOfUncheckedClass(ClassInfo ci)
public int newObject(String clsName)
public int newString(String s)
public int newStringArray(String[] a)
public int newString(int arrayRef)
public String format(int fmtRef, int argRef)
public int newBoolean(boolean b)
public int newInteger(int n)
public int newLong(long l)
public int newDouble(double d)
public int newFloat(float f)
public int newByte(byte b)
public int newShort(short s)
public int newCharacter(char c)
public void notify(int objref)
public void notify(ElementInfo ei)
public void notifyAll(int objref)
public void notifyAll(ElementInfo ei)
public void registerPinDown(int objref)
public void releasePinDown(int objref)
public boolean requiresClinitExecution(ClassInfo ci)
public void repeatInvocation()
public boolean isInvocationRepeated()
public boolean setNextChoiceGenerator(ChoiceGenerator<?> cg)
public void setMandatoryNextChoiceGenerator(ChoiceGenerator<?> cg, String failMsg)
public SchedulerFactory getSchedulerFactory()
public ChoiceGenerator<?> getChoiceGenerator()
public void setReturnAttribute(Object attr)
public Object[] getArgAttributes()
public Object getReturnAttribute()
public void throwException(int xRef)
public void throwException(String clsName)
public void throwAssertion(String details)
public void throwInterrupt()
public void stopThread()
public void stopThreadWithException(int xRef)
public ClassInfo getReferredClassInfo(int clsObjRef)
public ClassInfo getClassInfo(int objref)
public String getClassName(int objref)
public Heap getHeap()
public ElementInfo getElementInfo(int objref)
public ElementInfo getModifiableElementInfo(int objref)
public int getStateId()
public int peekException()
public int popException()
public boolean hasException()
public boolean hasPendingInterrupt()
public long currentTimeMillis()
public long nanoTime()
public KernelState getKernelState()
public MethodInfo getMethodInfo()
public Instruction getInstruction()
public ClassLoaderInfo getClassLoaderInfo(int clObjRef)
public ClassLoaderInfo getSystemClassLoaderInfo()
public SystemState getSystemState()
public ThreadInfo getThreadInfo()
public ThreadInfo getThreadInfoForId(int id)
public ThreadInfo getLiveThreadInfoForId(int id)
public ThreadInfo getThreadInfoForObjRef(int id)
public ThreadInfo getLiveThreadInfoForObjRef(int id)
public ThreadInfo[] getLiveThreads()
public void handleClinitRequest(ClassInfo ci)
public StackFrame getCallerStackFrame()
public StackFrame getModifiableCallerStackFrame()
public int valueOfBoolean(boolean b)
public int valueOfByte(byte b)
public int valueOfCharacter(char c)
public int valueOfShort(short s)
public int valueOfInteger(int i)
public int valueOfLong(long l)