Checker Framework Tutorial

This section of the tutorial is only for those who are interested in writing their own type-checkers. Please feel free to skip this section.

Although the Checker Framework ships with several checkers, it is often useful to write a custom checker. Perhaps there are other runtime exceptions you wish to prevent or maybe other properties of data that should always hold. In both these cases and others, you you might wish to write your own type checker. This section of the tutorial is for those who are interested in writing their own type-checkers. If you do not wish to write a new type-checker, feel free to skip this section.

Consider a hypothetical Encrypted type qualifier, which denotes that the representation of an object (such as a String, CharSequence, or byte[]) is encrypted. This project has two source files: Encrypted.java , the type annotation definition, and EncryptedDemo.java , the example program that use the Encrypted checker.

1.Write the type annotation definition

For this example, the annotation definition has already been written. It is Encrypted.java. Please see the manual for further explanation of this file.

This code needs to be compiled with the Checker Framework compiler.

                    $ javacheck myquals/Encrypted.java
                

The resulting .class file should either be on your classpath, or on the processor path (set via the -processorpath command-line option to javac).

2. Run the Encryption Checker

The @Encrypted annotations have already been written in EncryptionDemo.java. Invoke the compiler with the Basic Checker, specifying the @Encrypted annotation using the -Aquals option. You should add the Encrypted classfile to the processor classpath:

javacheck  -processor checkers.basic.BasicChecker -Aquals=myquals.Encrypted encrypted/EncryptionDemo.java
encrypted/EncryptionDemo.java:20: error: incompatible types in assignment.
		/*@Encrypted*/ int encryptInt = (character + OFFSET) % Character.MAX_VALUE ;
		                                                     ^
  found   : int
  required: @Encrypted int
encrypted/EncryptionDemo.java:31: error: incompatible types in argument.
		sendOverInternet(password);
		                 ^
  found   : String
  required: @Encrypted String
2 errors
                

3. Suppress the First Error

The first error needs to be suppressed, because the string on the left is considered "encrypted" in this encryption scheme. All @SuppressWarnings should have a comment explaining why suppressing the warning is the correct action. See the correction below.

// The SuppressWarnings is necessary because, the type system is not capable of
//validating that the return value is encrypted. -SOM 01/25/2013
@SuppressWarnings("encrypted")
private /*@Encrypted*/ char encryptCharacter(char character) {
                

4. Run the Encryption Checker

You should just see the following error.

Source Files: 
 .../src/encrypted/EncryptionDemo.java
.../src/encrypted/EncryptionDemo.java:24: error: incompatible types in argument.
sendOverInternet(password);
^
found   : String
required: @Encrypted String
1 error
                

This is a real error, because the programmer is trying to send a password over the internet without encrypting it first.

5. Correct the Second Error

The password should be encrypted before it is sent over the internet. The correction is below.

void sendPassword() {
   String password = getUserPassword();
   sendOverInternet(encrypt(password));
}