Checker Framework Tutorial

1. Run the Example

If you have not already done so, download the Eclipse projects and import the checker-framework-demo project into your Eclipse workspace.

To begin, open RegexExample.java. This program is called with two arguments; a regular expression and a string. The program prints the text from the string that matches the first capturing group in the regular expression. Run with a valid regular expression and a matching string such as [01]??\d-([0123]??\d)-\d{4}+ 01-24-2013 and then run with an invalid and a matching string one such as [01]??[\d-([0123]??\d)-\d{4}+ 01-24-2013 . (For a prompt in Eclipse, select Run Configurations->Arguments->Variables->string_prompt or Right click on RegexExample.launch->Run As-RegexExample)

Exception in thread "main" java.util.regex.PatternSyntaxException: Illegal character range near index 24
[01]??[\d-([0123]??\d)-\d{4}+
                        ^
	at java.util.regex.Pattern.error(Pattern.java:1924)
	at java.util.regex.Pattern.range(Pattern.java:2594)
	at java.util.regex.Pattern.clazz(Pattern.java:2507)
	at java.util.regex.Pattern.sequence(Pattern.java:2030)
	at java.util.regex.Pattern.expr(Pattern.java:1964)
	at java.util.regex.Pattern.compile(Pattern.java:1665)
	at java.util.regex.Pattern.(Pattern.java:1337)
	at java.util.regex.Pattern.compile(Pattern.java:1022)
	at RegexExample.main(RegexExample.java:13)

    
				

The user has made an error by passing in an invalid regular expression; however, good programming style dictates that a user should not see a stack trace.

2. Run Regex Checker

The Regex Checker prevents, at compile-time, use of syntactically invalid regular expressions and access of invalid capturing groups. So, it can be used to catch an invalid regular expression. Next run the Regex Checker to see how it could have spotted this issue at compile time. The checker prints out an "incompatible types" warning, because regex is not of type @Regex String which is required for strings passed to Pattern.compile() .

incompatible types in argument.
		Pattern pat = Pattern.compile(regex);
  found   : String
  required: @Regex String	RegexExample.java	

3. Fix the Code

To fix, verify the user input using the RegexUtil.isRegex(String) method. You must import org.checkerframework.checker.regex.RegexUtil. Please see the Regex chapter in the manual for a full discussion of RegexUtil class. If it is not a valid regular expression, print an error message and do not check for matches. If it is a valid regular expression, preform as before. It is not necessary to add an annotation to regex because the Regex Checker adds implicit qualifiers. Below are all the changes that need to be made to RegexExample.java to correctly handle the user input.

  import org.checkerframework.checker.regex.RegexUtil;
...
        if (!RegexUtil.isRegex(regex, 1)) {
            System.out.println("Input is not a regular expression \"" + regex
                    + "\": " + RegexUtil.regexException(regex).getMessage());
            System.exit(1);
        }
...

4. Run the Regex Checker

There should be no warnings.

5. Run the Example

Run the program exactly as before to verify that the program prints a user-friendly warning. The invalid regular expression and matching string used before are [01]??[\d-([0123]??\d)-\d{4}+ 01-24-2013 .

For a full discussion of this checker, please see the Regex Checker section of the manual.