External Constraints on Polyspace Analysis of Generated Code

When you check generated code for bugs or run-time errors, instead of full-range inputs, you can choose to perform the check for a specific range of input values. You can extract the input range from the Simulink^® model, or specify your own external constraints.

Likewise, you can use a fixed value for tunable parameters or a range of values. You can also check whether output values fall within a specific range.

Extract External Constraints from Model

Consider this simple model with an Inport (Simulink) block, a Gain (Simulink) block, and an Outport (Simulink) block. Suppose the signal in the Inport and Outport blocks and the gain parameter of the Gain block have a minimum and maximum value.

A simple Simulink model with a Gain block between an Inport and Outport block.

You can analyze the code generated from this model with these minimum and maximum values. On the Apps tab, select Polyspace Code Verifier. Then, on the Polyspace tab, select Settings. Specify these configuration parameters:

Input: Select Use specified minimum and maximum values. The Code Prover analysis checks the generated code within the specified range of values from the Inport block. The Bug Finder analysis uses this information to exclude false positives.
Default: This option is selected.
Tunable parametersOutput: Select Use specified minimum and maximum values.
Default: This option is not selected. The analysis uses the fixed gain value of the Gain block (the value 2 in the example).
For the analysis to consider a range instead of a fixed value, the parameters must be tunable and not inlined. See Default parameter behavior (Simulink Coder).
Output: Select Verify outputs are within minimum and maximum values. The Code Prover analysis creates a red check if the outputs exceed the range specified on the Outport block. See also Correctness condition (Polyspace Code Prover).
Default: This option is not selected. The Code Prover analysis does not check output values.

After analysis, to check if a constrained range value is used, see one of these files:

Constraint specification XML file modelname_drs.xml in the folder results_modelname\modelname.
Polyspace^® project file modelname.prpsj in the folder results_modelname.
Open this file in the Polyspace user interface. In the project configuration, see the extracted constraints specified for the option Constraint setup (-data-range-specifications).

Storage Classes Supported for Constraint Extraction from Simulink Model

To allow constraint extraction from the Simulink model, the signals and parameters must have data types in specific storage classes. For details on storage classes, see Choose Storage Class for Controlling Data Representation in Generated Code (Embedded Coder).

Common Storage Classes

Storage Class	Signal Constraint Supported	Parameter Constraint Supported
`Auto`	Yes	Yes
`ExportedGlobal`	Yes	Yes
`ImportedExtern`	Yes	Yes
`ImportedExternPointer`	Yes	Yes
`Model default`	Yes	Yes

Other Storage Classes

Storage Class	Signal Constraint Supported	Parameter Constraint Supported
`BitField`	Yes	Yes
`CompilerFlag`	No	No
`Const`	No	Yes
`ConstVolatile`	No	Yes
`Define`	No	No
`ExportToFile`	Yes	Yes
`FileScope`	Yes	No
`GetSet`	No	No
`ImportedDefine`	No	No
`ImportFromFile`	No	No
`Struct`	No	No
`Volatile`	Yes	Yes

Specify Custom External Constraints

In some instances, you might need to specify a custom set of constraints on your generated code. For instance, you might be integrating the generated code with an existing code base, which imposes a set of custom constraints.

When analyzing the generated code, specify custom external constraints through the Polyspace Configuration window:

In the Simulink Configuration Parameters window, locate the Polyspace tab, and then click Configure to open the Polyspace Configuration window.
In the Constraint Setup field, located in the Inputs & Stubbing node, specify the custom external specification XML file.

You can create and edit a custom external constraint template through the Polyspace user interface. See Specify External Constraints for Polyspace Analysis.