Exception raised when running String.join()

[Qiuchen Yan]

Hi,

I'm doing some work related to the string support of SPF, and has tested several Java string functions under SPF.

As shown below, when running a test for String.join(), SPF raised some weird exceptions.

============== error 1 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty java.lang.ClassNotFoundException: class not found: java.lang.NoSuchMethodException!!    at testJoin.foo(testJoin.java:13)    at testJoin.main(testJoin.java:6)

============== snapshot #1 thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack:    at testJoin.foo(testJoin.java:13)    at testJoin.main(testJoin.java:6)

============== results error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ClassNotFoundException: class not found:..."

The test example is attached, together with the configure file the full log. This exception is reproducable under the latest SPF in https://github.com/SymbolicPathFinder/jpf-symbc

[Johann Glock]

Hi Quichen,

you're getting this exception because String.join is not implemented in the JPF model of the String class, which can be found at jpf-core/src/classes/java/lang/String.java.

To fix the error, you'd have to add the missing String.join method to the mentioned model class.

For further reading on model classes etc., see the "Model Java Interface" documentation in the jpf-core wiki.

Note that according to https://github.com/javapathfinder/jpf-core/issues/313, methods are added to the model classes "when needed", so you might find some other missing methods if you keep working with JPF/SPF. If you get around to adding implementations for any missing methods you find, feel free to submit a PR with your changes to the jpf-core GitHub. :)