Java path finder and exception in native method java.text.DateFormat.parse

[Jiří Vahala]

Hello everybody! 

I am trying JPF for the first time and I am experiencing some sort of difficulties. I had lot of problems with System.getProperty methods, but I've already solved them, anyway, now I am dealing with new issue: 

====================================================== search started: 19/03/15 14:32

[SEVERE] JPF exception, terminating: exception in native method java.text.DateFormat.parse

gov.nasa.jpf.vm.ClinitRequired: java.util.Date

at gov.nasa.jpf.vm.MJIEnv.newElementInfo(MJIEnv.java:1038)

at gov.nasa.jpf.vm.MJIEnv.newElementInfo(MJIEnv.java:1067)

at gov.nasa.jpf.vm.MJIEnv.newObject(MJIEnv.java:1074)

at gov.nasa.jpf.vm.JPF_java_text_DateFormat.parse__Ljava_lang_String_2__Ljava_util_Date_2(JPF_java_text_DateFormat.java:62)

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:120)

at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:73)

at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1941)

at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1858)

at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:761)

at gov.nasa.jpf.vm.VM.forward(VM.java:1722)

at gov.nasa.jpf.search.Search.forward(Search.java:579)

at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)

at gov.nasa.jpf.JPF.run(JPF.java:613)

at gov.nasa.jpf.JPF.start(JPF.java:189)

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.tool.Run.call(Run.java:80)

at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)

---------------------- JPF error stack trace ---------------------

gov.nasa.jpf.JPFNativePeerException: exception in native method java.text.DateFormat.parse

at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:180)

at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:73)

at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1941)

at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1858)

at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:761)

at gov.nasa.jpf.vm.VM.forward(VM.java:1722)

at gov.nasa.jpf.search.Search.forward(Search.java:579)

at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)

at gov.nasa.jpf.JPF.run(JPF.java:613)

at gov.nasa.jpf.JPF.start(JPF.java:189)

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.tool.Run.call(Run.java:80)

at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)

Caused by: gov.nasa.jpf.vm.ClinitRequired: java.util.Date

at gov.nasa.jpf.vm.MJIEnv.newElementInfo(MJIEnv.java:1038)

at gov.nasa.jpf.vm.MJIEnv.newElementInfo(MJIEnv.java:1067)

at gov.nasa.jpf.vm.MJIEnv.newObject(MJIEnv.java:1074)

at gov.nasa.jpf.vm.JPF_java_text_DateFormat.parse__Ljava_lang_String_2__Ljava_util_Date_2(JPF_java_text_DateFormat.java:62)

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:120)

... 15 more

and I have no idea what to do with it. Can anybody help me, how can I solve it? (BTW, parsing date is somewhere in 3rd-party libs.)

[PETER C MEHLITZ]

thanks - it's a missing test for required class init in the DateFormat peer. Will fix.
As a temporary workaround you can reference java.util.Date from your code before it calls the lib.

-- Peter

> --
>
> ---
> You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Jiří Vahala]

thanks! 

Dne čtvrtek 19. března 2015 16:51:43 UTC+1 pcmehlitz napsal(a):