Function Call Semantics, and the Pre and Post Contexts
Each annotation that is applied to a function is presumed to apply in exactly one of the pre and post contexts. In the pre context, the annotation is expected to hold before the function is called (that is, what the annotation says about the parameter is true before the function call). In the post context, the annotation is expected to hold after the function returns. Typically, the __in family of functions is used to describe the requirements in pre context, and the __out family for post context.
The pre and post context actually yields four states of interest:
Immediately before the function is called: the requirements of all the annotations in pre context must be met. If that is not the case, the analysis tools report an error. The calling function is responsible for all of the requirements being met.
Upon entry to the function: the analysis tools assume that all the requirements of all the annotations in pre context are met. The analysis tools perform the analysis accordingly. Be aware that if the called function is a public interface or can otherwise be called from either an environment that is not being run through PFD, or that is potentially malicious, the called function should validate its parameters. In this situation, defensive coding is still required. Often the presence of defensive coding provides enough information for PFD to confirm that the defensive coding was successful.
At the point of exit from the function: PFD checks that all the requirements of all the annotations in post context have actually been met by the called function. The called function and its implementation are responsible for making sure this happens.
Immediately after the function returns: PFD assumes that the requirements of the annotations in post context are met.
Be aware that the first and last states are part of the analysis that is performed at the point where the function is called, and that the middle two states are performed as part of the analysis of the called function. These occur at different times. PFD analyzes only one function at a time. PFD views the same contract between the calling function and the called function differently, depending on whether PFD is analyzing the function body, or analyzing the function call.
The __drv_when and __success annotations modify the contract depending on the expressions in their parameters. The __drv_when annotations only hold when the expression evaluates to TRUE. If the expression cannot be evaluated, PFD simulates both the true and false cases. For the __success annotation, PFD acts as if every annotation in post context is conditional upon the success of the function (that is, upon the expression in the __success annotation being TRUE). The __on_failure annotation can further modify the contract.
In general, using the __in and __out annotation family (including __drv_in and __drv_out) is the best way to control the context in which an annotation is implied. Many annotations only apply in pre or post context, and for those there is no requirement to be explicit about the context. For those annotations that are in need of some context, the __in and __out annotations generally suffice.
In some situations, it is appropriate to explicitly control the context for a particular annotation. The annotation primitive operators, __pre and __post, are provided to do that. These are unary operators (they apply to exactly the one subsequent annotation). You might see theseunary operators used occasionally, but if other annotations will suffice, those others are less subject to misinterpretation by either humans or the tools.
Build date: 5/3/2011