[ BLAST Experiences ]

For the intended use of catching NULL pointers, it seems that BLAST is not the
tool of choice.  BLAST seems to be far more useful for catching temporal
problems involving locking.  Specifically, it is not simple to track the
NULL-ness of variables.  If it were possible to abstract pointer types, adding
a field to denote whether that pointer's NULL-ness had been checked, then at
every point where the pointer is dereferenced that field could be consulted.
Building such an abstract type is possible in BLAST, but only with struct
types.  

To solve this problem we have started to look into another compile time checker
called Ccured (http://manju.cs.berkeley.edu/ccured/).  At first glance this
package seems like it doesn't quite fit the requirements.  However, simple
modifications might be made to implement the desired abstract types for what
Ccured calls 'Wild' and 'Sequence' pointers.