crash when java file not found

[davidcok]

[ Files are in the gitbug573 test ]

Using these files and this command:

java -jar $OJ/openjml.jar -sourcepath /home/caro/PruebasTesina/src/ /home/caro/PruebasTesina/src/pckg/A.jml

The output is this:

warning: There is no java file on the sourcepath corresponding to the given jml file: /home/caro/PruebasTesina/src/pckg/A.jml
Internal JML bug - please report. BuildOpenJML-0.8.23-20170930
java.lang.IllegalStateException: endPosTable already set
at com.sun.tools.javac.util.DiagnosticSource.setEndPosTable(DiagnosticSource.java:136)
at com.sun.tools.javac.util.Log.setEndPosTable(Log.java:350)
at com.sun.tools.javac.main.JavaCompiler.parse(JavaCompiler.java:672)
at org.jmlspecs.openjml.JmlCompiler.parseSingleFile(JmlCompiler.java:225)
at org.jmlspecs.openjml.JmlCompiler.parse(JmlCompiler.java:137)
at com.sun.tools.javac.main.JavaCompiler.parse(JavaCompiler.java:670)
at com.sun.tools.javac.main.JavaCompiler.complete(JavaCompiler.java:778)
at com.sun.tools.javac.main.JavaCompiler$1.complete(JavaCompiler.java:317)
at com.sun.tools.javac.jvm.ClassReader.fillIn(ClassReader.java:2535)
at com.sun.tools.javac.jvm.ClassReader.complete(ClassReader.java:2442)
at com.sun.tools.javac.jvm.ClassReader.access$0(ClassReader.java:2429)
at com.sun.tools.javac.jvm.ClassReader$1.complete(ClassReader.java:240)
at com.sun.tools.javac.code.Symbol.complete(Symbol.java:574)
at com.sun.tools.javac.code.Symbol$ClassSymbol.complete(Symbol.java:1037)
at com.sun.tools.javac.jvm.ClassReader.loadClass(ClassReader.java:2623)
at com.sun.tools.javac.comp.JmlEnter.matchClassesForBinary(JmlEnter.java:403)
at com.sun.tools.javac.compJmlEnter.visitTopLevel(JmlEnter.java:226)
at com.suntools.javac.tree.JCTree$JCCompilationUnit.accept(JCTree.java:518)
at org.jmlspecs.openjml.JmlTree$JmlCompilationUnit.accept(JmlTree.java:904)
at com.sun.tools.javac.comp.Enter.classEnter(Enter.java:258)
at com.sun.tools.javac.comp.JmlEnter.classEnter(JmlEnter.java:469)
at com.sun.tools.javac.comp.Enter.complete(Enter.java:486)
at com.sun.tools.javac.comp.Enter.main(Enter.java:471)
at comsun.tools.javac.comp.JmlEnter.main(JmlEnter.java:774)
at com.sun.tools.javac.main.JavaCompiler.enterTrees(JavaCompiler.java:992)
at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:864)
at com.sun.tools.javac.main.Main.compile(Main.java:553)
at com.sun.tools.javac.mainMain.compile(Main.java:410)
at org.jmlspecs.openjml.Main.compile(Main.java:560)
at com.sun.tools.javac.main.Main.compile(Main.java:399)
at com.sun.tools.javacmain.Main.compile(Main.java:390)
at org.jmlspecs.openjml.Main.execute(Main.java:396)
at org.jmlspecs.openjml.Main.execute(Main.java:354)
at org.jmlspecs.openjml.Main.execute(Main.java:341)
at org.jmlspecs.openjml.Main.main(Main.java:313)

As it often happens, only after asking for help I found a way to make it work. So this command:

java -jar $OJ/openjml.jar -sourcepath /home/caro/PruebasTesina/src/ -specspath /home/caro/PruebasTesina/src/ /home/caro/PruebasTesina/src/pckg/A.java

Does work as expected.

[davidcok]

Fixed in V0.8.24