[JSR308] Some general questions

[Mahmood Ali]

Greetings Federico,

It's great to see your interest in static analysis.

> 1) The Null checker provided with the jsr308 should guarantee (up to  
> a a
> certain limit that I would like to understand better) that there won't
> be a NullPointerException in the program.
> However a type checker (as I understood it) should guarantee only that
> the null type system is enforced, i.e., no variable declared @NonNull
> will ever be assigned a null value.
The Nullness Checker enforces two properties/rules:
1. Null type system rules, i.e. any NonNull reference cannot reference  
null
2. Only NonNull references (either marked explicitly by user or  
inferred by the system) can be dereferenced.  The checker warns  
against dereferencing of a nullable reference.

A type system does more than verifies subtype rule of an explicit  
assignments (e.g. a = b).  A type system also checks for invalid  
operations on types (e.g. "a" * 2, or "m".nonExistingMethod()).   
Dereferencing a nullable value in the nullness type system is an error  
as the type isn't guaranteed to contain any member elements.

> 2) I think there might be a bug in the checker.
Can you please provide a sample code for this bug along with the  
expected behavior?  Please send it to the jsr308-bugs mailing list (jsr308-bugs at lists.csail.mit.edu 
).

> 3) Is it possible to define a new type by the kind of values that are
> valid for that type? For example the type @Date that defines all  
> strings
> that matches the regular expression "[1-31]/[1-12]/[2000-2010]".
> If so, how to extend the basic checker for this type?
Yes.  Please read sections 7 and 9 of the Checkers manual.

Here is a summary of those sections related to the example you provided:

Summary of section 7:
When using the basic checker, you simply need to declare the  
annotations:
   @TypeQualifier
   @SubtypeOf(Unqualified.class)
   public @interface Date { }
And have the basic checker enforce the semantics of the basic type  
system (checks assignments and pseudo-assignments only).

Such checker doesn't verify that a string literal in the code is  
indeed of a Date format.  This makes either need to cast such string  
literals to @Date String type (which is an unsafe cast), or have a  
format verifier method that ensures the string is a Date string at run- 
time.

Summary of Section 9:
Because of the limitation mentioned earlier, you can build a more  
powerful checker that implicitly add @Date qualifier to the types of  
string literals that match the specified format.

With this more powerful checker, you may still need to have a method  
that verifies the string Date format for strings that are inputs from  
the user or from configuration files.

Hope that helps.

Regards,
Mahmood