NPE in SandBoxChecker

[Attila Sragli]

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