This is so cool, from [MSDN]:

Annotation support

PREfast also supports annotations to improve the accuracy of the code analysis. Annotations provide additional information about pre- and post- conditions on function parameters and return types.

#include </prefast/SourceAnnotations.h>

[SA_Post( MustCheck=SA_Yes )] double* CalcSquareRoot

(

   [SA_Pre( Null=SA_No )] double* source,

   unsigned int size

)

In the above example:

·                     [SA_Post ( MustCheck=SA_Yes)] requires caller to check the return value of CalcSquareRoot

·                     [SA_Pre ( Null=SA_No)] requires caller to pass non-null parameter "source" to CalcSquareRoot