Checker Framework Tutorial

Getting Started

This page walks you through a simple example to show how to use a checker using the command line tools. It shows how the Nullness checker can be used to prevent null pointer exceptions.

Outline

  1. Manually spot the null pointer exception
  2. Run the Nullness Checker to see how it can catch this error
  3. Correct the error
  4. Run the Nullness Checker to verify that there are no more errors

1. Spot the null pointer exception

Begin by opening NullnessExample.java. (If you have not already, download the source files for the tutorial.) It is a simple Java program with an obvious null pointer exception. 

public class NullnessExample {
    public static void main(String[] args) {
        Object myObject = null;
        System.out.println(myObject.toString());
    }
}

2. Run the Nullness Checker

To run the Nullness checker, simply pass -processor with checkers.nullness.NullnessChecker. Note: javacheck should be an alias to the Checker Framework compiler. See the manual for an explanation. 

 
javacheck -processor checkers.nullness.NullnessChecker NullnessExample.java

The following error with be produced.

NullnessExample.java:4: error: dereference of possibly-null reference myObject
        System.out.println(myObject.toString());

3. Correct the error

Change ref to some non-null value 

public class NullnessExample {
    public static void main(String[] args) {
        Object myObject = new Object();
        System.out.println(myObject.toString());
    }
}

4. Re-run the Nullness Checker

No errors should be produced.

 
 javacheck -processor checkers.nullness.NullnessChecker NullnessExample.java

This was a very simple example to show how to use the Checker Framework in Eclipse. The next example is a little more complex.

Next, try Validating User Input, an example using the Regex checker.