[Javapathfinder-user] Problem about [Symbolic Execution][ Coverage ]

[ZHU H. <ry...@us...>]

Dear Sir or madam,

I tried the example under "~/trunk/extensions/symbc/examples/coverage"
this week to see how the symbolic execution runs.
As it is said that "The trickiest part here is
CheckCoverage.processTestCase()". But what I got from the symbolic
execution is like this:

Property Violated: PC is # = 3
int_2_SYMINT[-10000] < CONST_5 &&
int_1_SYMINT[-10000] < CONST_0 &&
(int_2_SYMINT[-10000] + int_1_SYMINT[-10000]) <= CONST_0
Property Violated: result is
"java.lang.reflect.InvocationTargetException: in
coverage.CheckCoverage.processTestCase :
java.lang.NullPointerException..."
****************************

====================================================== error #8
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.reflect.InvocationTargetException: in
coverage.CheckCoverage.processTestCase : java.lang.NullPointerException
        at coverage.CheckCoverage.processTestCase(Native Method)
        at
coverage.MyClassWithPathAnnotations.myMethod(MyClassWithPathAnnotations.java:34)
        at
coverage.MyDriverForPathAnnotations.main(MyDriverForPathAnnotations.java:7)


====================================================== trace #8
------------------------------------------------------ transition #0
thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
      [487 insn w/o sources]
------------------------------------------------------ transition #1
thread: 0
gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[0..0,delta=+1,cur=0]
      [15 insn w/o sources]
------------------------------------------------------ transition #2
thread: 0
gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[0..1,delta=+1,cur=1]
      [4 insn w/o sources]
------------------------------------------------------ transition #3
thread: 0
gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[0..1,delta=+1,cur=0]
      [4 insn w/o sources]
------------------------------------------------------ transition #4
thread: 0
gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[0..1,delta=+1,cur=1]
      [4 insn w/o sources]

====================================================== Method Summaries

myMethod(-1,2)  --> "java.lang.reflect.InvocationTargetException: in
coverage.CheckCoverage.processTestCase :
java.lang.NullPointerException..."
...
...


Here is my platform infos:
Linux 2.6.22-14-server #1 SMP Tue Feb 12 03:10:53 UTC 2008 x86_64 GNU/Linux
java version "1.6.0_07"
Java(TM) SE Runtime Environment (build 1.6.0_07-b06)
Java HotSpot(TM) 64-Bit Server VM (build 10.0-b23, mixed mode)

And my jpf.properties:
vm.classpath = .
vm.sourcepath+= ,${user.home}/tmp
vm.storage.class=
symbolic.method=myMethod(sym#sym)
search.multiple_errors=true
jpf.report.console.finished=
coverage.MyDriverForPathAnnotations
vm.insn_factory.class = gov.nasa.jpf.symbc.SymbolicInstructionFactory
jpf.listener = gov.nasa.jpf.symbc.SymbolicListener
log.level=warning

I typed this command:
:~/trunk/extensions/symbc/examples$ ~/trunk/bin/jpf -c
coverage/jpf.properties coverage.MyDriverForPathAnnotations


I really don't how to get through this. The trickest
CheckCoverage.processTestCase() is what I am interested in. Would you
please tell me what's going on with the error I got?

Thank you.

Best regards
ZHU Hua