JSR 308 Checkers and Framework

Version 0.1.1 (7 Jun 2007)

Contents:

Introduction

This distribution contains

This document describes how to use the provided plug-ins. If you wish to write your own compiler plug-in, you should first read this document, and then read How to write a JSR 308 checker plug-in.

Finding bugs with a compiler plug-in is a two-step process.

  1. A programmer writes annotations that specify additional information about Java types. For instance, a @NonNull annotation may specify that a variable should never have a null value, and a @Interned annotation may specify that a variable only holds interned values.
  2. The programmer runs the compiler plug-in, which reports whether the program contains any code that is inconsistent with the annotations. For instance, a null-checking plug-in might verify the absence of null pointer exceptions (or show where in the program they might occur), and an interning-checking plug-in might verify the absence of equality test errors (or show where in the program they might occur).

Installation

You must install the JSR 308 Java compiler before you can use the checkers or the framework. JSR 308 extends the Java language to permit annotations to appear on types.

Then, follow these steps to install the checkers and the framework.

  1. Download the checkers and framework: jsr308-checkers.zip.
  2. Unzip the distribution zipfile, which creates a checkers directory. We recommend that you do this in the parent of the JSR 308 compiler directory, so that the compiler and checkers directories are siblings.
  3. Edit the checkers/build.properties file so that the "compiler.lib" property specifies the location of the JSR 308 javac.jar library.
    (If the compiler and checkers directories are siblings, no edits are necessary.)
  4. Build the checkers.jar library by running "ant" in the checkers directory: 
      cd checkers
  ant dist
  5. Add the checkers.jar file (which is produced by a successful build) to your classpath.
  6. Test that everything works by running the NonNull checker examples.

Distribution contents

The checkers directory contains the following resources:
File Description
src source code for the checkers and framework
examples source file examples that use type annotations and can be checked by compiler plug-ins
build.xml an Ant build file for compiling the library
build.properties a configuration file for the build process

Using a checker

To run a checker (also known as a type-checking compiler plug-in, or an annotation processor), run javac as usual, but pass the -typeprocessor plug-in_class command-line option: 

  javac -typeprocessor plug-in_class ...

For an example command line, see the NonNull checker documentation.

You can always compile the code without the -typeprocessor command-line option, but in that case no checking of the type annotations is performed.

When writing source code with annotations, typically you will add 

import checkers.quals.*;

at the top of the source file, so that you can use annotations such as @NonNull instead of @checkers.quals.NonNull.

Checking against unannotated code

A checker plug-in reads annotations that appear in the source code or .class files of classes that are used by the code being compiled and checked. If annotated code uses unannotated code (e.g., libraries or the JDK), then the checker may issue warnings. For example, the NonNull checker will warn whenever an unannotated library call result is used in a non-null context: 

  @NonNull myvar = library_call();   // WARNING: library_call is not known to return a non-null value

There are three ways to avoid such warnings.

  1. Obtain a version of the library that is annotated, or a set of external annotations that describe the library. In the future, we intend to distribute such annotations for popular libraries, such as the JDK.
  2. Annotate the library with @NonNull. You can use the annotation file utilities to express the annotations even if you do not have access to the library source code.
  3. Suppress errors and warnings pertaining to un-annotated (or other) classes, by setting the checkers.skipClasses Java property to a regular expression that matches classes for which warnings and errors should be suppressed. For example, if you use -Dcheckers.skipClasses=^java\. on the command line when invoking javac, then the checkers will suppress warnings relating to uses of classes in the java package.

What the checker guarantees

A checker can guarantee that a particular property holds throughout the code — for example, that no expression of @NonNull type ever has a null value, or that every expression of @Interned type is interned. The checker makes this guarantee by examining every part of your program and verifying that no part of the program violates the guarantee.

There are some limitations to the guarantee.