Main Content

Default Polyspace Options for Code Generated with Embedded Coder

Default Options

For Embedded Coder® code, the software sets the following verification options by default:

-sources path_to_source_code
-D PST_ERRNO
-D main=main_rtwec
-I matlabroot\polyspace\include
-I matlabroot\extern\include
-I matlabroot\rtw\c\libsrc
-I matlabroot\simulink\include 
-functions-to-stub=[rtIsNaN,rtIsInf,rtIsNaNF,rtIsInfF]
-results-dir results

Note

matlabroot is the MATLAB® installation folder.

Constraint Specification

You can constrain inputs, parameters, and outputs to lie within specified ranges. Use these configuration parameters:

The software automatically creates a Polyspace® constraints file using information from the MATLAB workspace and block parameters.

You can also manually define a constraints file in the Polyspace user interface. See Specify External Constraints for Polyspace Analysis. If you define a constraints file, the software appends the automatically generated information to the constraints file you create. Manually defined constraint information overrides automatically generated information for all variables.

The software supports the automatic generation of constraint specifications for the following kinds of generated code:

  • Code from standalone models

  • Code from configured function prototypes

  • Reusable code

  • Code generated from referenced models and submodels

Additional Information

See also External Constraints on Polyspace Analysis of Generated Code.

Recommended Polyspace options for Verifying Generated Code

For Embedded Coder code, the software automatically specifies values for the following verification options:

  • -main-generator

  • -functions-called-in-loop

  • -functions-called-before-loop

  • -functions-called-after-loop

  • -variables-written-in-loop

  • -variables-written-before-loop

Embedded Coder performs a wraparound of the variables in the generated code that might overflow. When running a Code Prover analysis of code generated by Embedded Coder, Polyspace uses these options:

  • -signed-integer-overflows warn-with-wrap-around

  • -unsigned-integer-overflows allow

These options might have different default values when analyzing code that is not generated by Embedded Coder. See Overflow mode for signed integer (-signed-integer-overflows) and Overflow mode for unsigned integer (-unsigned-integer-overflows).

In addition, for the option -server, the software uses the value specified in the Send to Polyspace server check box on the Polyspace pane. These values override the corresponding option values in the Configuration pane of the Polyspace user interface.

You can specify other verification options for your Polyspace Project through the Polyspace Configuration pane. See Configure Polyspace Options in Simulink.

Hardware Mapping Between Simulink and Polyspace

The software automatically imports target word lengths and byte ordering (endianness) from Simulink® model hardware configuration settings. The software maps Device vendor and Device type settings on the Simulink Configuration Parameters > Hardware Implementation pane to Target processor type settings on the Polyspace Configuration pane.

The software creates a generic target for the verification.