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)

1. Open the project configuration. On the Configuration pane, select Inputs & Stubbing.

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

   

3. In the Constraint Specification dialog box, create a blank constraint template. The template contains a list of all variables on which you can provide constraints. To create a new template, click . The software compiles your project and creates a template. The new template is stored in a file Module_number_Project_name_drs_template.xml in your project folder.

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

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

   • Constrain Global Variable Range for Polyspace Analysis

   • Constrain Function Inputs for Polyspace Analysis

Create Constraint Template 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. Open the Orange Sources pane. Do one of the following:

   • Select an orange check. If the software can trace an orange check to a root cause, a icon appears on the Result Details pane. Click this icon to open the Orange Sources pane.

   • In the Polyspace user interface, select Window > Show/Hide View > Orange Sources. In the Polyspace Access web interface, select Window > Orange Sources.

   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 Template

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.

User Interface (Desktop Products Only)

1. On the Configuration pane, select Inputs & Stubbing.

2. Open the existing template in one of the following ways:

   • 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. Click Update.

   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:

• Appropriate error handling tests in your code.

  Polyspace checks to determine if the errors can actually occur. If they do not occur, the test blocks appear as Unreachable code.

• The unchecked_assert macro. For example, to constrain a variable var in the range [0,10], you can use assert(var >= 0 && var <=10);.

  See Constrain Variable Ranges for Polyspace Analysis Using Manual Stubs and Manual main() Function (Polyspace Code Prover).