Constrain Function Inputs for Polyspace Analysis

If a program module analyzed with Polyspace^® Code Prover™ does not contain a main function, the analysis by default starts effectively from all uncalled functions¹ . Since these functions are not called within the code, Code Prover has to make assumptions about the function inputs based on their data types. For a more precise Code Prover analysis, you can specify constraints (also known as data range specifications or DRS) on these function inputs. Code Prover analyzes these functions for run-time errors with respect to the constrained inputs. For the general workflow, see Specify External Constraints for Polyspace Analysis.

For instance, for a function defined as follows, you can specify that the argument val has values in the range [1..10]. You can also specify that the argument ptr points to a 3-element array where each element is initialized:

int func(int val, int* ptr) {
     .
     .
}

A similar assumption about function inputs is seen in Bug Finder if you use the option Run stricter checks considering all values of system inputs (-checks-using-system-input-values). You can also constrain a Bug Finder analysis with external constraints.

Note that if a function is called within the code, the external constraints no longer apply. Code Prover tracks the data flow within the code and analyzes a called function with actual arguments used in the code.

User Interface (Desktop Products Only)

To specify constraints on function inputs:

In your project configuration, select Inputs & Stubbing. Click the button for Constraint setup.
In the Constraint Specification window, click .
Under the User Defined Functions node, you see a list of functions whose inputs can be constrained.
Expand the node for each function.
You see each function input on a separate row. The inputs have the syntax function_name.arg1, function_name.arg2, etc.
Specify your constraints on one or more of the function inputs. For more information, see External Constraints for Polyspace Analysis.
For example, in the preceding code:
- To constrain val to the range [1..10], select INIT for Init Mode and enter 1..10 for Init Range.
- To specify that ptr points to a 3-element array where each element is initialized, select MULTI for Init Allocated and enter 3 for # Allocated Objects.
Run verification and open the results. On the Source pane, place your cursor on the function inputs.
The tooltips display the constraints. For example, in the preceding code, the tooltip displays that val has values in 1..10.

Command Line

Use the option Constraint setup (-data-range-specifications) with an XML file specifying your constraint.

For instance, for an analysis with Polyspace Code Prover Server™, specify the option as follows:

polyspace-code-prover-server -sources filename -data-range-specifications "C:\Polyspace\drs_project1.xml"

Create a blank constraint XML template as described in Specify External Constraints for Polyspace Analysis. In the XML file, locate and constrain the function inputs. The function inputs appear as a scalar or pointer tag in a function tag. The inputs are named as arg1, arg2 and so on. For instance, for the preceding code, the XML structure for the inputs of func appear as follows:

<function name="func" line="1" attributes="unused" main_generator_called="MAIN_GENERATOR" comment="">
     <scalar name="arg1" line="1" base_type="int32" complete_type="int32" init_mode="INIT" init_range="1..10" />
     <pointer name="arg2" line="1" complete_type="int32 *" init_mode="INIT" initialize_pointer="Not NULL" number_allocated="3" init_pointed="MULTI">  
         <scalar line="1" base_type="int32" complete_type="int32" init_mode="MAIN_GENERATOR" init_range=""/>
    </pointer>
     <scalar name="return" line="1" base_type="int32" complete_type="int32" init_mode="disabled" init_range="disabled"/>
</function>

To specify a constraint on a function input, set the attributes init_mode and init_range for scalar variables, and init_pointed and number_allocated for pointer variables.

To constrain val to the range [1..10], set the init_mode attribute of the tag with name arg1 to INIT and init_range to 1..10.
To specify that ptr points to a 3-element array where each element is initialized, set the init_mode attribute of the tag with name arg2 to INIT, init_pointed to MULTI and number_allocated to 3.