Modify Code Prover Run-Time Checks Through Code Behavior Specifications

Polyspace^® Code Prover™ exhaustively checks C/C++ code for run-time errors. For greater analysis precision, you can provide additional information outside your code.

You can specify most external information using the option -code-behavior-specifications. The option allows you to associate behaviors with elements in your code. For instance, you can map a custom library function to a standard function or specify that a function acts as a memory management function. The option takes a file in one of these formats as argument:

XML
Datalog

Only the XML format applies to Polyspace Code Prover. This topic describes the supported check modifications. For the full list of options that can modify run-time checks, see Modify or Disable Code Prover Run-Time Checks.

The code behavior specifications XML file associates specific behaviors with functions (or defines behaviors at global scope). The following sections list behaviors that are relevant to a Code Prover analysis. For behaviors relevant to Bug Finder, see Modify Bug Finder Checkers Through Code Behavior Specifications.

You can also see the supported behaviors in the sample template file code-behavior-specifications-template.xml provided with a Polyspace installation. The file is in polyspaceroot\polyspace\verifier\cxx\ where polyspaceroot is the Polyspace installation folder.

Mapping to Standard Function for Precision Improvement

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <functions>
        <function name="custom_function" std="std_function"> 
        </function>
    </functions>
</specifications>

Use this entry in the XML file to reduce the number of orange checks from imprecise Code Prover analysis of your function (or false negatives from an imprecise Bug Finder analysis). Sometimes, the verification does not analyze certain kinds of functions precisely because of inherent limitations in static verification. In those cases, if you find a standard function that is a close analog of your function, use this mapping. Though your function itself is not analyzed, the analysis is more precise at the locations where you call the function. For instance, if the verification cannot analyze your function cos32 precisely and considers full range for its return value, map it to the cos function for a return value in [-1,1].

The verification ignores the body of your function. However, the verification emulates your function behavior in the following ways:

The verification assumes the same return values for your function as the standard function.
For instance, if you map your function cos32 to the standard function cos, the verification assumes that cos32 returns values in [-1,1].
The verification checks for the same issues as it checks with the standard function.
For instance, if you map your function acos32 to the standard function acos, the Invalid use of standard library routine check determines if the argument of acos32 is in [-1,1].

The functions that you can map to include:

Standard library functions from math.h.
Memory management functions from string.h.
__ps_meminit: A function specific to Polyspace that initializes a memory area.
Sometimes, the verification does not recognize your memory initialization function and produces an orange Non-initialized local variable check on a variable that you initialized through this function. If you know that your memory initialization function initializes the variable through its address, map your function to __ps_meminit. The check turns green.
__ps_lookup_table_clip: A function specific to Polyspace that returns a value within the range of the input array.
Sometimes, the verification considers full range for the return values of functions that look up values in large arrays (look-up table functions). If you know that the return value of a look-up table function must be within the range of values in its input array, map the function to __ps_lookup_table_clip.
In code generated from models, the verification by default makes this assumption for look-up table functions. To identify if the look-up table uses linear interpolation and no extrapolation, the verification uses the function names. Use the mapping only for handwritten functions, for instance, functions in a C/C++ S-Function (Simulink) block. The names of those functions do not follow specific conventions. You must explicitly specify them.

Mapping to Standard Function for Concurrency Detection

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <functions>
        <function name="custom_function" std="std_function"> 
        </function>
    </functions>
</specifications>

Use this entry in the XML file for automatic detection of thread-creation functions and functions that begin and end critical sections. Polyspace supports automatic detection for certain families of multitasking primitives only. Extend the support using this XML entry.

If your thread-creation function, for instance, does not belong to one of the supported families, map your function to a supported concurrency primitive.

Extending Initialization Checks

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <functions>
        <function name="my_func">
            <check name=name="ARGUMENT_POINTS_TO_INITIALIZED_VALUE" arg="n"/>
        </function>
    </functions>
</specifications>

Use this entry in the XML file to specify if the pointer argument to a function my_func must point to an initialized buffer. The number n specifies which argument must be checked for buffer initialization.

Specifying Contribution from Stubbed Functions to Stack Size

XML Syntax:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <functions>
        <function name="my_func">
            <behavior name="STACK_SIZE_LOCAL_VARIABLES" value="size"/>
        </function>
    </functions>
</specifications>

Use this entry in the XML file to specify that local variables in a function my_func contribute size bytes to the stack size. Stack size computation for callers of my_func take this contribution into account.

Instead of a fixed size, you can also specify a lower and upper bound on the stack size contribution from a function. Enter a minimum local variable size min_size and a maximum size max_size for the value attribute as follows:

<?xml version="1.0" encoding="UTF-8"?>
<specifications xmlns="http://www.mathworks.com/PolyspaceCodeBehaviorSpecifications">
    <functions>
        <function name="my_func">
            <behavior name="STACK_SIZE_LOCAL_VARIABLES" value="min_size,max_size"/>
        </function>
    </functions>
</specifications>

Note that for template functions, you have to specify the same stack size contribution from all instantiations of the functions. You cannot specify separate values for different instantiations.