Extend Bug Finder Checkers for Standard Library Functions to Custom Libraries

This topic shows how to create checkers for your custom library functions by mapping them to equivalent functions from the Standard Library.

Identify Need for Extending Checker

If you identify a Bug Finder checker that applies to a Standard Library function and can be extended to your custom library function, use this technique.

For instance, you might define a math function that has the same domain as a Standard Library math function. If Bug Finder checks for domain errors when using the Standard Library function, you can perform the same checks for the equivalent custom function.

Suppose that you define a function acos32 that expects values in the range [-1,1]. You might want to detect if the function argument falls outside this range at run time, for instance, in this code snippet:

#include<math.h>
#include<float.h>

double acos32(double);
const int periodicity = 1.0;

int isItPeriodic() {
   return(abs(func(0.5) - func(0.5 + periodicity)) < DBL_MIN);
}

double func(double val) {
  return acos32(val);  
}

One of the arguments to acos32 is outside its allowed domain. If you do not provide the implementation of acos32 or if the analysis of the acos32 implementation is not precise, Bug Finder might not detect the issue. However, the function has the same domain as the Standard Library function acos. You can extend the checker

Invalid use of
                    standard library floating point routine

that detects domain errors in uses of acos to detect the same kinds of errors with acos32.

If your custom function does not have a constrained domain but returns values in a constrained range, you can still map the function to an equivalent Standard Library function (if one exists) for more precise results on other checkers. For instance, you can map a function cos32 that returns values in the range [-1,1] to the Standard Library function cos.

Extend Checker

You can extend checkers on functions from the Standard Library by mapping those functions to your custom library functions. For instance, in the preceding example, you can map the function acos32 to the Standard Library function acos.

To perform the mapping:

List each mapping in an XML file in a specific syntax.
Copy the template file code-behavior-specifications-template.xml from the folder polyspaceroot\polyspace\verifier\cxx to a writable location and modify the file. Enter the mapping in the file using the following syntax after existing similar entries:
```
<function name="acos32" std="acos"> </function>
```
Remove previously existing entries in the file to avoid warnings.
Specify this XML file as argument for the option -code-behavior-specifications.

Checkers That Can Be Extended

The following checkers can be extended in this way:

Limitations

You can map your custom function to a standard library function with similar semantics, subject to the following constraints:

Your custom function must have the same number of arguments as the standard library function or more. Make sure that every argument of the standard library function is mapped to an argument of the custom function. For examples of argument remapping, see also -code-behavior-specifications.
The mapped function arguments must have compatible data types. Likewise, the custom function must have a return type that is compatible with the standard library function. For instance:
- An integer type (char, int, etc.) is not compatible with a floating point type (float, double, etc.)
- A fundamental type is not compatible with a structure or enumeration.
- A pointer type is not compatible with a non-pointer type.