Package | Description |
---|---|
gov.nasa.jpf | |
gov.nasa.jpf.jvm | |
gov.nasa.jpf.jvm.bytecode | |
gov.nasa.jpf.listener | |
gov.nasa.jpf.perturb | |
gov.nasa.jpf.util | |
gov.nasa.jpf.vm | |
gov.nasa.jpf.vm.serialize |
Modifier and Type | Method and Description |
---|---|
void |
PropertyListenerAdapter.methodEntered(VM vm,
ThreadInfo currentThread,
MethodInfo enteredMethod) |
void |
ListenerAdapter.methodEntered(VM vm,
ThreadInfo currentThread,
MethodInfo enteredMethod) |
void |
PropertyListenerAdapter.methodExited(VM vm,
ThreadInfo currentThread,
MethodInfo exitedMethod) |
void |
ListenerAdapter.methodExited(VM vm,
ThreadInfo currentThread,
MethodInfo exitedMethod) |
Modifier and Type | Field and Description |
---|---|
protected MethodInfo |
JVMCodeBuilder.mi |
Modifier and Type | Method and Description |
---|---|
DirectCallStackFrame |
JVMClassInfo.createDirectCallStackFrame(ThreadInfo ti,
MethodInfo miCallee,
int nLocals) |
DirectCallStackFrame |
JVMClassInfo.createRunStartStackFrame(ThreadInfo ti,
MethodInfo miRun)
while this is a normal DirectCallStackFrame, it has different code which has to be created here
|
StackFrame |
JVMClassInfo.createStackFrame(ThreadInfo ti,
MethodInfo callee) |
void |
JVMCodeBuilder.initialize(ClassFile classFile,
MethodInfo targetMethod) |
abstract Instruction |
JVMInstructionFactory.runstart(MethodInfo miRun) |
void |
JVMCodeBuilder.runStart(MethodInfo mi) |
protected void |
JVMClassInfo.setAnnotationValueGetterCode(MethodInfo pmi,
FieldInfo fi)
to be called from super proxy ctor
this needs to be in the VM specific ClassInfo because we need to create code
|
protected void |
JVMClassInfo.setDirectCallCode(MethodInfo miDirectCall,
MethodInfo miCallee) |
protected void |
JVMClassInfo.setRunStartCode(MethodInfo miRun,
MethodInfo miStub) |
Constructor and Description |
---|
JVMCodeBuilder(JVMInstructionFactory insnFactory,
ClassFile classFile,
MethodInfo targetMethod) |
JVMCodeBuilder(MethodInfo targetMethod) |
JVMStackFrame(MethodInfo callee) |
Modifier and Type | Field and Description |
---|---|
protected MethodInfo |
InvokeInstruction.invokedMethod
watch out - this is only const for static and special invocation
all virtuals will use it only as a cache
|
Modifier and Type | Method and Description |
---|---|
MethodInfo |
EXECUTENATIVE.getExecutedMethod() |
MethodInfo |
InvokeInstruction.getInvokedMethod() |
MethodInfo |
INVOKESTATIC.getInvokedMethod() |
MethodInfo |
VirtualInvocation.getInvokedMethod(ThreadInfo ti) |
abstract MethodInfo |
InvokeInstruction.getInvokedMethod(ThreadInfo ti) |
MethodInfo |
INVOKESPECIAL.getInvokedMethod(ThreadInfo th)
we can do some more caching here - the MethodInfo should be const
|
MethodInfo |
INVOKESTATIC.getInvokedMethod(ThreadInfo ti) |
MethodInfo |
VirtualInvocation.getInvokedMethod(ThreadInfo ti,
int objRef) |
Modifier and Type | Method and Description |
---|---|
Instruction |
InstructionFactory.runstart(MethodInfo miRun) |
protected void |
InvokeInstruction.setupCallee(ThreadInfo ti,
MethodInfo callee) |
Instruction |
StaticFieldInstruction.typeSafeClone(MethodInfo mi) |
Instruction |
VirtualInvocation.typeSafeClone(MethodInfo clonedMethod) |
Instruction |
IfInstruction.typeSafeClone(MethodInfo mi) |
Instruction |
InvokeInstruction.typeSafeClone(MethodInfo mi) |
Instruction |
GOTO.typeSafeClone(MethodInfo mi) |
Instruction |
INVOKESTATIC.typeSafeClone(MethodInfo mi) |
Modifier and Type | Field and Description |
---|---|
protected HashMap<MethodInfo,Perturbator.ParamsPerturbation> |
Perturbator.perturbedParams |
protected HashMap<MethodInfo,Perturbator.ReturnPerturbation> |
Perturbator.perturbedReturns |
Modifier and Type | Method and Description |
---|---|
boolean |
Perturbator.isMethodWatched(Instruction insn,
MethodInfo mi) |
protected void |
OOMEInjector.markMatchingInstructions(MethodInfo mi,
LocationSpec locSpec) |
void |
StackDepthChecker.methodEntered(VM vm,
ThreadInfo thread,
MethodInfo mi) |
Modifier and Type | Field and Description |
---|---|
protected MethodInfo |
GenericDataAbstractor.mi |
Modifier and Type | Method and Description |
---|---|
int[] |
GenericDataAbstractor.populateBoolean(MethodInfo mi,
String name) |
int[] |
GenericDataAbstractor.populateByte(MethodInfo mi,
String name) |
int[] |
GenericDataAbstractor.populateChar(MethodInfo mi,
String name) |
int[] |
GenericDataAbstractor.populateDouble(MethodInfo mi,
String name) |
int[] |
GenericDataAbstractor.populateFloat(MethodInfo mi,
String name) |
int[] |
GenericDataAbstractor.populateInt(MethodInfo mi,
String name) |
int[] |
GenericDataAbstractor.populateLong(MethodInfo mi,
String name) |
int[] |
GenericDataAbstractor.populateShort(MethodInfo mi,
String name) |
void |
GenericDataAbstractor.setMethodInfo(MethodInfo m,
StackFrame frame) |
Modifier and Type | Method and Description |
---|---|
MethodInfo |
Invocation.getMethodInfo() |
MethodInfo |
MethodInfoRegistry.getMethodInfo(MJIEnv env,
int objRef,
String fieldName) |
MethodInfo |
MethodInfoRegistry.getRegisteredFieldInfo(int idx) |
Modifier and Type | Method and Description |
---|---|
LocalVarInfo |
VarSpec.getMatchingLocalVarInfo(MethodInfo mi,
int pc,
int slotIdx) |
boolean |
MethodSpec.matches(MethodInfo mi) |
int |
MethodInfoRegistry.registerMethodInfo(MethodInfo mi) |
Constructor and Description |
---|
Invocation(MethodInfo mi,
Object[] args,
Object[] attrs) |
Modifier and Type | Class and Description |
---|---|
class |
NativeMethodInfo
a MethodInfo for a native peer executed method
|
Modifier and Type | Field and Description |
---|---|
MethodInfo |
AtomicData.currentMethod
The method in which the line step started.
|
protected MethodInfo |
ClassInfo.finalizer |
protected MethodInfo |
StackFrame.mi |
protected MethodInfo |
Instruction.mi |
Modifier and Type | Field and Description |
---|---|
protected Map<String,MethodInfo> |
ClassInfo.methods
all our declared declaredMethods (we don't flatten, this is not
a high-performance VM)
|
protected static ArrayList<MethodInfo> |
MethodInfo.mthTable |
Modifier and Type | Method and Description |
---|---|
static MethodInfo |
MethodInfo.create(String name,
String signature,
int modifiers) |
MethodInfo |
DirectCallStackFrame.getCallee() |
MethodInfo |
ClassInfo.getClinit() |
MethodInfo[] |
ClassInfo.getDeclaredMethodInfos() |
MethodInfo |
ClassInfo.getEnclosingMethodInfo()
same restriction as getEnclosingClassInfo() - might not be registered/initialized
|
MethodInfo |
ThreadInfo.getEntryMethod() |
MethodInfo |
ClassInfo.getFinalizer() |
protected MethodInfo |
ClassInfo.getFinalizer0() |
MethodInfo |
MethodInfo.getInstanceFor(ClassInfo ci)
Creates a method for a given class, by cloning this MethodInfo
and all the instructions belong to the method
|
protected MethodInfo |
VM.getMainEntryMethodInfo(String mthName,
ClassInfo ciMain) |
MethodInfo |
ClassInfo.getMethod(String uniqueName,
boolean isRecursiveLookup)
Note that 'uniqueName' is the name plus the argument type part of the
signature, idx.e.
|
MethodInfo |
ClassInfo.getMethod(String name,
String signature,
boolean isRecursiveLookup)
if we don't know the return type
signature is in paren/dot notation
|
MethodInfo |
MJIEnv.getMethodInfo() |
MethodInfo |
StackFrame.getMethodInfo() |
MethodInfo |
Instruction.getMethodInfo() |
static MethodInfo |
MethodInfo.getMethodInfo(int globalId) |
static MethodInfo |
JPF_java_lang_reflect_Method.getMethodInfo(MJIEnv env,
int objRef) |
MethodInfo |
MethodInfo.getOverriddenMethodInfo() |
MethodInfo |
ClassInfo.getReflectionMethod(String fullName,
boolean isRecursiveLookup)
almost the same as above, except of that Class.getMethod() doesn't specify
the return type.
|
MethodInfo |
ThreadInfo.getTopFrameMethodInfo()
returns the current method in the top stack frame, which is always a
bytecode method (executed by JPF)
|
MethodInfo |
ClassInfo.putDeclaredMethod(MethodInfo mi)
be careful, this replaces or adds MethodInfos dynamically
|
Modifier and Type | Method and Description |
---|---|
Iterator<MethodInfo> |
ClassInfo.declaredMethodIterator() |
List<MethodInfo> |
ClassInfo.getMatchingMethodInfos(MethodSpec mspec) |
Iterator<MethodInfo> |
ClassInfo.iterator() |
Modifier and Type | Method and Description |
---|---|
DirectCallStackFrame |
ClassInfo.createDirectCallStackFrame(ThreadInfo ti,
MethodInfo callee,
int nLocalSlots) |
DirectCallStackFrame |
ClassInfo.createRunStartStackFrame(ThreadInfo ti,
MethodInfo miRun) |
StackFrame |
ClassInfo.createStackFrame(ThreadInfo ti,
MethodInfo callee) |
Object[] |
StackFrame.getArgumentAttrs(MethodInfo miCallee)
return an array of all argument attrs, which in turn can be lists.
|
ElementInfo |
ThreadInfo.getBlockedObject(MethodInfo mi,
boolean isBeforeCall,
boolean isModifiable) |
int |
ThreadInfo.getCalleeThis(MethodInfo mi)
Returns the this pointer of the callee from the stack.
|
int |
StackFrame.getCalleeThis(MethodInfo mi)
return the object reference for an instance method to be called (we are still in the
caller's frame).
|
boolean |
StackFrame.hasArgumentAttr(MethodInfo miCallee,
Class<?> attrType)
check if there is any argument attr of the provided type on the operand stack
this is far more efficient than retrieving attribute values (we don't
care for argument types)
|
void |
Instruction.init(MethodInfo mi,
int offset,
int position) |
boolean |
ClassInfo.isStaticMethodAbstractionDeterministic(ThreadInfo th,
MethodInfo mi)
Checks if a static method call is deterministic, but only for
abtraction based determinism, due to Bandera.choose() calls
|
boolean |
MethodLocator.match(MethodInfo mi) |
void |
VMListener.methodEntered(VM vm,
ThreadInfo currentThread,
MethodInfo enteredMethod)
method body was entered.
|
void |
VMListener.methodExited(VM vm,
ThreadInfo currentThread,
MethodInfo exitedMethod)
method body was left.
|
protected void |
VM.notifyMethodEntered(ThreadInfo ti,
MethodInfo mi) |
protected void |
VM.notifyMethodExited(ThreadInfo ti,
MethodInfo mi) |
void |
StackFrame.processRefArguments(MethodInfo miCallee,
ReferenceProcessor visitor)
generic visitor for reference arguments
|
protected void |
VM.pushMainEntry(MethodInfo miMain,
String[] args,
ThreadInfo tiMain) |
protected void |
VM.pushMainEntryArgs(MethodInfo miMain,
String[] args,
ThreadInfo tiMain,
DirectCallStackFrame frame) |
MethodInfo |
ClassInfo.putDeclaredMethod(MethodInfo mi)
be careful, this replaces or adds MethodInfos dynamically
|
void |
StackFrame.removeArguments(MethodInfo mi) |
void |
NativeMethodInfo.replace(MethodInfo mi) |
protected void |
ClassInfo.setAnnotationValueGetterCode(MethodInfo pmi,
FieldInfo fi) |
protected void |
ClassInfo.setDirectCallCode(MethodInfo miCallee,
MethodInfo miStub) |
void |
Instruction.setMethodInfo(MethodInfo mi)
that's used for explicit construction of MethodInfos (synthetic methods)
|
void |
Attributor.setMethodInfoAttributes(MethodInfo mi) |
void |
DefaultAttributor.setMethodInfoAttributes(MethodInfo mi) |
void |
ConfigAttributor.setMethodInfoAttributes(MethodInfo mi) |
void |
ClassInfo.setMethods(MethodInfo[] methods) |
protected void |
ClassInfo.setRunStartCode(MethodInfo miRun,
MethodInfo miStub) |
Instruction |
Instruction.typeSafeClone(MethodInfo mi)
this is overridden by any Instruction that use a cache for class or
method to provide a type safe cloning
|
Constructor and Description |
---|
DirectCallStackFrame(MethodInfo miDirectCall,
MethodInfo callee) |
MethodInfo(MethodInfo mi)
for NativeMethodInfo creation
|
MethodInfo(MethodInfo callee,
int nLocals,
int nOperands)
for direct call construction
Note: this is only a partial initialization, the code still has to be created/installed by the caller
|
NativeMethodInfo(MethodInfo mi,
Method mth,
NativePeer peer) |
StackFrame(MethodInfo callee) |
StackFrame(MethodInfo m,
int nLocals,
int nOperands) |
Modifier and Type | Method and Description |
---|---|
FramePolicy |
AmmendableFilterConfiguration.FrameAmmendment.ammendFramePolicy(MethodInfo mi,
FramePolicy sofar) |
FramePolicy |
IgnoresFromAnnotations.ammendFramePolicy(MethodInfo mi,
FramePolicy sofar) |
protected FramePolicy |
FilteringSerializer.getFramePolicy(MethodInfo mi) |
FramePolicy |
AmmendableFilterConfiguration.getFramePolicy(MethodInfo mi) |
FramePolicy |
FilterConfiguration.getFramePolicy(MethodInfo mi) |