OpenJML (JML)

Using the command-line tool

Basic example

OpenJML can be invoked as a command in a command-shell environment. It requires that Java 1.7 and the java command are available. THe current release of OpenJML cannot be run with Java 8 or 9. The basic form is standard:

java -jar openjml.jar options files
The options and files may be intermingled. The files are listed just as they would be in a java compilation command; they may include .java and .jml files. files may include folders; listing a folder is equivalent to listing all .java and .jml files within the folder and its subfolders. Files and folders are written as absolute paths or as paths relative to the current working directory. [TBD - is the -dir option necessary?] The openjml.jar library need not be in the current working directory (as in the example above). You may give a relative or absolute path to the library instead.

Using directory paths

The discussion here describes how OpenJML uses the classpath, sourcepath, and specifications path to find class, source and specifications files.

Exit codes

The exit codes from the command-line version of OpenJML have these meanings:

• 0 (EXIT_OK) : successful operation, no errors, there may be warnings (including static checking warnings)
• 1 (EXIT_ERROR) : normal operation, but with errors (parsing or type-checking)
• 2 (EXIT_CMDERR) : an error in the formulation of the command-line, such as invalid options
• 3 (EXIT_SYSERR) : a system error, such as out of memory
• 4 (EXIT_ABNORMAL) : a fatal error, such as a program crash, caused by an internal bug

Command-line options

The commandline options follow the style of the OpenJDK compiler -- they begin with a single hyphen.

OpenJML (but not OpenJDK) options that require a parameter may either use an = followed directly by the argument or may provide the argument as the subsequent entry of the argument list. For example, either --racbin=output or --racbin output is permitted. If the argument is optional but present, the = form must be used.

Options that are boolean in nature can be enabled and disabled by either
1) adding a prefix -no, as in -showRacSource and -no-showRacSource
2) using the = form, as in -showRacSource=true and -showRacSource=false

Informational options

• -help: gives information about the command-line options and exits, with no further processing
• -version: gives the version of this OpenJML library and exits, with no further processing

Relevant Java compiler options

All the OpenJDK compiler options apply to OpenJML as well. The most commonly used or important OpenJDK options are listed here.

• -cp or -classpath: the parameter gives the classpath to use to find unnamed but referenced class files
• -sourcepath: the parameter gives the sequence of directories in which to find source files for unnamed but referenced classes
• -d: specifies the output directory for compiled files - the directory must exist
• -deprecation: enables warnings about the use of deprecated features (applies to JML features as well)
• -nowarn: shuts off all compiler warnings, including the static check warnings produced by ESC
• -Werror: turns all warnings into errors, including JML (and static check) warnings
• @filename: the given filename contains a list of arguments
• -source: specifies the Java version to use (default 1.7)
• -verbose: turn on Java verbose output
• -Xprefer:source or -Xprefer:newer: when both a .java and a .class file are present, whether to choose the .java (source) file or the file that has the more recent modification time
• -stopIfParseErrors: if enabled (disabled by default), processing stops after parsing if there are any parsing errors

OpenJML operational modes (mutually exclusive)

• -jml (default) : use the OpenJML implementation to process the listed files, including embedded JML comments and any .jml files
• -no-jml: uses the OpenJML implementation to type-check and possibly compile the listed files, but ignores all JML annotations in those files
• -java: processes the command-line options and files using only OpenJDK functionality. No OpenJML functionality is invoked. Must be the first option and overrides the others

JML operational modes (mutually exclusive)

• -check: (default) runs JML parsing and type-checking
• -esc: runs extended static checking
• -rac: compiles files with runtime assertions
• -doc: runs the jmldoc tool (not yet implemented)
• -command command: runs the given command, for arguments check, esc, rac, or doc; the default is \texttt{check}

Options applicable to all JML tasks

• -dir: Indicates that its argument is a directory. All the .java and .jml files in the directory and its subdirectories are processed.
• -dirs: Indicates that all subsequent command-line arguments are directories, to be processed as for -dir, until an argument is reached that begins with a hyphen.
• -specspath: the parameter gives the sequence of directories in which to find .jml specification files for unnamed but referenced classes
• -checkSpecsPath: if enabled (the default), warns about specspath elements that do not exist
• -keys: comma-separated list of the optional JML comment keys to enable
• -strictJML: (disabled by default) warns about the use of any OpenJML extensions to standard JML; disable with -no-strictJML
• -showNotImplemented: (disabled by default) warns about the use of features that are not implemented; disable with -no-showNotImplemented

Options related to parsing and type-checking

• -nullableByDefault: sets the global default to be that all declarations are implicitly @Nullable
• -nonnullByDefault: sets the global default to be that all declarations are implicitly @NonNull (the default)
• -purityCheck: enables (default on) checking for purity; disable with -no-purityCheck
• -internalSpecs: enables (default on) using the built-in library specifications; disable with -no-internalSpecs
• -internalRuntime: enables (default on) using the built-in runtime library; disable with -no-internalRuntime

Options specific to static checking

• -prover prover: the name of the prover to use: one of z3_4_3, yices2 [TBD: expand list]
• -exec path: the path to the executable corresponding to the given prover
• -boogie: enables using boogie (-prover option ignored; -exec must specify the Z3 executable)
• -method methodlist: a comma-separated list of method names to check (default is all methods in all listed classes) [TBD - describe wildcards and fully
• -exclude methodlist: a comma-separated list of method names to exclude from checking
• -checkFeasibility where: checks feasibility of the program at various points: one of none, all, exit [TBD, finish list, give default]
• -escMaxWarnings int: the maximum number of assertion violations to look for; the argument is either a positive integer or All (or equivalently all, default is All)
• -trace: prints out a counterexample trace for each failed assert
• -subexpressions: prints out a counterexample trace with model values for each subexpression
• -counterexample or -ce: prints out counterexample information

Options specific to runtime checking

• -showNotExecutable: warns about the use of features that are not executable (and thus ignored)
• -racShowSource: includes source location in RAC warning messages [ TBD: default? ]
• -racCheckAssumptions: enables (default on [TBD - is this default correct?]) checking assume statements as if they were asserts
• -racJavaChecks: enables (default on) performing JML checking of violated Java features (which will just proceed to throw an exception anyway)
• -racCompileToJavaAssert: (default off) compile RAC checks using Java asserts (which must then be enabled using -ea), instead of using org.jmlspecs.utils.JmlAssertionFailure
• -racPreconditionEntry: (default off) enable distinguishing internal Precondition errors from entry Precondition errors, appropriate for automated testing; compiles code to generate JmlAssertionError exceptions (rather than RAC warning messages)[TBD - should this turn on -racCheckAssumptions?]

Options that control output

• -quiet: turns off all output except errors and warnings. Equivalent to -verboseness=0
• -normal: quiet output plus a modest amount of informational and progress output. Equivalent to -verboseneness=1
• -progress: normal output plus output about progress through the phases of activity and the files being processed. Equivalent to -verboseneness=2
• -jmlverbose: progress output plus a verbose amount of output about the phases of activity and the files being processed. Equivalent to -verboseneness=3
• -jmldebug: output useful only for detailed debugging (includes the jmlverbose output). Equivalent to -verboseneness=4
• -verboseness level: sets the verbosity level (0-4)
• -show: prints out the various translated versions of the methods
• -verbose: enables openJDK output
• -jmltesting: adjusts the output so that test output is more stable

Last modified Nov 14 2025.