escjava - Checks Java source files for possible errors
escjava options source_filename...
The escjava command takes a list of Java source files (i.e., filename.java) and checks the classes contained within those files for possible errors. If the -depend option is supplied, then any class on which a checked class depends will also be checked.
More information can be obtained from the ESC/Java User's Manual, which is provided as Technical Note 2000-002, Compaq Systems Research Center.
- -bootclasspath path
- Overrides escjava's built-in path for locating .spec and .class files for the system classes (java.lang.String, etc.) with path. This option is provided so that files may be checked against a different version of JDK than the one escjava comes with (currently a version of JDK 1.2 augmented with a limited number of spec files). Note: if the -v option is supplied, escjava will print the complete classpath it is using when it starts up.
- -classpath path
- Sets the path to be used to locate user classes not supplied on the command line to path. Overrides all previous -classpath options and the CLASSPATH environment variable. The actual classpath escjava uses is the user path followed by the bootclasspath (see -bootclasspath); this allows users to add new .spec files for the system classes. Note: if the -v option is supplied, escjava will print the complete classpath it is using when it starts up.
- -counterexample
- Causes a pretty printed version of the counterexample context to be displayed after each warning message. Elements of the counterexample context that are almost certainly irrelevant are not printed. Use the -pcc option to get the raw, unadulterated counterexample context.
- -depend
- Normally, escjava checks only the classes contained in the source files given to it on the command line. If the -depend option is given, however, escjava also checks any classes on which those classes depend (including indirectly).
- -f file
- Instructs escjava to append to the list of source files given directly on the command line the files named on separate lines in file. Multiple -f flags may be used.
- -loop n
- Instructs escjava to unroll loops n iterations. The number of iterations n can be specified in increments of one half; more precisely, the syntax of n is a natural number optionally followed by .0 or .5. A "half" iteration consists of evaluating the initial guard, if any. The default value for n is 1.5. For faster, less thorough checking, consider using a value of 1.
- -nocheck
- Causes no extended static checking to be done. Syntax and Java type checking as well as verification-condition generation is still performed, however.
- -notrace
- Do not print the execution trace that leads to the potential error being warned about.
- -nowarn category
- Turns off all extended static checking of type category. See the user manual for a complete list of valid categories. If category is All, turns off all checking, which can be a useful option in conjunction with the -warn switch.
- -plainwarning
- By default, escjava will sometimes accompany an error message with selected details of the counterexample it found. The -plainwarning option suppresses this information; this may be helpful when escjava's output is to be fed to a program.
- -quiet
- Turns off display of the progress messages that escjava normally prints.
- -routine routinename
- If -routine is used, escjava checks only the routines specified by -routine arguments. The routinename can either be a simple method or constructor name (which specifies all routines with this name), or a fully qualified routine signature (which specifies a routine uniquely). For example, routinename may be String or java.lang.String.String(char[],int,int).
- -routineIndirect file
- This option is equivalent to having the -routine flag present and using each line of file as an argument to -routine.
- -start n
- This option causes escjava to start checking the first file on the command line at line number n. (Later files are checked from the beginning as normal.) Starting checking at line n means that all possible warnings before line n are automatically nowarned. (Only the possible warnings themselves are so nowarned, not their associated declarations. For example, escjava may still issue a warning that a method declared after line n fails to maintain an invariant declared before line n.) Since no warnings would be produced for types and type members whose declarations end before line n, these are skipped.
- -suggest
- After each warning, suggest an annotation that will suppress the warning. Although it is human-readable, the suggestion is mainly intended for use by the ESC/Java Annotation Wizard. Note: the suggestion may or may not correspond to the programmer's intended design, so it may be inappropriate to actually follow the suggestion.
- -v
- Turns on verbose mode, which causes escjava to print additional information that may be helpful in some cases, for example when debugging problems related to the classpath (since verbose mode prints the complete classpath).
- -vclimit n
- Sets the maximum size verification condition that escjava will attempt to verify. Defaults to 500,000. This limit exists to handle the rare cases where escjava generates exponential-size VCs.
- -warn category
- Turns on all extended static checking of type category if it is currently turned off. See the user manual for a complete list of valid categories.
Source-file line numbers are counted starting at 1, while column numbers are counted starting at 0, treating tabs as one character each. When source is displayed, however, tabs are expanded using 8-space tab stops.
For more information, see the user's manual, and especially the section entitled Warnings.
The following environment variables affect the execution of escjava:
- CLASSPATH
- If set, specifies the path to be used to locate user classes not supplied on the command line. Defaults to the current working directory. The -classpath option overrides this variable. Where to find the system classes is specified separately using the -bootclasspath option.
- ESCJ_SIMPLIFY
- If set, specifies the pathname to use to invoke the Simplify Theorem prover.
- ESCJ_SIMPLIFY_ARGS
- If set, specifies the arguments to pass to the Simplify Theorem prover when it is invoked. Defaults to "-noprune -noplunge".
- ESCJ_STDARGS
- If set, specifies a set of default escjava arguments. These arguments will be processed before any command-line arguments. Currently defaults to "-nowarn Deadlock".
- PROVER_CC_LIMIT
- If set, specifies the maximum number of warnings to generate per routine. Should be set to a positive integer. Defaults to 10.
- PROVER_KILL_TIME
- If set, specifies a rough upper bound of how many seconds escjava should spend attempting to prove error free any given method or constructor. Should be set to a positive integer greater than 50. Defaults to 300 (5 minutes).
- escjava/examples/
- This directory, where escjava denotes the directory into which escjava is installed, contains example code.
- escjava/lib/specs/
- This directory, where escjava denotes the directory into which escjava is installed, contains .spec files for selected JDK library types. It is considered part of the system libraries by escjava and is thus included as part of the bootclasspath (see the -bootclasspath flag above).
This page was generated automatically by mtex software.CLASSPATH, JAVA(5)