Here is a code sample:
// Overrided method from PropertyListenerAdapter
public void executeInstruction(JVM jvm) {
if (logExecuteInstruction) {
Instruction instr = jvm.getLastInstruction();
log("Execute instruction ");
ElementInfo ei = JVM.getVM().getLastElementInfo();
int numberOfFields = ei.getNumberOfFields();
for (int i = 0; i < numberOfFields; i++) {
FieldInfo fi = ei.getFieldInfo(i);
String fieldName = fi.getName();
log("\t" + fieldName);
if (fieldName.equals("isPrimitive")) {
log("\t\t isPrimitive ==" +
ei.getFields().getBooleanValue(i));
}
}
}
}
I receive a lot of output when I add this listener here is it part:
[MYLISTENER] Execute instruction
[MYLISTENER] name
[MYLISTENER] cref
[MYLISTENER] isPrimitive
[MYLISTENER] isPrimitive ==false
[MYLISTENER] enumConstantDirectory
I hope this will help you.
(1) noticing when the relevant variables are changed. This you do with a normal instructionExecuted() listener either on PUTFIELD/STATIC (if x,y are fields) or xSTORE instruction (if x,y are local vars, which is a little harder because you have to get the name of the local variable from the StackFrame this is executed in).
(2) store these variable/value tuples as a state extension, and restore it upon backtracking. There is some support for this with gov.nasa.jpf.util.StateExtensionListener/Client, but the only jpf-core example (SrciptEnvironment) is actually more complicated than your example.
(3) recognizing end states and processing your stored variables/values - that is a simple stateAdvanced() listener that checks for Search.isEndState()
(1) and (3) can be combined within the same listener, which should also be a StateExtensionClient. For (2) you use the StateExtensionListener as is.
-- Peter
Is that a solution to your problem?
Or you have some code that should do this but it doesn't work?
You are also aware of that you are using a cascaded ChoiceGenerator? Verify.getInt() already registers a CG, which is not replaced by your 'instrumentVerifyGetInt'. If you want to replace the Verify.getInt() CG you have to either (a) remove it and then register yours, or (b) use a executeInstruction() notification and skip the Verify.getInt() call (in which case you have to clean up the callstack yourself)
-- Peter
-- Peter