[Checkers] NonNull assertions

[Michael Ernst]

> From: Mahmood Ali <mahmood at MIT.EDU>
> To: checkers at lists.csail.mit.edu
> Subject: [Checkers] NonNull assertions
> Date: Mon, 28 Apr 2008 20:39:50 -0400
> 
> Greetings,
> 
> This may not be relevant to this paper.  However, I wanted to bring it  
> up for future reference.
> 
> In my case studies,  I have noticed that many projects have their own  
> method of asserting (non-)null-ability.
> 
> - Eclipse has Assert.nonNull()
> - Google Guice has Objects.nonNull() and ensureNonNull() to assert  
> nonnullability

Also, JUnit has Assert.assertNotNull and Assert.assertNull (several
overloaded versions of each), and the body of AssertTrue could be treated
just like the expression in an "assert" statement.

But, the more modern way to do testing in JUnit (and the only way supported
in TestNG, I think) is the assert statement.

All of these methods could be added to the NonNull checker's customization
of the flow-sensitive type inference.  This is a reasonable thing to put on
Matt's to-do list (*after* the paper deadline!), especially if it is
getting in Mahmood's way.  Certainly it would reduce the number of
annotations that Mahmood has to write in the case studies.

> - Javac tends to start calling getClass() on parameters as the first  
> statements in the method declaration block.

This doesn't seem to be like the others.  We want to guarantee the absence
of null pointer errors.  An explicit assumption (you could view it as a
loophole in the type system) is that all assertions pass.  If an assertion
fails, then we can still say that there wasn't a null pointer error.

By contrast, calling a method is like dereferencing a field:  it's an
operation that may fail.  Just because the program acts like the reference
is non-null is no reason for the checker to assume that is true.  (Except
that once the reference has been dereferenced, it is known to be non-null
until after the next time it might be reset.  Maybe this is what Mahmood
was getting at.)

                    -Mike