Tests for DateFormat

[Fatih Turkmen]

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

[Peter Mehlitz]

Java 1.7 is currently a problem since the library behaviors seem to have changed significantly and some of the implementations (OS X) aren't stabilized yet. Your case seems to be caused by a null Locale, which is probably due to not using en_US.

I currently don't have time to work on Java 1.7 issues, but I add it to the list.

-- Peter

> ....

[Fatih Turkmen]

Hi Peter,

Thanks for the response. I understand that Java 1.7 is a bit ahead of time.
I spotted this point while I was trying to reproduce my problem in an environment where
1.7 was installed. However my problem is related to DateFormat.
I think I asked the same question once more however I would like to rephrase it
because it seems like there is something wrong (at least IMHO) with the DateFormat
peer in JPF.

My code works perfectly fine when executed alone. It calls a method of a very simple
library that parses a given string with a DateFormat parser (i.e. SimpleDateFormat).
However when executed with JPF it throws a ParseException, and of course returning
null, setting ParsePosition to its initial value. I tried several possibilities as you suggested
like setting locale etc but they don't seem like helping.
Here is the code I have problem with:

strictParse(DateFormat parser, String str){
ParsePosition pos = new ParsePosition(0);
Date ret;
synchronized (parser) {
       ret = parser.parse(str, pos);
}
if (pos.getIndex() != str.length())
            throw new ParseException("", 0);
}

Now if you call this method with a simple string such as "1970-01-01T08:00:00",
JPF seems to cause ParseException, although the code alone works fine.

I am now checking the peer method to see whether there is something I am doing
or there is a problem with the peer (i.e. parse__Ljava_lang_String_2__Ljava_util_Date_2).
Do you have any idea on the issue?

Thanks.

--
Fatih

[Fatih Turkmen]

Hi,

I realized that there is no peer for the parse method with ParsePosition parameter...
parse(str) is available but not parse(str, pos).

Thanks.

--
Fatih Turkmen

Web: http://sites.google.com/site/fturkmen/