Constraint setup (-data-range-specifications)

Constrain global variables, function inputs and return values of stubbed functions

Description

This option applies primarily to a Code Prover analysis. In Bug Finder, you can only specify external constraints on global variables.

Specify constraints (also known as data range specifications or DRS) for global variables, function inputs and return values of stubbed functions using a Constraint Specification template file. The template file is an XML file that you can generate in the Polyspace^® user interface.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Inputs & Stubbing node.

Command line and options file: Use the option -data-range-specifications. See Command-Line Information.

Why Use This Option

Use this option for specifying constraints outside your code.

Polyspace uses the code that you provide to make assumptions about items such as variable ranges and allowed buffer size for pointers. Sometimes the assumptions are broader than what you expect because:

• You have not provided the complete code. For example, you did not provide some of the function definitions.

• Some of the information about variables is available only at run time. For example, some variables in your code obtain values from the user at run time.

Because of these broad assumptions:

• Code Prover can consider more execution paths than those paths that occur at run time. If an operation fails along one of the execution paths, Polyspace places an orange check on the operation. If that execution path does not occur at run time, the orange check indicates a false positive.

• Bug Finder can sometimes produce false positives.

To reduce the number of such false positives, you can specify additional constraints on global variables, function inputs, and return values of stubbed functions.

After you specify your constraints, you can save them as an XML file to use them for subsequent analyses. If your source code changes, you can update the previous constraints. You do not have to create a new constraint template.

Settings

No Default

Enter full path to the template file. Alternately, click to open a Constraint Specification wizard. This wizard allows you to generate a template file or navigate to an existing template file.

For more information, see Specify External Constraints.

Command-Line Information

Parameter: -data-range-specifications

Value: file

No Default

Example (Bug Finder): polyspace-bug-finder -sources file_name -data-range-specifications "C:\DRS\range.xml"

Example (Code Prover): polyspace-code-prover -sources file_name -data-range-specifications "C:\DRS\range.xml"

Example (Bug Finder Server): polyspace-bug-finder-server -sources file_name -data-range-specifications "C:\DRS\range.xml"

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -data-range-specifications "C:\DRS\range.xml"