共用方式為

Conditional Annotations

  • 發行項

Some functions have complex interfaces in which some aspect of the interface is applicable only in certain circumstances. For such functions, applying annotations unconditionally can create a situation in which, no matter how the annotations are written, PREfast for Drivers (PFD) issues some false positives for perfectly good code.

By using conditional annotations, you can specify the precise circumstances in which the annotations apply, thereby avoiding false positives.

Use the __drv_when annotation to apply annotations conditionally. This annotation has the following syntax:

__drv_when(cond, anno_list)

This annotation specifies that the annotations in anno_list should be checked only if the conditional expression cond is true.

  • cond is an annotation expression that yields an r-value. If the condition cannot be evaluated to a constant at or before simulation time, PFD simulates the function with both the true and false possibilities.

  • anno_list consists of one or more annotations in a space-separated list. __drv_when can be freely mixed with the other annotations in the list. __drv_when annotations can also be nested. The inner annotation is applied when both the inner and outer conditions are true.

You can also use the __success annotation. If the condition is dependent on the success or failure of the function, the __success annotation is usually more clear and more compact. The __drv_when annotation is particularly useful for preconditions. For more information, see Success and Failure Annotations

One of the more common examples of a function that benefits from conditional annotation is ExAcquireResourceExclusiveLite:

BOOLEAN   ExAcquireResourceExclusiveLite(
    __in PERESOURCE  Resource,
    __in BOOLEAN Wait);

If Wait is true, the function's BOOLEAN return value does not have to be checked. If Wait is false, however, the return value must always be checked. One approach would be to write code that checks when Wait is true, but this is both irritating and confusing. However, failing to check when Wait is false invites a very bad bug.

For the case in which Wait is false, PFD requires the __checkReturn annotation to perform good analysis. To avoid checking the return value when Wait is true, use the __drv_when annotation to make the __checkReturn conditional:

__drv_when(!Wait, __checkReturn)
BOOLEAN   ExAcquireResourceExclusiveLite(
    __in PERESOURCE Resource,
    __in BOOLEAN Wait);

One of the primary uses of conditions is to indicate that, if a called function is successful, it acquires some resource (either memory or another resource type). If the called function is unsuccessful, it does not acquire the resource and thus, the resource cannot leak. This information is particularly important for functions that return NTSTATUS to indicate success because the resource that is acquired might not change in any detectable way; only the function's status value indicates success or failure. For more about annotations for resources, see Memory Resources.

Conditional Annotation Examples

The following annotations indicate that when wait is true, p must not be NULL.

__drv_when(wait, __drv_arg(p, __drv_in(__drv_deref(__notnull)))

The following annotations show an example of nesting __drv_when annotations. These annotations indicate that when wait is true, p must not be NULL, and if (wait && p2) is true, p3 must not be NULL.

    __drv_when(wait, __drv_arg(p, __drv_in(__notnull)) 
        __drv_when(p2, __drv_arg(p3, __drv_in(__notnull))

Conditional Expressions

The grammar for expressions that are supported by PFD is described in Annotation Expressions. For conditional expressions, the following additional concerns apply:

  • The expression must evaluate to an r-Value.

  • The expressions in each __drv_when annotation are evaluated independently. For a given function, all, some, or none of the conditional expressions might be true, depending on context. If two conditions are meant to be mutually exclusive, they should be coded so that they actually are.

 

 

Send comments about this topic to Microsoft

Build date: 5/3/2011