Specify External Constraints for Polyspace Analysis

Polyspace® products analyzes C/C++ code and checks for issues such as defects (bugs) or run-time errors. The analysis 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 comes from an assumption that is too broad, the orange check might indicate 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 and modifiable arguments of stubbed functions. This example shows how to specify these external constraints (also known as data range specifications or DRS). You save the constraints 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.

Create Constraint Template

User Interface (Desktop Products Only)

To specify external constraints in the Polyspace user interface:,

  1. Locate the template file drs-template.xml that is generated in the results folder when you run a Polyspace analysis. If you have not run a Polyspace analysis before, run a Polyspace analysis and then locate the template in the folder where the .psbf or .pscp files are generated. You can run the analysis up to the compilation phase to create the template. See Verification level (-to).

  2. Copy the template file drs-template.xml to the project folder of your current analysis and rename the file.

  3. Open the project configuration. On the Static Analysis tab, select Inputs & Stubbing.

  4. To the right of Constraint setup, click the Edit button to open the Constraint Specification window.

    Constraint Specification window

  5. In the Constraint Specification dialog box, click Open and navigate to the renamed template file.

  6. Specify your constraints and save the template as an XML file. For more information, see External Constraints for Polyspace Analysis.

  7. Click OK.

    You see the full path to the template XML file in the Constraint setup field. If you run an analysis, Polyspace uses this template for extracting variable constraints.

Command Line

Use the option Constraint setup (-data-range-specifications) to specify the constraints XML file.

To specify constraints in the XML file:

  1. First, create a blank XML template. The template lists all global variables, function inputs and modifiable arguments and return values of stubbed functions without specifying any constraints on them.

    To create a blank template, run an analysis only up to the compilation phase. In Bug Finder, disable checking of defects. Use the option Find defects (-checkers). In Code Prover, check for source compliance only. Use the argument compile for the option Verification level (-to). After the analysis, a blank template XML drs-template.xml is created in the results folder.

    For C++ projects, to create a blank constraints template, you have to use the argument cpp-normalize for the option Verification level (-to).

  2. Edit the XML file to specify your constraints.

    For examples, see:

Find Variable to Constrain from Code Prover Analysis Results

You can constrain variable ranges based on their expected range in real-world applications. For instance, if a variable represents vehicle speed, you can set a maximum possible value. You can also constrain variable ranges only if they cause too many orange checks from overapproximation.

A Code Prover analysis shows all global variables, function inputs and stubbed functions that lead to orange checks from possible overapproximation. You can constrain only these variables for a more precise analysis.

  1. Open Code Prover results in the Polyspace user interface or Polyspace Access web interface.

  2. Select Orange Sources in the toolstrip.

  3. Select an orange check. If the software can trace an orange check to a root cause, a icon appears on the Result Details pane.

    Constraint Specification window

    You see the full list of variables (function inputs or return values of stubbed functions) that can cause orange checks. Constrain the ranges of these variables.

In the details for individual orange checks, you often see a message similar to this:

If appropriate, applying DRS to stubbed function random_float in example.c line 44 may remove this orange.

The message is an indication that the stubbed function is a possible source of the orange check. You can apply external constraints on the function to enforce more precise assumptions and possibly remove the orange check (in case it came from the broader assumptions).

Update Existing Constrains

With new code submissions, you might have to specify additional constraints. You can update an existing template to add global variables, function inputs and stubbed functions that come from the new code submissions.

Additionally, if you remove some variables or functions from your code, constraints on them are not applicable any more. Instead of regenerating a constraint template and respecifying the constraints, you can update an existing template and remove the variables that are not present in your code.

Note

Editing the constraint file in the Polyspace Platform user interface is not supported on Apple silicon-based Mac computers. You can edit the constraint XML file in the Polyspace Platform user interface on Windows® or Linux® machines. Alternatively, manually edit this file outside of the user interface. See XML File Format for Polyspace Analysis Constraints.

User Interface (Desktop Products Only)

  1. On the Configuration node, select Static Analysis tab.

  2. In Inputs & Stubbing, do one the following:

    • In the Constraint setup field, enter the path to the template XML file. Click Edit.

    • Click Edit. In the Constraint Specification dialog box, click the icon to navigate to your template file.

  3. After updating the constraints, click OK.

    1. Variables that are no longer present in your source code appear under the Non Applicable node. To remove an entry under the Non Applicable node or the node itself, right-click and select Remove This Node.

    2. Specify your new constraints for any of the other variables.

Command Line

In a continuous integration workflow, you can use the constraints XML file from the previous run. If new code submissions require additional constraints:

  1. Specify constraints on variables from new code submissions in a constraints XML file. See Create Constraint Template: Command Line.

  2. Merge the constraints XML file with the new constraints and the constraints XML file from the previous run.

Specify Constraints in Code

Specifying constraints outside your code allows for more precise analysis. However, you must use the code within the specified constraints because the constraints are outside your code. Otherwise, the results might not apply. For example, if you use function inputs outside your specified range, a run-time error can occur on an operation even though checks on the operation are green.

To specify constraints inside your code, you can use:

See Also

Topics