Each instance of a Pre or Post attribute specifies a set of properties for the annotated parameter or return value at a particular level of dereference.
The following table list properties that can be expressed as a parameter to the Pre and Post attributes.
Guidelines for Writing Secure Code
Detecting and Correcting C/C++ Code Defects