JSR 308 Checkers and Framework

Version 0.1.0 (1 May 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 plugin.

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 plugin might verify the absence of null pointer exceptions (or show where in the program they might occur), and an interning-checking plugin 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.

There are four steps to installing the checkers and the framework.

  1. Download the checkers and framework. In the future, it will also be available via anonymous SVN.
  2. Unzip the distribution zipfile, which creates a checkers directory.
  3. Edit the checkers/build.properties file so that the "compiler.lib" property specifies the location of the JSR 308 javac.jar library.
    (If you installed the compiler and checkers directories side-by-side, 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 after a successful build) to your classpath.

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 plugins
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 plugin_class command-line option: 


  javac -typeprocessor plugin_class ...

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.

Running the NonNull Example

The distribution includes an example plugin for the @NonNull type annotation. The plugin warns whenever such a variable might become null; if the plugin issues no warnings, then it is guaranteed that no use of such a variable can cause a null pointer exception. The plugin itself is implemented in the checkers.nonnull package.

To try the @NonNull plugin on a source file that uses the @NonNull qualifier, use the following command (where javac is the JSR 308 compiler):


  javac -typeprocessor checkers.nonnull.NonnullChecker examples/NonNullExample.java

Compilation should complete successfully. To show an example of the checker warning about incorrect usage of annotations (and therefore the possibility of a null pointer exception at run time), use the following command: 


  javac -typeprocessor checkers.nonnull.NonnullChecker examples/NonNullExampleWithWarnings.java

The compiler should issue three warnings regarding violation of the semantics of @NonNull in the NonNullExampleWithWarnings.java file.

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.