jpf-core/bin/jpf config.jpf


--------------------------------------------------------------------------------


symbolic.min_int=-2147483648
symbolic.min_long=-9223372036854775808
symbolic.min_short=-32768
symbolic.min_byte=-128
symbolic.min_char=0
symbolic.max_int=2147483647
symbolic.max_long=9223372036854775807
symbolic.max_short=32767
symbolic.max_byte=127
symbolic.max_char=65535
symbolic.min_double=4.9E-324
symbolic.max_double=1.7976931348623157E308
JavaPathfinder core system v8.0 (rev 32) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
Main.main()

====================================================== search started: 7/29/18 4:03 PM
[SEVERE] JPF exception, terminating: exception in native method gov.nasa.jpf.ConsoleOutputStream.printf
java.util.IllegalFormatConversionException: c != java.lang.String
	at java.util.Formatter$FormatSpecifier.failConversion(Formatter.java:4302)
	at java.util.Formatter$FormatSpecifier.printCharacter(Formatter.java:2869)
	at java.util.Formatter$FormatSpecifier.print(Formatter.java:2757)
	at java.util.Formatter.format(Formatter.java:2520)
	at java.util.Formatter.format(Formatter.java:2455)
	at java.lang.String.format(String.java:2940)
	at gov.nasa.jpf.vm.MJIEnv.format(MJIEnv.java:1155)
	at gov.nasa.jpf.vm.JPF_gov_nasa_jpf_ConsoleOutputStream.printf__Ljava_lang_String_2_3Ljava_lang_Object_2__Ljava_io_PrintStream_2(JPF_gov_nasa_jpf_ConsoleOutputStream.java:137)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:125)
	at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:73)
	at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
	at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
	at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
	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:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	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 gov.nasa.jpf.ConsoleOutputStream.printf
	at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:186)
	at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:73)
	at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
	at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
	at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
	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:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at gov.nasa.jpf.tool.Run.call(Run.java:80)
	at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
Caused by: java.util.IllegalFormatConversionException: c != java.lang.String
	at java.util.Formatter$FormatSpecifier.failConversion(Formatter.java:4302)
	at java.util.Formatter$FormatSpecifier.printCharacter(Formatter.java:2869)
	at java.util.Formatter$FormatSpecifier.print(Formatter.java:2757)
	at java.util.Formatter.format(Formatter.java:2520)
	at java.util.Formatter.format(Formatter.java:2455)
	at java.lang.String.format(String.java:2940)
	at gov.nasa.jpf.vm.MJIEnv.format(MJIEnv.java:1155)
	at gov.nasa.jpf.vm.JPF_gov_nasa_jpf_ConsoleOutputStream.printf__Ljava_lang_String_2_3Ljava_lang_Object_2__Ljava_io_PrintStream_2(JPF_gov_nasa_jpf_ConsoleOutputStream.java:137)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:125)
	... 15 more