---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.format
at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:263)
at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:74)
at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:2022)
at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1909)
at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:734)
at gov.nasa.jpf.vm.VM.forward(VM.java:1675)
at gov.nasa.jpf.search.Search.forward(Search.java:580)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
at gov.nasa.jpf.JPF.run(JPF.java:715)
at gov.nasa.jpf.util.test.TestJPF.createAndRunJPF(TestJPF.java:677)
at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:807)
at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:831)
at cmu.defect4j.math3.analysis.differentiation.DerivativeStructureTest.testSerialization(DerivativeStructureTest.java:598)
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:606)
at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:47)
at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:44)
at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
at org.junit.internal.runners.statements.FailOnTimeout$StatementThread.run(FailOnTimeout.java:74)
Caused by: java.util.IllegalFormatConversionException: x != cmu.conditional.One
at java.util.Formatter$FormatSpecifier.failConversion(Formatter.java:4045)
at java.util.Formatter$FormatSpecifier.printInteger(Formatter.java:2748)
at java.util.Formatter$FormatSpecifier.print(Formatter.java:2702)
at java.util.Formatter.format(Formatter.java:2488)
at java.util.Formatter.format(Formatter.java:2423)
at java.lang.String.format(String.java:2790)
at gov.nasa.jpf.vm.MJIEnv.format(MJIEnv.java:1191)
at gov.nasa.jpf.vm.JPF_java_lang_String.format__Ljava_lang_String_2_3Ljava_lang_Object_2__Ljava_lang_String_2(JPF_java_lang_String.java:729)
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:606)
at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:182)
... 21
Problem
Serialization problem.
Example
DerivativeStructureTest.java (testSerialization)
---------------------- JPF error stack trace --------------------- gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.format at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:263) at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:74) at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:2022) at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1909) at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:734) at gov.nasa.jpf.vm.VM.forward(VM.java:1675) at gov.nasa.jpf.search.Search.forward(Search.java:580) at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79) at gov.nasa.jpf.JPF.run(JPF.java:715) at gov.nasa.jpf.util.test.TestJPF.createAndRunJPF(TestJPF.java:677) at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:807) at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:831) at cmu.defect4j.math3.analysis.differentiation.DerivativeStructureTest.testSerialization(DerivativeStructureTest.java:598) 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:606) at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:47) at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12) at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:44) at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17) at org.junit.internal.runners.statements.FailOnTimeout$StatementThread.run(FailOnTimeout.java:74) Caused by: java.util.IllegalFormatConversionException: x != cmu.conditional.One at java.util.Formatter$FormatSpecifier.failConversion(Formatter.java:4045) at java.util.Formatter$FormatSpecifier.printInteger(Formatter.java:2748) at java.util.Formatter$FormatSpecifier.print(Formatter.java:2702) at java.util.Formatter.format(Formatter.java:2488) at java.util.Formatter.format(Formatter.java:2423) at java.lang.String.format(String.java:2790) at gov.nasa.jpf.vm.MJIEnv.format(MJIEnv.java:1191) at gov.nasa.jpf.vm.JPF_java_lang_String.format__Ljava_lang_String_2_3Ljava_lang_Object_2__Ljava_lang_String_2(JPF_java_lang_String.java:729) 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:606) at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:182) ... 21