Constrain Function Inputs

For a more precise Code Prover analysis, you can specify constraints (also known as data range specifications or DRS) on function inputs. Code Prover checks your function definition for run-time errors with respect to the constrained inputs. For the general workflow, see Specify External Constraints.

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) {
     .
     .
}

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. 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.

Documentation