Hi,

I am attempting to install and run OpenJML to test it out for my study. The code example that I am using is the AddLoop class, which is successfully demo-ed on the rise4fun web site (https://www.rise4fun.com/OpenJMLESC/).

The JML type check is ok, but the ESC check fails for all three solvers mentioned on the OpenJML download web site: CVC4 (4.1.0-4.1.5), Z3 (4.3.2), and Yices (2.5.2). For CVC4, in particular, I could not find the version 1.2 that is mentioned in download page so I have to use the latest stable versions. I am using Windows 7, Oracle JDK 1.8, and Eclipse neon (4.6.0).

In short, the ESC check does not produce the same response as that on the rise4fun web site (i.e. the method satisfies the spec). This makes me wonder what back-end solver is actually used to run the rise4fun example on the web site?

The error messages for 3 solvers are listed below: 1/ CVC4 (with a red error message reported in the Problems view):

• In Trace view: Error occurred while checking method: AddLoop.AddLoop() error: An error while executing a proof script for : (error "Parse Error: :1.22: Expecting at least 2 arguments for operator 'DISTINCT', found 1")

2/ Yices (with a red error message reported in the Problems view):

• In Trace view: Error occurred while checking method: AddLoop.AddLoop() error: An error while executing a proof script for : (error "Error writing to solver: (declare-fun intValue (REF ) Int) java.io.IOException: The pipe is being closed")

3/ Z3 (withOUT any red errors being reported in Problems):

• In Trace view: Method and its specifications are infeasible: AddLoop.AddLoop()
• In Console view: C:\Users\IEUser\workspace\INT8028\src\AddLoop.java:18: Invalid assertion (LoopInvariant)

Please advise as to what could possibly be wrong here.

Thank you very much. Duc

Hi All,

I have been trying to use OpenJML on some popular leaf libraries such org.apache.commons.math3 to check method and specification consistency. I am attaching a toy example where the OpenJML-ESC/Java2 is reporting that method and specification is consistent. However that shouldn't be the case as the method being called here inserts an element into an array. So there should be possible index out of range warnings and so on. Can you please help me understand the possible reason behind this?

I get the impression from "Design by Contract with JML" that Person.java, Person.refines-java and PersonMain.java should form a first example program (since the square root example doesn't have a main). So I've copied them into a new directory, deleted the package declarations, compiled PersonMain and when I run it I get:

File "....\MySpecs\Person.java", line 47, character 12 error: Cannot throw "java.lang.IllegalArgumentException" it does not inherit from "java.lang.Throwable" [JLS 11.2]

Original comment by: ianbayley

Hello,

I've been using JML Runtime Assertion Checker, and there are some details in which I doesn't found an explanation in the JML Reference Manual, could any of you please clarify those?:

- Why the method clone is not pure in the specification of class Object?

• Why the quantified expressions are not allowed in 'assert' clause? (since version 5.5)
• Which is the semantic of including just an array position (like a[n]) in the clause 'assignable'?, I thought it would be that only that position is assignable but the tool doesn't complain when a method with this kind of specification assign another array position.
• How can I specify the bound of a recursive method? I tried with the 'measured_by' clause, but It doesn't complain when the bound doesn't decrease.
• Why the quantifier \max (with int variable) return 0 when the range is empty? isn't allowed negative values?

Gabriela Montoya.

Original comment by: gmontoya

I am compiling a simple demo with JML annotations and I get an internal error :

java -jar openjml.jar -rac ListSeq.java Seq.java ListSeq.java:47: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression } ^ ListSeq.java:47: Note: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression } ^ Internal JML bug - please report. BuildOpenJML-20131218-REV3178

java.lang.ArrayIndexOutOfBoundsException: 277

(see full error text attached)

Also find the two source files attached.

Original comment by: keith-foster

JML keywords such as "helper", "pure", etc are not allowed in model import statements. For example, the following file produces a parsing error.

//@ model import helper.*; public class Test { }

cheon@TRON] jml -Q Test.java Test.java:1:23 error: Syntax error: expecting an identifier, found 'helper'

This is unfortunate as some JML keywords (e.g., helper) are very likely to be used as package name. Three options are possible.

(1) Leave as it is. Seems too restrictive. (2) Selectively allow JML keywords (e.g., helper). (3) Allow all JML keywords.

I think the option (3) sounds proper. Any opinions?

Original comment by: cheon

I get the message "The system cannot find the path specified" when I run jmlc with the following classpath.

set CLASSPATH=S:\JML\bin\jmlruntime.jar;H:\U08186 \Week1;S:\JML\bin\jml-release.jar

I've changed the batch file to the following (because I want both versions of java):

@ECHO OFF rem @(#)$Date: 2004/01/27 20:40:27 $ rem rem jmlc -- script for running the JML runtime assertion checker compiler rem rem SYNOPSIS: set CLASSPATH and run JML runtime assertion checker compiler

call jmlenv.bat

rem save the old CLASSPATH set OLDCLASSPATH=%CLASSPATH% set CLASSPATH=.;%JMLDIR%\bin\jml-release.jar;% JMLDIR%\specs;%CLASSPATH%

set CMDLINE_ARGS=%1 :getargs shift if "%1"=="" goto endgetargs set CMDLINE_ARGS=%CMDLINE_ARGS% %1 goto getargs :endgetargs

rem You can use java' orjre -cp %CLASSPATH%' below rem but these have to be in your PATH

rem (used to be) java -mx128m org.jmlspecs.jmlrac.Main %CMDLINE_ARGS% S:\j2sdk1.4.2_09\bin\java -mx128m org.jmlspecs.jmlrac.Main %CMDLINE_ARGS%

rem restore the old CLASSPATH set CLASSPATH=%OLDCLASSPATH% set CMDLINE_ARGS= set OLDCLASSPATH=

rem Copyright (C) 2004 Iowa State University rem rem This file is part of JML rem rem JML is free software; you can redistribute it and/or modify rem it under the terms of the GNU General Public License as published by rem the Free Software Foundation; either version 2, or (at your option) rem any later version. rem rem JML is distributed in the hope that it will be useful, rem but WITHOUT ANY WARRANTY; without even the implied warranty of rem MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the rem GNU General Public License for more details. rem rem You should have received a copy of the GNU General Public License rem along with JML; see the file COPYING. If not, write to rem the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.

Original comment by: ianbayley

Sorry. but I only saw this bug tracker after submitting the following bug under request support. Specifically using the openJML Eclipse plug-in downloaded from http://jmlspecs.sourceforge.net/ on Eclipse 3.6.2 gives rise to the following internal bug.

/local/home/user/eclipse-helios/configuration/org.eclipse.osgi/bundles/716/1/.cp/java5/java/util/Calendar.jml:89: The field cachedLocaleData in the specification matches a Java field java.util.Calendar.cachedLocaleData with different modifiers: final private /@ spec_public @/ static Hashtable<Locale,int[]> cachedLocaleData; ^ /local/home/user/eclipse-helios/configuration/org.eclipse.osgi/bundles/716/1/.cp/java5/java/util/Calendar.jml:89: The field cachedLocaleData in the specification matches a Java field java.util.Calendar.cachedLocaleData but they have different types: Hashtable<Locale,int[]> vs. ConcurrentMap<Locale,int[]> private /@ spec_public @/ static Hashtable<Locale,int[]> cachedLocaleData; ^ Internal JML bug - please report. BuildOpenJML-20110212 java.lang.NullPointerException at com.sun.tools.javac.comp.JmlAttr.visitBlock(JmlAttr.java:555) at com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:784) at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:435) at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:422) at com.sun.tools.javac.comp.Attr.attribStat(Attr.java:484) at com.sun.tools.javac.comp.Attr.visitIf(Attr.java:1197) at com.sun.tools.javac.tree.JCTree$JCIf.accept(JCTree.java:1143) at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:435) at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:422) at com.sun.tools.javac.comp.Attr.attribStat(Attr.java:484) at com.sun.tools.javac.comp.Attr.attribStats(Attr.java:500) at com.sun.tools.javac.comp.Attr.visitBlock(Attr.java:863) at com.sun.tools.javac.comp.JmlAttr.visitBlock(JmlAttr.java:529) at com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:784) at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:435) at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:422) at com.sun.tools.javac.comp.Attr.attribStat(Attr.java:484) at com.sun.tools.javac.comp.Attr.attribClassBody(Attr.java:3138) at com.sun.tools.javac.comp.JmlAttr.attribClassBody(JmlAttr.java:442) at com.sun.tools.javac.comp.Attr.attribClass(Attr.java:3061) at com.sun.tools.javac.comp.JmlAttr.attribClass(JmlAttr.java:369) at com.sun.tools.javac.comp.JmlAttr.completeTodo(JmlAttr.java:414) at com.sun.tools.javac.comp.JmlAttr.attribClass(JmlAttr.java:406) at com.sun.tools.javac.comp.Attr.attribClass(Attr.java:2997) at com.sun.tools.javac.main.JavaCompiler.attribute(JavaCompiler.java:1156) at org.jmlspecs.openjml.JmlCompiler.attribute(JmlCompiler.java:359) at org.jmlspecs.openjml.JmlCompiler.attribute(JmlCompiler.java:368) at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:833) at org.jmlspecs.openjml.JmlCompiler.compile2(JmlCompiler.java:514) at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:802) at org.jmlspecs.openjml.JmlCompiler.compile(JmlCompiler.java:509) at com.sun.tools.javac.main.Main.compile(Main.java:418) at com.sun.tools.javac.main.Main.compile(Main.java:336) at org.jmlspecs.openjml.Main.compile(Main.java:364) at com.sun.tools.javac.main.Main.compile(Main.java:327) at org.jmlspecs.openjml.Main.execute(Main.java:319) at org.jmlspecs.openjml.Main.execute(Main.java:287) at org.jmlspecs.openjml.Main.execute(Main.java:274) at org.jmlspecs.openjml.Main.main(Main.java:248) ENDING with exit code 4

Original comment by: peteryhwong

The code is as follows:

/*@
 requires 0 <= len && len <= src.length-srcOfs && len <= dst.length;
 requires 0 <= srcOfs && srcOfs < src.length;
 ensures \forall int k;0 <= k && k < len;dst[k] == src[srcOfs + k];
 @*/
public static void CopyArray(final /*@non_null \readonly @*/ int [] src, final int srcOfs, /*@ non_null @*/int [] dst, final int len) {
	//@ loop_invariant \forall int k;0 <= k && k < i;dst[k] == src[srcOfs+k];
	//@ loop_invariant \forall int k;i <= k && k < dst.length; dst[k]==\old(dst[k]);
	//@ loop_invariant 0 <= i && i <= len;
	//@ decreasing len-i;
	for(int i = 0;i < len;i++) {
		dst[i] = src[srcOfs+i];
	}
}

Output from z3:

`... //@ loop_invariant \forall int k; 0 <= k && k < i; dst[k] == src[srcOfs + k]; VALUE: \forall int k; 0 <= k && k < i; dst[k] == src[srcOfs + k] === false

... LoopInvariant assertion: _JML__tmp211

... Invalid assertion (LoopInvariant) ` A very similar method however is proven correctly:

/*@
 requires src != null && dst != null && 0 <= len && len <= src.length && len <= dst.length;
 ensures src != null && dst != null;
 ensures \forall int k;0 <= k && k < len;dst[k] == src[k];
 @*/
public static void CopyArray(final int [] src, int [] dst, final int len) {
	//@ loop_invariant \forall int k;0 <= k && k < i;dst[k] == src[k];
	//@ loop_invariant 0 <= i && i <= len;
	//@ decreasing len-i;
	for(int i = 0;i < len;i++) {
		dst[i] = src[i];
	}
}

Seems that the problem is related to the index arithmetic srcOfs + k. I have tried many techniques, and searched everywhere to resolve this issue, but it seems that it is related to the prover.

Several times you run into this console output: warning: Failure while preparing VC: java.lang.NullPointerException Completed proof attempt of <method> [0.0] using yices

a) Can I trust "completed proof attempt..." or not? The time used 0.0 indicates that I can't trust it, but I'm not sure, since sometimes it uses some time. b) What null pointer? Is the null pointer in my implementation or in the OpenJML implementation? An output stating "Null pointer on line x would help.

Original comment by: *anonymous

Sorry to bother you guys again, but I'm trying to get our project compiling with JML. Maybe someone can enlighten me in relation to these problems....

As far as I understand, the JML compiler "extends" the MultiJava compiler. Maybe these problems are due to different interpretations of the JLS by: the compiler used by Eclipse and Sun's javac vs. the MultiJava compiler?
What do you think?

To give you an idea I'm getting messages such as the following:

- Cannot find method "java.io.PrintStream.println(double)"

- Cannot find method "java.io.PrintStream.print(char)"

- Cannot find method "java.lang.StringBuffer.replace(int, int, java.lang.String)"

• Cannot find method "java.lang.StringBuffer.append(int)

- Cannot find method "java.lang.StringBuffer.append (double)"

- Switch label must be constant value [JLS 14.9]

- Exception "java.io.FileNotFoundException" is not caught and does not appear in throws list [JLS 8.4.4]

In relation to the last point above, the exception would be thrown from a FileInputStream instance field in an anonymous inner class in a method. The method declares that it throws an IOException (superclass of FileInputStreamException) and this is good enough for both Eclipse and Suns compiler.

Any ideas?

Thanks.

Original comment by: shanleyr

When I try to run ESC on the attached CircleOperations.java file I get the following output: $ esc CircleOperations.java CircleOperations.java:9: verify: The prover cannot establish an assertion (InvariantLeaveCaller: /usr/local/openjml/specs/java/io/PrintStream.jml:42:) in method main: (Caller: CircleOperations.main(java.lang.String[]), Callee: java.io.PrintStream.println(int)) System.out.println(cops.id(79)); ^ /usr/local/openjml/specs/java/io/PrintStream.jml:42: verify: Associated declaration: CircleOperations.java:9: //-RAC@ public invariant outputText != null && \invariant_for(outputText); ^ CircleOperations.java:9: verify: The prover cannot establish an assertion (InvariantLeaveCaller: /usr/local/openjml/specs/java/io/PrintStream.jml:35:) in method main: (Caller: CircleOperations.main(java.lang.String[]), Callee: java.io.PrintStream.println(int)) System.out.println(cops.id(79)); ^ /usr/local/openjml/specs/java/io/PrintStream.jml:35: verify: Associated declaration: CircleOperations.java:9: //-RAC@ public static invariant \invariant_for(eol) && eol.length() > 0; ^ 4 verification failures $ esc --version openjml 0.17.0-alpha-15 $ uname -a Linux NEW-SURFACE 5.10.16.3-microsoft-standard-WSL2 #1 SMP Fri Apr 2 22:23:49 UTC 2021 x86_64 x86_64 x86_64 GNU/Linux CircleOperations.zip

In the following example, the JML block specification is ended by a */ inside a line comment:

class T {
  /*@ requires true;
      // commented out: ensures false; */
  void m() {}
}

This should parse and verify, i.e. the */ should indeed end the block comment/specification.

Instead, I get "error: A method or type declaration within a JML annotation must be model" for the void m() method. Or (in variations of the code above) I get "Expected a declaration or a JML construct inside the JML annotation here". Clearly, the OpenJML parser does not recognise the */ as the end of the JML annotation.

This happened on OpenJML version 0.8.59 as well as 0.17.0-alpha-15.

Putting the */ on a new line solves the issue.

Note that e.g. javac (Version 11) has no problem compiling this code, i.e. it is valid Java.

I am attempting to use the API in a project however I am unable to use the API. The project is running using the modified OpenJDK provided in the releases. I would appreciate any advice if the error is on my end.

My source code:

public class MainApp
{
    public static void main( String[] args ) throws Exception
    {
        IAPI api = Factory.makeAPI("-progress -verbose");
        api.execute(null, "-cp", "src/main/java/", "src/main/java/MaxBad.java");
    }
}

The error:

error: The compiler aborted with an uncaught exception: java.lang.NullPointerException: Cannot invoke "org.jmlspecs.openjml.IAPI$IProofResultListener.setListener(org.jmlspecs.openjml.IAPI$IProofResultListener)" because the return value of "com.sun.tools.javac.util.Context.get(java.lang.Class)" is null
java.lang.NullPointerException: Cannot invoke "org.jmlspecs.openjml.IAPI$IProofResultListener.setListener(org.jmlspecs.openjml.IAPI$IProofResultListener)" because the return value of "com.sun.tools.javac.util.Context.get(java.lang.Class)" is null
	at jdk.compiler/org.jmlspecs.openjml.Main.setProofResultListener(Main.java:645)
	at jdk.compiler/org.jmlspecs.openjml.Main.compile(Main.java:516)
	at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:178)
	at jdk.compiler/org.jmlspecs.openjml.Main.executeNS(Main.java:473)
	at jdk.compiler/org.jmlspecs.openjml.API.execute(API.java:222)
	at MainApp.main(MainApp.java:21)

My set-up:

• Macbook M1 macOS 13.0.1 (arm64)
• IntelliJ IDEA 2022.2.3 (however, error re-created using terminal using openjml script provided in releases).

The following error occurs when running ESC on the Google Guava library.

error: A catastrophic JML internal error occurred.  Please report the bug with as much information as you can.
  Reason: Unexpected exception: Exception during parsing near ct object) {
        if (object instanceof StringConverter) {
   java.lang.NullPointerException: Cannot invoke "org.jmlspecs.openjml.IJmlClauseKind$ModifierKind.isTypeAnnotation()" because "ja.kind" is null
java.lang.NullPointerException: Cannot invoke "org.jmlspecs.openjml.IJmlClauseKind$ModifierKind.isTypeAnnotation()" because "ja.kind" is null
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.extractTypeAnnotations(JmlParser.java:369)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.formalParameter(JmlParser.java:385)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.formalParameters(JavacParser.java:4534)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.formalParameters(JavacParser.java:4526)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.formalParameters(JmlParser.java:403)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.methodDeclaratorRest(JavacParser.java:4409)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classOrInterfaceOrRecordBodyDeclaration(JavacParser.java:4273)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classOrInterfaceOrRecordBodyDeclaration(JmlParser.java:1196)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classInterfaceOrRecordBody(JavacParser.java:4154)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classInterfaceOrRecordBody(JmlParser.java:615)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classDeclaration(JavacParser.java:3866)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classDeclaration(JmlParser.java:625)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classOrRecordOrInterfaceOrEnumDeclaration(JavacParser.java:3806)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classOrRecordOrInterfaceOrEnumDeclaration(JmlParser.java:443)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classOrInterfaceOrRecordBodyDeclaration(JavacParser.java:4205)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classOrInterfaceOrRecordBodyDeclaration(JmlParser.java:1196)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.enumBody(JavacParser.java:4051)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.enumDeclaration(JavacParser.java:3983)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classOrRecordOrInterfaceOrEnumDeclaration(JavacParser.java:3812)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classOrRecordOrInterfaceOrEnumDeclaration(JmlParser.java:443)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.typeDeclaration(JavacParser.java:3791)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.parseCompilationUnit(JavacParser.java:3635)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.parseCompilationUnit(JmlParser.java:265)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.parse(JavaCompiler.java:620)
	at jdk.compiler/com.sun.tools.javac.main.JmlCompiler.parse(JmlCompiler.java:211)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.parseFiles(JavaCompiler.java:1009)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.parseFiles(JavaCompiler.java:996)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:922)
	at jdk.compiler/com.sun.tools.javac.main.JmlCompiler.compile(JmlCompiler.java:197)
	at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:321)
	at jdk.compiler/org.jmlspecs.openjml.Main.compile(Main.java:534)
	at jdk.compiler/org.jmlspecs.openjml.Main.execute(Main.java:374)
	at jdk.compiler/org.jmlspecs.openjml.Main.execute(Main.java:332)
	at jdk.compiler/org.jmlspecs.openjml.Main.main(Main.java:295)
	at jdk.compiler/com.sun.tools.javac.Main.main(Main.java:53)

Steps to reproduce:

1. Clone the Google Guava library https://github.com/google/guava (as of this writing, the latest commit ID on main was d48418e4528ad0323e51e34d4e1044cc03c77c98)
2. From the root of the Guava repo, cd guava
3. Run mvn clean compile and mvn dependency:copy-dependencies
4. Run openjml --class-path "target/dependency/*" --esc --dir guava/src/com/google/common/base --method "Strings.nullToEmpty"
5. Observe the error above

Hi David, I am using OpenJML to perform static verification on the apache commons collections4. An internal error is returned once the command is used. For more information, please refer to the information attached below.

Version: openjml 0.17.0-alpha-15 Command: openjml -esc --dir=path_to_src Error message:

error: A catastrophic JML internal error occurred.  Please report the bug with as much information as you can.
  Reason: Unexpected exception: Exception during parsing near ... coll2) {
          if (coll1.size() < coll2.length) {
     java.lang.NullPointerException: Cannot invoke "org.jmlspecs.openjml.IJmlClauseKind$ModifierKind.isTypeAnnotation()" because "ja.kind" is null
java.lang.NullPointerException: Cannot invoke "org.jmlspecs.openjml.IJmlClauseKind$ModifierKind.isTypeAnnotation()" because "ja.kind" is null
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.extractTypeAnnotations(JmlParser.java:369)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.formalParameter(JmlParser.java:385)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.formalParameters(JavacParser.java:4546)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.formalParameters(JavacParser.java:4526)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.formalParameters(JmlParser.java:403)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.methodDeclaratorRest(JavacParser.java:4409)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classOrInterfaceOrRecordBodyDeclaration(JavacParser.java:4273)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classOrInterfaceOrRecordBodyDeclaration(JmlParser.java:1196)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classInterfaceOrRecordBody(JavacParser.java:4154)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classInterfaceOrRecordBody(JmlParser.java:615)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classDeclaration(JavacParser.java:3866)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classDeclaration(JmlParser.java:625)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classOrRecordOrInterfaceOrEnumDeclaration(JavacParser.java:3806)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classOrRecordOrInterfaceOrEnumDeclaration(JmlParser.java:443)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.typeDeclaration(JavacParser.java:3791)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.parseCompilationUnit(JavacParser.java:3635)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.parseCompilationUnit(JmlParser.java:265)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.parse(JavaCompiler.java:620)
	at jdk.compiler/com.sun.tools.javac.main.JmlCompiler.parse(JmlCompiler.java:211)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.parseFiles(JavaCompiler.java:1009)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.parseFiles(JavaCompiler.java:996)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:922)
	at jdk.compiler/com.sun.tools.javac.main.JmlCompiler.compile(JmlCompiler.java:197)
	at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:321)
	at jdk.compiler/org.jmlspecs.openjml.Main.compile(Main.java:534)
	at jdk.compiler/org.jmlspecs.openjml.Main.execute(Main.java:374)
	at jdk.compiler/org.jmlspecs.openjml.Main.execute(Main.java:332)
	at jdk.compiler/org.jmlspecs.openjml.Main.main(Main.java:295)
	at jdk.compiler/com.sun.tools.javac.Main.main(Main.java:53)
1 error

This is an initial support of translation from Java/JML into Rapid/SMT-LIB.

I added a few new options (-jml2rapid, -mName, -outputDir). The major contribution is org.jmlspecs.openjml.translation package.