Hi,
After some minor and totally harmless refactoring in my code, I always get the following from JPF:
JavaPathfinder v6.0 (rev 960) - (C) RIACS/NASA Ames Research Center
====================================================== system under test
application: hu/ngms/jpf/maven/JUnitWrapper.java
arguments: hu.ngms.jpf.maven.ConstTest
====================================================== search started: 3/12/13 2:54 PM
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFListenerException: exception during instructionExecuted() notification
at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:766)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:2256)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:2197)
at gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:781)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1794)
at gov.nasa.jpf.search.Search.forward(Search.java:533)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:78)
at gov.nasa.jpf.JPF.run(JPF.java:618)
at hu.ngms.jpf.maven.JpfUnittestMojo.execute(JpfUnittestMojo.java:46)
at org.apache.maven.plugin.DefaultBuildPluginManager.executeMojo(DefaultBuildPluginManager.java:101)
at org.apache.maven.lifecycle.internal.MojoExecutor.execute(MojoExecutor.java:209)
at org.apache.maven.lifecycle.internal.MojoExecutor.execute(MojoExecutor.java:153)
at org.apache.maven.lifecycle.internal.MojoExecutor.execute(MojoExecutor.java:145)
at org.apache.maven.lifecycle.internal.LifecycleModuleBuilder.buildProject(LifecycleModuleBuilder.java:84)
at org.apache.maven.lifecycle.internal.LifecycleModuleBuilder.buildProject(LifecycleModuleBuilder.java:59)
at org.apache.maven.lifecycle.internal.LifecycleStarter.singleThreadedBuild(LifecycleStarter.java:183)
at org.apache.maven.lifecycle.internal.LifecycleStarter.execute(LifecycleStarter.java:161)
at org.apache.maven.DefaultMaven.doExecute(DefaultMaven.java:320)
at org.apache.maven.DefaultMaven.execute(DefaultMaven.java:156)
at org.apache.maven.cli.MavenCli.execute(MavenCli.java:537)
at org.apache.maven.cli.MavenCli.doMain(MavenCli.java:196)
at org.apache.maven.cli.MavenCli.main(MavenCli.java:141)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:601)
at org.codehaus.plexus.classworlds.launcher.Launcher.launchEnhanced(Launcher.java:290)
at org.codehaus.plexus.classworlds.launcher.Launcher.launch(Launcher.java:230)
at org.codehaus.plexus.classworlds.launcher.Launcher.mainWithExitCode(Launcher.java:409)
at org.codehaus.plexus.classworlds.launcher.Launcher.main(Launcher.java:352)
Caused by: java.lang.NullPointerException
at gov.nasa.jpf.aprop.listener.SandBoxChecker.instructionExecuted(SandBoxChecker.java:307)
at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:755)
... 29 more
My code:
private static final String[] CONFIG = {
"+vm.insn_factory.class=.numeric.bytecode.InstructionFactory",
"+listener+=,.aprop.listener.ConstChecker",
"+listener+=,.aprop.listener.ContractVerifier",
"+listener+=,.aprop.listener.NonnullChecker",
"+listener+=,.aprop.listener.SandBoxChecker",
"+listener+=,.listener.PreciseRaceDetector",
"+listener+=,.listener.DeadlockAnalyzer",
JUnitWrapper.class.getName(), "hu.ngms.jpf.maven.ConstTest"
};
Config config = JPF.createConfig(CONFIG);
JPF jpf = new JPF(config);
jpf.run();
Any ideas, what went wrong?
Thanks,
--
Attila Sragli