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 many checkers, you may wish to write your own checker because there are other run-time problems you wish to prevent. If you do not wish to write a new type-checker, feel free to skip this section of the tutorial.
As an example, suppose that you wish to only allow encrypted information to be sent over the internet. To do so, you can write an Encryption Checker.
You need to do some setup to prepare Eclipse.
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 myqual.Encrypted is never used warning should be ignored. When building the encryption-checker project, set the -source and -target levels to at least 1.7 (1.8 is recommended). See Issue 2.
The Encryption Checker is built on top of the Subtyping Checker. The Subtyping Checker allows you to enforce a basic type systems by listing its qualifiers when type checking. To set up the Subtyping Checker to use the Encryption Checker's qualifiers, do the following:
For this example, the annotation definitions have already been
written for you and appear in files Encrypted.java,
PossiblyUnencrypted.java, and
PolyEncrypted.java.
The @Encrypted annotations have already been written
in file EncryptionDemo.java. The default for types without annotations is
@PossiblyUnencrypted.
Invoke the compiler with the Subtyping Checker. Right Click on the src package, select Checker Framework->Run Built-in Checker->Subtyping Checker. You should see the following errors:
incompatible types in assignment.
/*@Encrypted*/ int encryptInt = (character + OFFSET) % Character.MAX_VALUE ;
found : @PossiblyUnencrypted int
required: @Encrypted int EncryptionDemo.java /encryption-checker/src/encrypted
incompatible types in argument.
sendOverInternet(password);
found : @PossiblyUnencrypted String
required: @Encrypted String EncryptionDemo.java /encryption-checker/src/encrypted
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.
@SuppressWarnings("encrypted") // this is the encryption algorithm
private /*@Encrypted*/ char encryptCharacter(char character) {
You will see the following error:
incompatible types in argument.
sendOverInternet(password);
found : @PossiblyUnencrypted String
required: @Encrypted String
This is a real error, because the programmer is trying to send a password over the Internet without encrypting it first.
The password should be encrypted before it is sent over the Internet. The correction is below.
void sendPassword() {
String password = getUserPassword();
sendOverInternet(encrypt(password));
}
There should be no errors.
For further explanations, see the Checker Framework manual, chapter How to create a new checker.
Writing a Type annotation requires ElementType.TYPE_USE and/or ElementType.TYPE_PARAMETER which are part of Java 8. If you are using a version of Eclipse that does not support Java 8, Eclipse will give an error: "TYPE_USE cannot be resolved or is not a field".
To update your -source and -target levels: