Main Content

Constraint setup (-data-range-specifications)

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

expand all in page

Description

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.

User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Static Analysis tab 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 to constrain certain objects in your code whose values are known only at run time, for instance, user inputs or sensor values. Using correctly constrained objects might reduce false positives or orange checks in Polyspace results.

Based on your source code, Polyspace makes assumptions about items such as variable ranges and allowed buffer size for pointers. Sometimes these 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.

For instance, an int variable representing a real life speed cannot have a value that is smaller than zero or greater than the speed of light. Polyspace might assume that the variable has a range [-2^32... 2^32-1]. Because of such broad assumptions:

  • Code Prover might 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 might produce false positives.

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

After you specify your constraints, save them as an XML file to use them for subsequent analyses. If your source code changes, update the previous constraints. Creating a new constraint template is not necessary.

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 for Polyspace Analysis.

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"

You can specify an absolute path to the constraints file or a path relative to the location from which you run the polyspace-bug-finder or polyspace-code-prover command.

Examples

expand all

In this code, the multiplication operation in the definition of tmp has an orange overflow check. This check appears because Polyspace assumes that the return value of the function getSpeed() has a range -2^32... 2^32-1.

//file1.c
extern int getSpeed(); //Returns the reading of speedometer
int main(){
	//...
	int tmp = 2* getSpeed();
	//...
	return 0;
}

To resolve this orange check, constrain the return value of getSpeed() with a range [0..30000000]. Create an XML file drs.xml that has this content:

<?xml version="1.0" encoding="UTF-8"?>
<!--EDRS Version 2.0-->
<global>
	<file name="C:\\Users\\example.c">
		<function name="getSpeed"
				  line="1"
				  attributes="extern"
				  main_generator_called="disabled"
				  comment="">
			<scalar name="return"
					line="1"
					base_type="int32"
					complete_type="int32"
					init_mode="PERMANENT"
					init_modes_allowed="4"
					init_range="0  30000000"
					global_assert="unsupported"
					assert_range="unsupported"
					comment=""/>
		</function>
	</file>
</global>

After specifying the data range, run the verification again. Use the command:

polyspace-code-prover file1.c -data-range-specifications drs.xml -lang c
The orange check is replaced by a green check.
extern int getSpeed(); //Returns the reading of speedometer
int main(){
	//...
	int tmp = 2* getSpeed();
	//...
	return 0;
}

See Also

|

Topics