Checker Framework Tutorial

Getting Started

This page walks you through a simple example to show how to use a type-checker in the Eclipse plugin. It shows how the Nullness Checker can be used to prevent null pointer exceptions.

Outline

  1. Import checker-framework-tutorial project into Eclipse
  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. Import checker-framework-tutorial

If you have not already, download the Eclipse projects. Begin by importing the checker-framework-tutorial project into your Eclipse workspace. Select from the menu, File->Import->Existing Project, then browse to the eclipse-projects/checker-framework-tutorial directory.

Open NullnessExample.java. 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

Run the Nullness Checker to see how it can warn you about this error, before you run the program.

  1. Right-click on NullnessExample.java.
  2. Open the "Checker Framework" sub-menu.
  3. Open the "Run Built-In Checker" sub-menu.
  4. Select "Nullness Checker".

The following error will be produced.

dereference of possibly-null reference myObject
        System.out.println(myObject.toString());

3. Correct the Code

Change myObject 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 checker

Re-run the checker. No errors should be produced.

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