Annotation Overview

Annotations allow functions to explicitly state behavior. Developers can embed functional annotations into their source code to explicitly state the contracts between implementations (callees) and clients (callers). The the code analysis tool uses the additional information about the conditions of the function parameters and return types before and after the function is called to detect violations of the contract between the caller and the callee. If you specify annotations on the function declaration then you do not have to specify them on the function definition.

Attributes

The annotation scheme is implemented as VC++ compiler attributes. The following two attributes provide the basis for annotation:

Pre

Each instance of a Pre attribute specifies a set of properties for the annotated parameter. The following annotation uses the Pre attribute with the Valid property:

void f ( [ Pre (Valid = Yes) ] int pWidth);

By annotating the parameter pWidth, the function requires callers to pass a valid integer value. For an integral —or floating point— value it means that the parameter has been initialized and does not contain garbage data.

Post

Each instance of a Post attribute specifies a set of properties for the annotated parameter or return value. The following annotation uses the Post attribute with the MustCheck property:

[returnvalue:Post(MustCheck=Yes)] bool f();

By annotating the return value of a function, the caller is required to examine the return value of the function; therefore, a call like the following generates C6031:

void main( )
{
  // code
  f ( ); // warning 6031
  // code 
}

Besides the Pre and Post attributes, the following two attributes are available:

• FormatString attribute is provided to specify format information. It is used with the Style property.

• InvalidCheck attribute is provided to determine whether a return value of a function is valid or invalid. It is used with the Value property.

Properties

There are several properties that can be specified with Pre and Post attributes. Even though most properties can be used on both Pre and Post attributes, the MustCheck property can be applied only to the return value of the function and must be specified with a Post attribute. Before using a particular property, you should read the documentation to learn about the attributes and data types supported by it. For more information, see Annotation Properties.

Using Annotation in C

To use annotations in C source files, include the following file:

#include <CodeAnalysis/SourceAnnotations.h>

Next, annotate the function as shown in the following code:

void f ([ SA_Pre (Valid = SA_Yes) ] int pWidth );

Note   In C code, you must use the SA_ prefix on attributes and enumerated values.

Using Annotation in C++

In C++, after adding the #include <CodeAnalysis/SourceAnnotations.h> file, add the following namespace:

using namespace vc_attributes;

Next, annotate the function as shown in the following code:

void CMyClass::f ([ Pre (Valid = Yes) ] int pWidth )

See Also

Reference

C6031