Hi,
I tried to build and test JPF (jpf-core) on Ubuntu 11.10. There is Java 1.7 (icedtea) installed on
the system (both jre and jdk). During the tests (ant test), everything seems correct up to the point
with DateFormatTest. I found a similar thread on the list however, there was no conclusion about the
problem.
I ran the specific test for DateFormat : bin/test .test.java.text.DateFormatTest. I get the below
ouput (sorry for the long text). I am currently debugging a software that uses DateTime and Date
classes and I want to make sure that JPF passes all tests at the first place. Do you have any idea
what might be the reason I am getting this error?
I am also reading the information at the link:
http://javapathfinder.sourceforge.net/The_Model_Java_Interface.html
for learning more about JPF's JVM but is there a more up-to-date link or that is already u-to-date?
Thanks in advance.
OUTPUT:
......................................... testing testSetAndGetTimeZone()
running jpf with args: gov.nasa.jpf.util.test.TestJPFHelper gov.nasa.jpf.test.java.text.DateFormatTest testSetAndGetTimeZone
JavaPathfinder v6.0 (rev 659) - (C) RIACS/NASA Ames Research Center
====================================================== system under test
application: gov/nasa/jpf/util/test/TestJPFHelper.java
arguments: gov.nasa.jpf.test.java.text.DateFormatTest testSetAndGetTimeZone
====================================================== search started: 15/02/12 11:54
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.toLowerCase
at gov.nasa.jpf.jvm.NativeMethodInfo.executeNative(NativeMethodInfo.java:199)
at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:72)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:2223)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:2175)
at gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:712)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1775)
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 gov.nasa.jpf.util.test.TestJPF.runJPF(TestJPF.java:655)
at gov.nasa.jpf.util.test.TestJPF.createAndRunJPF(TestJPF.java:601)
at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:706)
at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:736)
at gov.nasa.jpf.test.java.text.DateFormatTest.testSetAndGetTimeZone(DateFormatTest.java:70)
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 gov.nasa.jpf.util.test.TestJPF.runTests(TestJPF.java:496)
at gov.nasa.jpf.util.test.TestJPFHelper.runWithoutMain(TestJPFHelper.java:61)
at gov.nasa.jpf.util.test.TestJPFHelper.main(TestJPFHelper.java:43)
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 gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunTest.main(RunTest.java:79)
Caused by: java.lang.NullPointerException
at gov.nasa.jpf.jvm.ElementInfo.getReferenceField(ElementInfo.java:1037)
at gov.nasa.jpf.jvm.MJIEnv.getReferenceField(MJIEnv.java:477)
at gov.nasa.jpf.jvm.JPF_java_util_Locale.getLocale(JPF_java_util_Locale.java:41)
at gov.nasa.jpf.jvm.JPF_java_lang_String.toLowerCase__Ljava_util_Locale_2__Ljava_lang_String_2(JPF_java_lang_String.java:251)
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 gov.nasa.jpf.jvm.NativeMethodInfo.executeNative(NativeMethodInfo.java:148)
... 26 more
java.lang.AssertionError: JPF internal exception executing: gov.nasa.jpf.util.test.TestJPFHelper gov.nasa.jpf.test.java.text.DateFormatTest testSetAndGetTimeZone :gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.toLowerCase
at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:155)
at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:147)
at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:710)
at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:736)
at gov.nasa.jpf.test.java.text.DateFormatTest.testSetAndGetTimeZone(DateFormatTest.java:70)
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 gov.nasa.jpf.util.test.TestJPF.runTests(TestJPF.java:496)
at gov.nasa.jpf.util.test.TestJPFHelper.runWithoutMain(TestJPFHelper.java:61)
at gov.nasa.jpf.util.test.TestJPFHelper.main(TestJPFHelper.java:43)
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 gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunTest.main(RunTest.java:79)
......................................... test method failed with: JPF internal exception executing: gov.nasa.jpf.util.test.TestJPFHelper gov.nasa.jpf.test.java.text.DateFormatTest testSetAndGetTimeZone :gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.toLowerCase
......................................... testSetAndGetTimeZone: Failed
......................................... testing testFormatWithTimeZone()
running jpf with args: gov.nasa.jpf.util.test.TestJPFHelper gov.nasa.jpf.test.java.text.DateFormatTest testFormatWithTimeZone
JavaPathfinder v6.0 (rev 659) - (C) RIACS/NASA Ames Research Center
====================================================== system under test
application: gov/nasa/jpf/util/test/TestJPFHelper.java
arguments: gov.nasa.jpf.test.java.text.DateFormatTest testFormatWithTimeZone
====================================================== search started: 15/02/12 11:54
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.toLowerCase
at gov.nasa.jpf.jvm.NativeMethodInfo.executeNative(NativeMethodInfo.java:199)
at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:72)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:2223)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:2175)
at gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:712)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1775)
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 gov.nasa.jpf.util.test.TestJPF.runJPF(TestJPF.java:655)
at gov.nasa.jpf.util.test.TestJPF.createAndRunJPF(TestJPF.java:601)
at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:706)
at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:736)
at gov.nasa.jpf.test.java.text.DateFormatTest.testFormatWithTimeZone(DateFormatTest.java:83)
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 gov.nasa.jpf.util.test.TestJPF.runTests(TestJPF.java:496)
at gov.nasa.jpf.util.test.TestJPFHelper.runWithoutMain(TestJPFHelper.java:61)
at gov.nasa.jpf.util.test.TestJPFHelper.main(TestJPFHelper.java:43)
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 gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunTest.main(RunTest.java:79)
Caused by: java.lang.NullPointerException
at gov.nasa.jpf.jvm.ElementInfo.getReferenceField(ElementInfo.java:1037)
at gov.nasa.jpf.jvm.MJIEnv.getReferenceField(MJIEnv.java:477)
at gov.nasa.jpf.jvm.JPF_java_util_Locale.getLocale(JPF_java_util_Locale.java:41)
at gov.nasa.jpf.jvm.JPF_java_lang_String.toLowerCase__Ljava_util_Locale_2__Ljava_lang_String_2(JPF_java_lang_String.java:251)
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 gov.nasa.jpf.jvm.NativeMethodInfo.executeNative(NativeMethodInfo.java:148)
... 26 more
java.lang.AssertionError: JPF internal exception executing: gov.nasa.jpf.util.test.TestJPFHelper gov.nasa.jpf.test.java.text.DateFormatTest testFormatWithTimeZone :gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.toLowerCase
at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:155)
at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:147)
at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:710)
at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:736)
at gov.nasa.jpf.test.java.text.DateFormatTest.testFormatWithTimeZone(DateFormatTest.java:83)
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 gov.nasa.jpf.util.test.TestJPF.runTests(TestJPF.java:496)
at gov.nasa.jpf.util.test.TestJPFHelper.runWithoutMain(TestJPFHelper.java:61)
at gov.nasa.jpf.util.test.TestJPFHelper.main(TestJPFHelper.java:43)
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 gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunTest.main(RunTest.java:79)
......................................... test method failed with: JPF internal exception executing: gov.nasa.jpf.util.test.TestJPFHelper gov.nasa.jpf.test.java.text.DateFormatTest testFormatWithTimeZone :gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.toLowerCase
......................................... testFormatWithTimeZone: Failed
......................................... testing testConversionCycle()
running jpf with args: gov.nasa.jpf.util.test.TestJPFHelper gov.nasa.jpf.test.java.text.DateFormatTest testConversionCycle
JavaPathfinder v6.0 (rev 659) - (C) RIACS/NASA Ames Research Center
====================================================== system under test
application: gov/nasa/jpf/util/test/TestJPFHelper.java
arguments: gov.nasa.jpf.test.java.text.DateFormatTest testConversionCycle
====================================================== search started: 15/02/12 11:54
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.toLowerCase
at gov.nasa.jpf.jvm.NativeMethodInfo.executeNative(NativeMethodInfo.java:199)
at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:72)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:2223)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:2175)
at gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:712)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1775)
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 gov.nasa.jpf.util.test.TestJPF.runJPF(TestJPF.java:655)
at gov.nasa.jpf.util.test.TestJPF.createAndRunJPF(TestJPF.java:601)
at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:706)
at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:736)
at gov.nasa.jpf.test.java.text.DateFormatTest.testConversionCycle(DateFormatTest.java:36)
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 gov.nasa.jpf.util.test.TestJPF.runTests(TestJPF.java:496)
at gov.nasa.jpf.util.test.TestJPFHelper.runWithoutMain(TestJPFHelper.java:61)
at gov.nasa.jpf.util.test.TestJPFHelper.main(TestJPFHelper.java:43)
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 gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunTest.main(RunTest.java:79)
Caused by: java.lang.NullPointerException
at gov.nasa.jpf.jvm.ElementInfo.getReferenceField(ElementInfo.java:1037)
at gov.nasa.jpf.jvm.MJIEnv.getReferenceField(MJIEnv.java:477)
at gov.nasa.jpf.jvm.JPF_java_util_Locale.getLocale(JPF_java_util_Locale.java:41)
at gov.nasa.jpf.jvm.JPF_java_lang_String.toLowerCase__Ljava_util_Locale_2__Ljava_lang_String_2(JPF_java_lang_String.java:251)
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 gov.nasa.jpf.jvm.NativeMethodInfo.executeNative(NativeMethodInfo.java:148)
... 26 more
java.lang.AssertionError: JPF internal exception executing: gov.nasa.jpf.util.test.TestJPFHelper gov.nasa.jpf.test.java.text.DateFormatTest testConversionCycle :gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.toLowerCase
at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:155)
at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:147)
at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:710)
at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:736)
at gov.nasa.jpf.test.java.text.DateFormatTest.testConversionCycle(DateFormatTest.java:36)
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 gov.nasa.jpf.util.test.TestJPF.runTests(TestJPF.java:496)
at gov.nasa.jpf.util.test.TestJPFHelper.runWithoutMain(TestJPFHelper.java:61)
at gov.nasa.jpf.util.test.TestJPFHelper.main(TestJPFHelper.java:43)
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 gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunTest.main(RunTest.java:79)
......................................... test method failed with: JPF internal exception executing: gov.nasa.jpf.util.test.TestJPFHelper gov.nasa.jpf.test.java.text.DateFormatTest testConversionCycle :gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.toLowerCase
......................................... testConversionCycle: Failed
......................................... execution of testsuite: gov.nasa.jpf.test.java.text.DateFormatTest FAILED
.... [1] testSetAndGetTimeZone: Failed
.... [2] testFormatWithTimeZone: Failed
.... [3] testConversionCycle: Failed
--
Fatih Turkmen