[Javapathfinder-user] NullPointer during search of jpf

[zuo j. <zu...@pk...>]

Hi, a new trouble came out. A NullPointer Exception was issued from deep
inside jpf. At the beginning, I thought that the NullPointer might happen
somewhere in my application. So, I set up many points to print out how my
app behaved. In this way, I narrowed down to the place where the exception
happened. But I could not find any reference to a null pointer there.
Instead, my app just stopped there. Superficially, there seemed nothing
wrong with the piece of code. 

Can anybody give me a hint? Though I know the problem is so subtle that it
may be difficult to find out the reason. I just paste the error message
below. Sorry for its length.

 

J. H. Zuo 

 

$ bin/jpf model.MailVerifier > result

JPF exception, terminating: class java.lang.NullPointerException: null

 

java.lang.NullPointerException

        at gov.nasa.jpf.jvm.DynamicArea.markRecursive(DynamicArea.java:310)

        at gov.nasa.jpf.jvm.DynamicArea.analyzeHeap(DynamicArea.java:161)

        at
gov.nasa.jpf.jvm.ElementInfo.updateReachability(ElementInfo.java:346

 

        at
gov.nasa.jpf.jvm.ElementInfo.setReferenceField(ElementInfo.java:367)

        at gov.nasa.jpf.jvm.bytecode.PUTFIELD.execute(PUTFIELD.java:63)

        at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1505)

        at gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2081)

        at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1565)

        at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:285)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1111)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at
gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340)

        at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:92)

        at gov.nasa.jpf.JPF.run(JPF.java:308)

        at gov.nasa.jpf.JPF.main(JPF.java:238)

java.lang.NullPointerException

        at gov.nasa.jpf.jvm.DynamicArea.markRecursive(DynamicArea.java:310)

        at gov.nasa.jpf.jvm.DynamicArea.analyzeHeap(DynamicArea.java:161)

        at
gov.nasa.jpf.jvm.ElementInfo.updateReachability(ElementInfo.java:346

 

        at
gov.nasa.jpf.jvm.ElementInfo.setReferenceField(ElementInfo.java:367)

        at gov.nasa.jpf.jvm.bytecode.PUTFIELD.execute(PUTFIELD.java:63)

        at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1505)

        at gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2081)

        at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1565)

        at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:285)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1111)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at
gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340)

        at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:92)

        at gov.nasa.jpf.JPF.run(JPF.java:308)

        at gov.nasa.jpf.JPF.main(JPF.java:238)

gov.nasa.jpf.JPFException: class java.lang.NullPointerException: null

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1154)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)

        at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)

        at
gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340)

        at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:92)

        at gov.nasa.jpf.JPF.run(JPF.java:308)

        at gov.nasa.jpf.JPF.main(JPF.java:238)