#54 Using RAC and ESC in command line

[Peter Wong]

I am experimenting with ESC and RAC features provided by OpenJML. However, I come to some issues with using these features.

For ESC, I use the following command, where the corresponding OpenJML jar files are downloaded from http://jmlspecs.sourceforge.net/openjml.tar.gz and yices is obtained from http://yices.csl.sri.com/cgi-bin/yices-newlicense.cgi?file=yices-1.0.31-x86_64-pc-linux-gnu-static-gmp.tar.gz

/usr/java/jdk1.7.0/bin/java -Dopenjml.defaultProver=yices -Dopenjml.prover.yices=<path to yices executable> -jar <path-to-openjml.jar> -noPurityCheck -specspath <path-to-jmlspec.jar> -noInternalSpecs -noInternalRuntime -cp <path-to-jmlruntimejar> -dir <dir-of-C.java> -command esc

I get the following

Internal JML bug - please report. BuildOpenJML-20111005
java.lang.NoClassDefFoundError: org/smtlib/IVisitor$VisitorException
at org.jmlspecs.openjml.JmlCompiler.esc(JmlCompiler.java:482)
at org.jmlspecs.openjml.JmlCompiler.desugar(JmlCompiler.java:346)
at com.sun.tools.javac.main.JavaCompiler.desugar(JavaCompiler.java:1280)
at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:866)
at org.jmlspecs.openjml.JmlCompiler.compile2(JmlCompiler.java:527)
at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:835)
at com.sun.tools.javac.main.Main.compile(Main.java:417)
at com.sun.tools.javac.main.Main.compile(Main.java:331)
at org.jmlspecs.openjml.Main.compile(Main.java:367)
at com.sun.tools.javac.main.Main.compile(Main.java:322)
at org.jmlspecs.openjml.Main.execute(Main.java:322)
at org.jmlspecs.openjml.Main.execute(Main.java:288)
at org.jmlspecs.openjml.Main.execute(Main.java:275)
at org.jmlspecs.openjml.Main.main(Main.java:248)
Caused by: java.lang.ClassNotFoundException: org.smtlib.IVisitor$VisitorException
at java.net.URLClassLoader$1.run(URLClassLoader.java:366)
at java.net.URLClassLoader$1.run(URLClassLoader.java:355)
at java.security.AccessController.doPrivileged(Native Method)
at java.net.URLClassLoader.findClass(URLClassLoader.java:354)
at java.lang.ClassLoader.loadClass(ClassLoader.java:423)
at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:308)
at java.lang.ClassLoader.loadClass(ClassLoader.java:356)
... 14 more

If I run RAC I use the following command where OpenJML and Yices are obtained from the same places as indicated above

/usr/java/jdk1.7.0/bin/java -Dopenjml.defaultProver=yices -Dopenjml.prover.yices=<path to yices executable> -jar <path-to-openjml.jar> -noPurityCheck -specspath <path-to-jmlspec.jar> -noInternalSpecs -noInternalRuntime -cp <path-to-jmlruntimejar> -dir <dir-of-C.java> -command rac

and get the following error

Internal JML bug - please report. BuildOpenJML-20111005
java.lang.NullPointerException
at com.sun.tools.javac.comp.JmlRac.visitMethodDef(JmlRac.java:2508)
at com.sun.tools.javac.comp.JmlRac.visitJmlMethodDecl(JmlRac.java:2638)
at org.jmlspecs.openjml.JmlTree$JmlMethodDecl.accept(JmlTree.java:1040)
at com.sun.tools.javac.tree.TreeTranslator.translate(TreeTranslator.java:58)
at com.sun.tools.javac.tree.TreeTranslator.translate(TreeTranslator.java:70)
at com.sun.tools.javac.tree.TreeTranslator.visitClassDef(TreeTranslator.java:134)
at com.sun.tools.javac.comp.JmlRac.visitClassDef(JmlRac.java:1428)
at com.sun.tools.javac.comp.JmlRac.visitJmlClassDecl(JmlRac.java:1491)
at org.jmlspecs.openjml.JmlTree$JmlClassDecl.accept(JmlTree.java:986)
at com.sun.tools.javac.tree.TreeTranslator.translate(TreeTranslator.java:58)
at org.jmlspecs.openjml.JmlCompiler.rac(JmlCompiler.java:452)
at org.jmlspecs.openjml.JmlCompiler.desugar(JmlCompiler.java:352)
at com.sun.tools.javac.main.JavaCompiler.desugar(JavaCompiler.java:1280)
at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:866)
at org.jmlspecs.openjml.JmlCompiler.compile2(JmlCompiler.java:527)
at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:835)
at com.sun.tools.javac.main.Main.compile(Main.java:417)
at com.sun.tools.javac.main.Main.compile(Main.java:331)
at org.jmlspecs.openjml.Main.compile(Main.java:367)
at com.sun.tools.javac.main.Main.compile(Main.java:322)
at org.jmlspecs.openjml.Main.execute(Main.java:322)
at org.jmlspecs.openjml.Main.execute(Main.java:288)
at org.jmlspecs.openjml.Main.execute(Main.java:275)
at org.jmlspecs.openjml.Main.main(Main.java:248)

[Peter Wong]

The Java source file I try to run ESC and RAC on