rev 686+ - JPF error stack trace

47 views
Skip to first unread message

Darky SiDai

unread,
Mar 18, 2012, 8:06:35 AM3/18/12
to Java™ Pathfinder
Hello, Im using rev 686 and have the following problem when trying to
run it under a SUT.
I'm only using jpf-awt plugin with jpf-core, although i haven't
configure it yet, and I think
JPF crashes before reaching the scripted execution of the GUI:

java.lang.NullPointerException
at
gov.nasa.jpf.jvm.bytecode.Instruction.getFilePos(Instruction.java:275)
at
gov.nasa.jpf.jvm.StackFrame.getStackTraceInfo(StackFrame.java:1072)
at gov.nasa.jpf.jvm.JVM.printLiveThreadStatus(JVM.java:1679)
at
gov.nasa.jpf.report.ConsolePublisher.publishSnapshot(ConsolePublisher.java:
359)
at
gov.nasa.jpf.report.Publisher.publishPropertyViolation(Publisher.java:
299)
at
gov.nasa.jpf.report.Reporter.publishPropertyViolation(Reporter.java:
208)
at gov.nasa.jpf.report.Reporter.propertyViolated(Reporter.java:
242)
at
gov.nasa.jpf.search.Search.notifyPropertyViolated(Search.java:478)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:83)
at gov.nasa.jpf.JPF.run(JPF.java:618)
at gov.nasa.jpf.JPF.start(JPF.java:190)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown
Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:100)
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFListenerException: exception during propertyViolated()
notification
at
gov.nasa.jpf.search.Search.notifyPropertyViolated(Search.java:481)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:83)
at gov.nasa.jpf.JPF.run(JPF.java:618)
at gov.nasa.jpf.JPF.start(JPF.java:190)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown
Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:100)
Caused by: java.lang.NullPointerException
at
gov.nasa.jpf.jvm.bytecode.Instruction.getFilePos(Instruction.java:275)
at
gov.nasa.jpf.jvm.StackFrame.getStackTraceInfo(StackFrame.java:1072)
at gov.nasa.jpf.jvm.JVM.printLiveThreadStatus(JVM.java:1679)
at
gov.nasa.jpf.report.ConsolePublisher.publishSnapshot(ConsolePublisher.java:
359)
at
gov.nasa.jpf.report.Publisher.publishPropertyViolation(Publisher.java:
299)
at
gov.nasa.jpf.report.Reporter.publishPropertyViolation(Reporter.java:
208)
at gov.nasa.jpf.report.Reporter.propertyViolated(Reporter.java:
242)
at
gov.nasa.jpf.search.Search.notifyPropertyViolated(Search.java:478)
... 9 more

It happens only in a specific AUT, rest work fine. Any ideas on what
the problem might be?
Thanks in advance,
G.S.

George C. Stergiopoulos

unread,
Mar 18, 2012, 8:22:17 AM3/18/12
to java-pa...@googlegroups.com
I traced the error to this: Apparently, JPF traces an error

**
====================================================== error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: sun.misc.SharedSecrets.setJavaAWTAccess(Lsun/misc/JavaAWTAccess;)V
    at sun.awt.AppContext.<clinit>
    at javax.swing.SwingUtilities.appContextPut
    at javax.swing.JDialog.setDefaultLookAndFeelDecorated
**

and then fails at the snapshot output :

**
====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@343
  call stack:
[SEVERE] JPF exception, terminating: exception during propertyViolated() notification
**

Hope this helps in sheding some light on the matter.
G.S.

Peter Mehlitz

unread,
Mar 19, 2012, 2:09:10 PM3/19/12
to java-pa...@googlegroups.com
this (undocumented) code has unfortunately changed in Java 1.7, so I need to find some version independent solution.

The NPE should be fixed with v687, please verify. Apparently there is a class that didn't have a SourceFile attribute

-- Peter

Reply all
Reply to author
Forward
0 new messages