Specifying Data Ranges for Variables and Functions (Contextual Verification)

Overview of Data Range Specifications (DRS)

By default, Polyspace software performs robustness verification, proving that the software works under all conditions. Robustness verification assumes that all data inputs are set to their full range. Therefore, nearly any operation on these inputs could produce an overflow.

The Polyspace Data Range Specifications (DRS) feature allows you to perform contextual verification, proving that the software works under normal working conditions. Using DRS, you set constraints on data ranges, and verify the code within these ranges. This can substantially reduce the number of orange checks in the verification results.

You can use DRS to set constraints on:

• Global variables

• Input parameters for user-defined functions called by the main generator

• Return values for stub functions

Note   Data ranges are applied during level 2 verification (pass2).

Back to Top

Specifying Data Ranges Using DRS Template

To use the DRS feature, you must provide a list of variables (or functions) and their associated data ranges.

Polyspace software can analyze the files in your project, and generate a DRS template containing all the global variables, user defined functions, and stub functions for which you can specify data ranges. You can then modify this template to set data ranges.

To use a DRS template to set data ranges:

1. Open the project for which you want to set data ranges.

2. Ensure that the project contains all the source files and include folders that you want to verify, and specifies the verification options that you want to use. The compilation phase of verification must complete successfully for the software to generate a DRS template.

3. In the Project Manager perspective, select the Configuration > All Settings tab.

4. Expand the Polyspace inner settings > Stubbing node.

5. In the Variable/function range setup row, select the browse button .

   The Polyspace DRS configuration dialog box opens.

   

6. On the toolbar, click Generate. The software compiles the project and generates a DRS template, for example, Module_1_Demo_C-with-MISRA-checker_drs_template.xml. You can view the DRS values through the Polyspace DRS configuration dialog box.

   

7. Specify the data ranges for global variables, user-defined function inputs, and stub-function return values. For more information, see DRS Configuration Settings.

8. To save your DRS configuration file, click (Save DRS).

   To save your DRS configuration file to a location that you specify, click (Save DRS as).

9. If you change your source code, click to generate an updated DRS configuration file.

   Note   The update functionality is not supported if the option -unit-by-unit is enabled.

10. Click OK to close the Polyspace DRS configuration dialog box. In the Variable/function range setup row, the Value cell now contains the name of the DRS configuration file. The software uses this DRS configuration file the next time you start a verification.

11. Select File > Save Project to save your project settings.

Back to Top

DRS Configuration Settings

The Polyspace DRS Configuration dialog box allows you specify data ranges for all the global variables, user defined functions, and stub functions in your project. The following table describes the parameters in the DRS Configuration interface.

Pointer Examples

For pointer p, # Allocated objects = 1, and Init Allocated = Single:

void f(int *p) { 
  int x; 
  x = p[0]; // green IDP, green NIV 
  x = p[1]; // red IDP: out of bounds 
} 

Note   Pointer p may point to any element inside the array.

For pointer p (a pointer to int), # Allocated objects = 3, and Init Allocated = MULTI:

void f(int *p) { 
  int x; 
  x = p[0]; // green IDP, green NIV 
  x = p[1]; // orange IDP, green NIV 
  x = p[2]; // orange IDP, green NIV 
  x = p[3]; // red IDP: out of bounds 
} 

Back to Top

Specifying Data Ranges Using Existing DRS Configuration

Once you have created a DRS configuration file for a project, you can reuse the data ranges for subsequent verifications.

To specify an existing DRS configuration file for your project:

1. Open the project.

2. In the Project Manager perspective, select the Configuration > All Settings tab.

3. Expand the Polyspace inner settings > Stubbing node.

4. In the Variable/function range setup row, select the browse button .

   The Polyspace DRS configuration dialog box opens.

   

5. On the toolbar, click the button to open the Load a DRS file dialog box.

6. Navigate to the folder that contains the required DRS configuration file, and select the file. Then click Open. The Load a DRS file dialog box closes.

7. In the Polyspace DRS configuration dialog box, click OK.

8. Select File > Save Project to save your project settings, including the DRS file location.

The software uses the specified DRS configuration file the next time you start a verification.

Back to Top

Editing Existing DRS Configuration

Once you have created a DRS configuration file for your project, you can edit the configuration using the Polyspace DRS configuration dialog box.

To edit an existing DRS configuration:

1. Open the project.

2. In the Project Manager perspective, select the Configuration > All Settings tab.

3. Expand the Polyspace inner settings > Stubbing node.

4. In the Variable/function range setup row, select the browse button .

   The Polyspace DRS configuration dialog box opens.

   

5. Specify the data ranges for global variables, user-defined function inputs, and stub-function return values.

6. To save your DRS configuration file, click (Save DRS),

7. Click OK, which closes the Polyspace DRS configuration dialog box.

Back to Top

XML Format of DRS File

Syntax Description — XML Elements

The DRS file contains the following XML elements:

• <file> Element

• <scalar> Element

• <pointer> Element

• <array> and <struct> Elements

• <function> Element

The following notes apply to specific fields in each XML element:

• (*) – Fields used only by the GUI. These fields are not mandatory for verification to accept the ranges. The field line contains the line number where the variable is declared in the source code, complete_type contains a string with the complete variable type, and base_type is used by the GUI to compute the min and max values.

• (**) – The field name is mandatory for scope elements <file> and <function>. For variable elements, the name must be specified when declaring a root symbol or a struct field.

• (***) – If more than one attribute applies to the variable, the attributes must be separated by a space. Only the static attribute is mandatory, to avoid conflicts between static variables having the same name.

• (****) – This element is used only by the GUI, to determine which init modes are allowed for the current element (according to its type). The value works as a mask, where the following values are added to specify which modes are allowed:

  • 1: The mode "NO" is allowed.

  • 2 : The mode "INIT" is allowed.

  • 4: The mode "PERMANENT" is allowed.

  • 8: The mode "MAIN_GENERATOR" is allowed.

  For example, the value "10" means that modes "INIT" and "MAIN_GENERATOR" are allowed. To see how this value is computed, refer to Valid Modes and Default Values.

<file> Element.  The file element has only one element "name". This element must contain the complete path to the file or only the file name.

<scalar> Element.  

<pointer> Element.  

<array> and <struct> Elements.  

<function> Element.  

Valid Modes and Default Values

Back to Top

Specifying Data Ranges Using Text Files

To use the DRS feature, you must provide a list of variables (or functions) and their associated data ranges.

You can specify data ranges using the Polyspace DRS configuration dialog box (see Specifying Data Ranges Using DRS Template), or you can provide a text file that contains a list of variables and data ranges.

Note   If you used the DRS feature prior to R2010a, you created a text file to specify data ranges. The format of this file has not changed. You can use your existing DRS text file to specify data ranges.

To specify data ranges using a DRS text file:

1. Create a DRS text file containing the list of global variables (or functions) and their associated data ranges, as described in DRS Text File Format.

2. Open the project.

3. In the Project Manager perspective, select the Configuration > All Settings tab.

4. Expand the Polyspace inner settings > Stubbing node.

5. In the Variable/function range setup row, select the browse button . The Polyspace DRS configuration dialog box opens.

6. On the toolbar, click the button to open the Load a DRS file dialog box.

7. Navigate to the folder that contains the required DRS text file, and select the file. Then click Open. The Load a DRS file dialog box closes.

   

8. In the Polyspace DRS configuration dialog box, click OK.

9. Select File > Save Project to save your project settings, including the DRS file location.

When you run a verification, the software automatically merges the data ranges in the text file with a DRS template for the project and saves the information in the file drs-template.xml, located in your results folder.

Note   You can convert your text file to an XML file. On the toolbar of the Polyspace DRS configuration dialog box, click the button . The software generates an XML version of your text file, which you can edit without affecting your original text file.

DRS Text File Format

The DRS file contains a list of global variables and associated data ranges. The point during verification at which the range is applied to a variable is controlled by the mode keyword: init, permanent, or globalassert.

The DRS file must have the following format:

variable_name min_value max_value <init|permanent|globalassert>

function_name.return min_value max_value permanent

• variable_name — The name of the global variable.

• min_value — The minimum value for the variable.

• max_value — The maximum value for the variable.

• init — The variable is assigned to the specified range only at initialization, and keeps it until first write.

• permanent — The variable is permanently assigned to the specified range. If the variable is assigned outside this range during the program, no warning is provided. Use the globalassert mode if you need a warning.

• globalassert — After each assignment, an assert check is performed, controlling the specified range. The assert check is also performed at global initialization.

• function_name — The name of the stub function.

Tips for Creating DRS Text Files

• You can use the keywords "min" and "max" to denote the minimum and maximum values of the variable type. For example, for the type long, min and max correspond to -2^31 and 2^31-1 respectively.

• You can use hexadecimal values. For example, x 0x12 0x100 init.

• Supported column separators are tab, comma, space, or semicolon.

• To insert comments, use shell style "#".

• init is the only mode supported for user-defined function arguments.

• permanent is the only mode supported for stub function output.

• Function names may be C or C++ functions with blanks or commas. For example, f(int, int).

• Function names can be specified in the short form ("f") as long as no ambiguity exists.

• The function returns either an integral (including enum and bool) or floating point type. If the function returns an integral type and you specify the range as a floating point [v0.x, v1.y], the software applies the integral interval [(int)v0-1, (int)v1+1].

Example DRS Text File

In the following example, the global variables are named x, y, z, w, and v.

x 	12 	100  		init 				
y 	0  	10000		permanent 		
z 	0  	1    		globalassert 		
w 	min	max  		permanent 		
v 	0  	max  		globalassert 		
arrayOfInt		-10 	20 	init 	
s1.id     		0   	max	init 			
array.c2  		min 	1  	init 		
car.speed	 	0   	350	permanent 
bar.return		-100	100	permanent	

# x is defined between [12;100] at initialization
# y is permanently defined between [0,10000] even any assignment
# z is checked in the range [0;1] after each assignment
# w is volatile and full range on its declaration type
# v is positive and checked after each	assignment.
# All cells arrayOfInt are defined between [-10;20] at initializsation
# s1.id is defined between [0;2^31-1] at initialisation.
# All cells array[i].c2 are defined between [-2^31;1] at initialization
# Speed of Struct car is permanently defined between 0 and 350 Km/h
# function bar returns -100..100

Back to Top

Variable Scope

DRS supports variables with external linkages, const variables, and defined variables. In addition, extern variables are supported with the option -allow-undef-variables.

Note   If you set a data range on a const global variable that is used in another variable declaration (for example as an array size) the variable using the global variable ranged, is not ranged itself.

The following table summarizes possible uses:

Every variable (or function) and associated data range will be written in the log file during the compile phase of verification. If Polyspace software does not support the variable, a warning message is displayed.

Note   If you use DRS to set a data range on a const global variable that is used in another variable declaration (for example as an array size), the variable that uses the global variable you ranged is not ranged itself.

DRS Support for Structures

DRS can initialize arrays of structures, structures of arrays, etc., as the long as the last field is explicit (structures of arrays of integers, for example).

However, DRS cannot initialize a structure itself — you can only initialize the fields. For example, "s.x 20 40 init" is valid, but "s 20 40 init" is not (because Polyspace software cannot determine what fields to initialize).

DRS Support for Union Members

In init mode, the software applies the last range in DRS to the union members at the given offset.

In globalassert mode, the software checks every globalassert in DRS for a given offset within the union at every assignment to the union variable at that offset.

For example:

union position { 
	int   sunroof; 
 	int   window; 
 	int   locks; 
} positionData; 

DRS:

positionData.sunroof	0	100	globalassert 
positionData.window	-100	0	globalassert 
positionData.locks		-1		1	globalassert 

An assignment to positionData.locks (or other members) will perform assertion checking on the ranges 0 to 100, -100 to 0, and -1 to 1.

Back to Top

Performing Efficient Module Testing with DRS

DRS allows you to perform efficient static testing of modules. This is accomplished by adding design level information missing in the source-code.

A module can be seen as a black box having the following characteristics:

• Input data are consumed

• Output data are produced

• Constant calibrations are used during black box execution influencing intermediate results and output data.

Using the DRS feature, you can define:

• The nominal range for input data

• The expected range for output data

• The generic specified range for calibrations

These definitions then allow Polyspace software to perform a single static verification that performs two simultaneous tasks:

• answering questions about robustness and reliability

• checking that the outputs are within the expected range, which is a result of applying black-box tests to a module

In this context, you assign DRS keywords according to the type of data (inputs, outputs, or calibrations).

Back to Top

Reducing Oranges with DRS

When performing robustness (worst case) verification, data inputs are always set to their full range. Therefore, every operation on these inputs, even a simple "one_input + 10" can produce an overflow, as the range of one_input varies between the min and the max of the type.

If you use DRS to restrict the range of "one-input" to the real functional constraints found in its specification, design document, or models, you can reduce the number of orange checks reported on the variable. For example, if you specify that "one-input" can vary between 0 and 10, Polyspace software will definitely know that:

• one_input + 100 will never overflow

• the results of this operation will always be between 100 and 110

This not only eliminates the local overflow orange, but also results in more accuracy in the data. This accuracy is then propagated through the rest of the code.

Using DRS removes the oranges located in the red circle below.

Why Is DRS Most Effective on Module Testing?

Removing oranges caused by full-range (worst-case) data can drastically reduce the total number of orange checks, especially when used on verifications of small files or modules.  However, the number of orange checks caused by code complexity is not effected by DRS. For more information on oranges caused by code complexity, see Subdividing Code.

This section describes how DRS reduces oranges on files or modules only.

Example

The following example illustrates how DRS can reduce oranges. Suppose that in the real world, the input "My_entry" can vary between 0 and 10.

Polyspace verification produces the following results: one with DRS and one without.

Back to Top

Polyspace C++ Class Analyzer

Preparing Source Code for Verification