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.

Suppose that you wish to only allow encrypted information to be sent over the internet. To do so, you can write an Encryption Checker.

1. Import encryption-checker project

This project has two source files: Encrypted.java, the type qualifier definition, and EncryptedDemo.java, the example program that use the Encrypted checker. You will need to setup your JRE to use the Checker Framework jars, see Issue 1 below. This will fix the "TYPE_USE cannot be resolved or is not a field" error. The import myquals.Encrypted is never used warning should be ignored.

2. Set Up the Basic Checker

The Encryption Checker is built on top of the Basic Checker. Use the following steps to setup it up with in the Eclipse plugin.

  1. Navigate to Eclipse->Preferences->Checker Framework
  2. Click Add
  3. Type in BasicChecker
  4. Select BasicChecker - checkers.basic (not the one from sun) and click Ok
  5. Under Additional compiler parameters, add -Aquals=myquals.Encrypted
  6. Click Ok

3. Run the Encrypted Checker

Right Click on the src package, select Checker Framework->Run Custom Checker->Basic Checker. You should see the following errors:

incompatible types in assignment.
		/*@Encrypted*/ int encryptInt = (character + OFFSET) % Character.MAX_VALUE ;
  found   : int
  required: @Encrypted int	EncryptionDemo.java	/encryption-checker/src/encrypted	
incompatible types in argument.
		sendOverInternet(password);
  found   : String
  required: @Encrypted String	EncryptionDemo.java	/encryption-checker/src/encrypted	

4. 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. The comment should also be initialed and dated. 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) {

      

5. Run the Encryption Checker

You will see the following error:

incompatible types in argument.
		sendOverInternet(password);
  found   : String
  required: @Encrypted String	EncryptionDemo.java	/encryption-checker/src/encrypted

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

6. 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));
}

Writing a Type annotation requires ElementType.TYPE_USE and/or ElementType.TYPE_PARAMETER which are part of Java 8, but not yet supported by Eclipse. This means that Eclipse will give an error: "TYPE_USE cannot be resolved or is not a field."

Workaround
  1. Navigate to Eclipse->Preferences->Java->Installed JRES
  2. Highlight a preferred JRE and click Duplicate...
  3. (Optionally) Add Checker Framework to the JRE name
  4. Click Add External Jars
  5. Navigate to eclipse->plugins->checker.framework.eclipse.plugin_VERSION->lib
  6. Select checkers.jar, javac.jar and either jdk6.jar or jdk7.jar depending on the version the JRE you are duplicating. Click Open
  7. Move the three jars to the top of the system libraries list. Click Finish