Constrain Global Variable Range for Polyspace Analysis

You can impose external constraints (also known as data range specifications or DRS) on the range of global variables in C/C++ code and check with Polyspace^® Code Prover™ whether write operations on the variable violate the constraint. For the general workflow, see Specify External Constraints for Polyspace Analysis.

User Interface (Desktop Products Only)

To constrain a global variable range and also check for violation of the constraint:

In your project configuration, select Inputs & Stubbing. Click the button next to the Constraint setup field.
In the Constraint Specification window, click .
Under the Global Variables node, you see a list of global variables.
For the global variable that you want to constrain:
- From the drop-down list in the Global Assert column, select YES.
- In the Global Assert Range column, enter the range in the format min..max. min is the minimum value and max the maximum value for the global variable.
To save your specifications, click the button.
In Save a Constraint File window, save your entries as an xml file.
Run a verification and open the results.
For every write operation on the global variable, you see a green, orange, or red Correctness condition check. If the check is:
- Green, the variable is within the range that you specified.
- Orange, the variable can be outside the range that you specified.
- Red, the variable is outside the range that you specified.
When two or more tasks write to the same global variable, the Correctness condition check can appear orange on all write operations to the variable even when only one write operation takes the variable outside the Global Assert range.

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 global variables. XML tags for global variables appear directly within the file tag without an enclosing function tag. For instance, in this constraint XML, PowerLevel and SHR are global variables:

<file name="\\\\home\\johndoe\\Documents\\Polyspace_Workspace\\Examples\\Code_Prover_Example\\sources\\tasks1.c">
     <scalar name="PowerLevel" line="26" ... global_assert="YES" assert_range="0..10" />
     <scalar name="SHR" line="30" ... global_assert="NO" assert_range="" />
     <function name="Tserver" line="73" .../>
     <function name="initregulate" line="47" .../>
     <function name="orderregulate" line="35" ...>
           <scalar name="return" ... global_assert="unsupported" assert_range="unsupported" />
     </function>
     <function name="proc1" line="101" .../>
</file>

To specify a constraint on a global variable and check during a Code Prover analysis if the constraint is violated:

Set the global_assert attribute of the variable's scalar tag to YES.
Set the assert_range attribute to a range in the form min..max, for instance, 0..10.

In the preceding example, the variable PowerLevel is constrained this way.