External Constraints for Polyspace Analysis

Polyspace^® uses the code that you provide to make assumptions about items such as variable ranges and allowed buffer size for pointers. Sometimes the assumptions that Polyspace makes are broader than what you expect, which might result in Bug Finder false positives or more Code Prover orange checks. To reduce such false positives or orange checks, you can specify external constraints on:

Global variables.
User-defined functions.
Stubbed functions.

For more information, see Specify External Constraints for Polyspace Analysis. For a partial list of limitations, see Constraint Specification Limitations.

Effect of External Constraints

Consider the following function:

int getFlooredNumber(int total, int size) {
    return total/size;
}

Since the input size is unknown, if you analyze this function:

With Polyspace Code Prover™, you see an orange Division by zero check. The orange check indicates that Code Prover suspects a possible division by zero error, but this error does not occur on all execution paths.
With Polyspace Bug Finder™, if you use the option Run stricter checks considering all values of system inputs (-checks-using-system-input-values), you see an Integer division by zero defect along with one possible input value leading to the defect (in this case, a size of 0).
In more sophisticated examples, for instance, if the division occurs inside a condition, a defect appears from unknown inputs even without using the option.

In both cases, the analysis determines possible values of the input variable size from its data type. Since the variable size has data type int, on targets where int has a size of 32 bits, the variable is assumed to have values in the range [-2³¹, 2³¹-1].

If you know that an input has values only within a certain range, you can specify an external constraint on the input (also known as Data Range Specification or DRS). For instance, in the above example, if you specify a range on size that excludes zero:

Code Prover no longer shows the orange Division by zero check.
Bug Finder no longer shows the Integer division by zero defect.

You can specify external constraints to emulate design constraints that live outside your code. For instance, if an input variable represents a physical quantity such as vehicle speed, you can constrain the variable values to speeds for which the vehicle is designed.

Constraint Specification

In the user interface of the Polyspace desktop products, you can specify the constraints through a Constraint Specification window. The constraints are saved in an XML file that you can reuse for other projects.

This table describes the various columns in the Constraint Specification window. If you directly edit the constraint XML file to specify a constraint (for instance, in the Polyspace Server products), this table also shows the correspondence between columns in the user interface and entries in the XML file. The XML entry highlighted in bold appears in the corresponding column of the Constraint Specification window.

Column	Settings	XML File Entry
Name	Displays the list of variables and functions in your project for which you can specify data ranges. This Column displays three expandable menu items: Globals – Displays global variables in the project. User defined functions – Displays user-defined functions in the project. Expand a function name to see its inputs. Stubbed functions – Displays a list of stub functions in the project. Expand a function name to see the inputs and return values.	<function name = "funcName" ...> <scalar name = "arg1" ...> <pointer name = "arg2" ...>
File	Displays the name of the source file containing the variable or function.	<file name = "C:\Project1\Sources\file.c" ...>
Attributes	Displays information about the variable or function. For example, static variables display `static`. Uncalled functions display `unused`.	<function name="funcName" attributes="unused" ...>
Data Type	Displays the variable type.	<scalar name="arg1" complete_type="int32" ...>
Main Generator Called	Applicable for only user-defined functions. Specifies whether the main generator calls the function: `MAIN GENERATOR` – Main generator may call this function, depending on the value of the `-functions-called-in-loop` (C) or `-main-generator-calls` (C++) parameter. `NO` – Main generator will not call this function. `YES` – Main generator will call this function.	<function name="funcName" main_generator_called="MAIN_GENERATOR" ...>
Init Mode	Specifies how the software assigns a range to the variable: `MAIN GENERATOR` – Variable range is assigned depending on the settings of the main generator options `-main-generator-writes-variables` and `-no-def-init-glob`. `IGNORE` – Variable is not assigned to any range, even if a range is specified. `INIT` – Variable is assigned to the specified range only at initialization, and keeps the range until first write. `PERMANENT` – 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. User-defined functions support only `INIT` mode. Stub functions support only `PERMANENT` mode. For C verifications, global pointers support `MAIN GENERATOR`, `IGNORE`, or `INIT` mode. `MAIN GENERATOR` – Pointer follows the options of the main generator. `IGNORE` – Pointer is not initialized. `INIT` – Specify if the pointer is NULL, and how the pointed object is allocated (Initialize Pointer and Init Allocated options).	<scalar name="arg1" init_mode="INIT" ...>
Init Range	Specifies the minimum and maximum values for the variable. 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 also use hexadecimal values. For example: `0x12..0x100`. For `enum` variables, you cannot specify ranges directly by using the enumerator constants. Instead use the values represented by the constants. For `enum` variables, you can also use the keywords `enum_min` and `enum_max` to denote the minimum and maximum values that the variable can take. For example, for an `enum` variable of the type defined below, `enum_min` is 0 and `enum_max` is 5: enum week{ sunday, monday=0, tuesday, wednesday, thursday, friday, saturday};	<scalar name="arg1" init_range="-1..0"...>
Initialize Pointer	Applicable only to pointers. Enabled only when you specify Init Mode:`INIT`. Specifies whether the pointer should be NULL: `May-be NULL` – The pointer could potentially be a NULL pointer (or not). `Not Null` – The pointer is never initialized as a null pointer. `Null` – The pointer is initialized as NULL. Note Not applicable for C++ projects. See Constraint Specification Limitations.	<pointer name="arg1" initialize_pointer="Not NULL"...>
Init Allocated	Applicable only to pointers. Enabled only when you specify Init Mode:`INIT`. Specifies how the pointed object is allocated: `MAIN GENERATOR` – The pointed object is allocated by the main generator. `NONE` – Pointed object is not written. `SINGLE` – The pointed object or the first element of an array are initialized. You can also constrain the pointed-to object using its Init Range attribute. That is, if the pointer is `ptr`, then you can also constrain the pointed-to object `ptr`. If the pointed-to object is an array, the range applies only to the first element of the array. `MULTI`* – All objects (or array elements) are initialized. You can also constrain the pointed-to object using its Init Range attribute. That is, if the pointer is `ptr`, then you can also constrain the pointed-to object `ptr`. If the pointed-to object is an array, the range applies to all elements of the array. Two other options are available for pointer arguments to stubbed functions: `SINGLE_CERTAIN_WRITE`* – The pointed object or the first element of an array is initialized by the stubbed function. `MULTI_CERTAIN_WRITE` – All pointed objects (or array elements) are initialized by the stubbed function. For stubbed functions, the options `SINGLE` and `MULTI` mean a probable initialization instead of a certain initialization. Note Not applicable for C++ projects. See Constraint Specification Limitations.	<pointer name="arg1" init_pointed="MAIN_GENERATOR"...>
# Allocated Objects	Applicable only to pointers. Specifies how many objects are pointed to by the pointer (the pointed object is considered as an array). The Init Allocated parameter specifies how many allocated objects are actually initialized. For instance, consider this code: void func(int ptr) { assert(ptr[0]==1); assert(ptr[1]==1); } If you specify these constraints: `ptr` has Init Allocated* set to `MULTI` and # Allocated Objects set to 2, `ptr` has Init Range* set to `1..1`, both assertions are green. If you specify these constraints: `ptr` has Init Allocated set to `SINGLE` `ptr` has Init Range* set to `1..1`, the second assertion is orange. Only the first object that `ptr` points to initialized to 1. Objects beyond the first can be potentially full range. Use the keyword "max" to specify that a pointer can point to anywhere within a very large array of unknown file size. In your analysis results, you see very large offsets and buffer sizes for the pointer. The offset and buffer sizes depend on the pointer size and other characteristics of the target processor type used. The largest object Polyspace creates using this method is a buffer of 2^27-1 bytes (134217726 bytes). Note Not applicable for C++ projects. See Constraint Specification Limitations.	<pointer name="arg1" number_allocated="10"...>
Global Assert	Specifies whether to perform an assert check on the variable at global initialization, and after each assignment.	<scalar name="glob" global_assert="YES"...>
Global Assert Range	Specifies the minimum and maximum values for the range you want to check.	<scalar name="glob" assert_range="0..200"...>
Comment	Remarks that you enter, for example, justification for your DRS values.	<scalar name="glob" comment="Speed Range"...>

Constraint Specification Limitations

You cannot specify the following types of constraints using the constraint specification interface. To work around some of these limitations, you can define your own stubs and main(). For details, see Constrain Variable Ranges for Polyspace Analysis Using Manual Stubs and Manual main() Function (Polyspace Code Prover).

The constraint specification interface does not support these kinds of constraints:

In C++, you cannot constrain pointer or reference arguments of functions.
Because of polymorphism, a C++ pointer or reference can point to objects of multiple classes in a class hierarchy and can require invoking different constructors. The pre-analysis for constraint specification cannot determine which object type to constrain or which constructor to call.
You cannot specify a constraint that relates the return value of a function to its inputs. You can specify only a constant range for the constraints.
You cannot specify multiple ranges for a constraint. For instance, you cannot specify that a function argument has either the value -1 or a value in the range [1,100]. Instead, specify the range [-1,100] or perform two separate analyses, once with the value -1 and once with the range [1,100].
You cannot specify separate constraints on different fields of a union.
You cannot constrain an object that is accessed by more than one level of indirection. For example, you can specify constraints for a pointer, but you cannot specify constraints for a pointer to pointer.