help me with symbc

[Imran]

im using Netbeans 7.2 on which successfully build core  v6.0 (rev 960+) 

Im getting errors trying to verify a .jpf file 

Errors :

Executing command: java -jar C:\Users\Imran\Documents\NetBeansProjects\jpf-core\build\RunJPF.jar +shell.port=4242 C:\Users\Imran\Documents\NetBeansProjects\jpf-core\src\examples\TopLevelcommandlineex.jpf 

JavaPathfinder v6.0 (rev 960+) - (C) RIACS/NASA Ames Research Center

====================================================== system under test

application: TopLevelcommandlineex.java

====================================================== search started: 5/1/13 4:30 PM

====================================================== error #1

gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty

java.lang.NoClassDefFoundError: commandlineexReader

at TopLevelcommandlineex.main(TopLevelcommandlineex.java:87)

====================================================== snapshot #1

thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,lockCount:0,suspendCount:0}

  call stack:

at TopLevelcommandlineex.main(TopLevelcommandlineex.java:87)

java.lang.NullPointerException

at gov.nasa.jpf.symbc.SymbolicListener.publishFinished(SymbolicListener.java:651)

[SEVERE] JPF exception, terminating: exception during searchFinished() notification

at gov.nasa.jpf.report.Publisher.publishFinished(Publisher.java:318)

at gov.nasa.jpf.report.ConsolePublisher.publishFinished(ConsolePublisher.java:120)

at gov.nasa.jpf.report.Reporter.publishFinished(Reporter.java:220)

at gov.nasa.jpf.report.Reporter.searchFinished(Reporter.java:248)

at gov.nasa.jpf.search.Search.notifySearchFinished(Search.java:523)

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

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 searchFinished() notification

at gov.nasa.jpf.search.Search.notifySearchFinished(Search.java:526)

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

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.symbc.SymbolicListener.publishFinished(SymbolicListener.java:651)

at gov.nasa.jpf.report.Publisher.publishFinished(Publisher.java:318)

at gov.nasa.jpf.report.ConsolePublisher.publishFinished(ConsolePublisher.java:120)

at gov.nasa.jpf.report.Reporter.publishFinished(Reporter.java:220)

at gov.nasa.jpf.report.Reporter.searchFinished(Reporter.java:248)

at gov.nasa.jpf.search.Search.notifySearchFinished(Search.java:523)

The TopLevelcommandlineex.jpf contents are :

target = TopLevelcommandlineex

classpath=.;C:/Users/Imran/Documents/NetBeansProjects/Polyglot/bin/TopLevelcommandlineex ;C:/Users/Imran/Documents/NetBeansProjects/Polyglot/bin/commandlineexReader;C:/Users/Imran/Documents/NetBeansProjects/Polyglot/bin/JSAP-2.1.jar;C:/Users/Imran/Documents/NetBeansProjects/Polyglot/bin/Statemachines.jar;

sourcepath = C:/Users/Imran/Documents/NetBeansProjects/Polyglot/bin/TopLevelcommandlineex;C:/Users/Imran/Documents/NetBeansProjects/Polyglot/bin/commandlineexReader

#cg.enumerate_random = true

#report.console.property_violation=error,trace

symbolic.method = Assume.test(sym#sym)

symbolic.min_int=-100

symbolic.max_int=100

[Imran Syed]

I tried verifying other .jpf and it worked fine

TopLevelxxxx files are giving no problem when verified without symbc .

 .... Im not much familiar with symbc but its always not finding class xxxxReader.class even though classpath and sourcepath is given in .jpf .

Im following instructions given in docs of polyglot

Thank you

--
 
---
You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

[Corina Pasareanu]

??

your message is confusing

corina

[Corina Pasareanu]

seems there is a bug in the listener?

can you please send me the java example so that i can debug?

thanks
corina

--