Default Polyspace Configuration for Analyzing Code Generated by Embedded Coder

When analyzing generated code, Polyspace^® requires these sets of options:

Build options: These options specify the source files, the include files, compiler flags, and configuration about the target processor.
Code description options: These options describe the dataflow of the generated code.
Static analysis options: These options specify whether you want to check for coding rule violations, find code defects or find runtime errors in the generated code.
External constraints: These options constrain the variables in the analysis using information from the Simulink^® block parameters and MATLAB^® workspace variables.

When you run a Polyspace analysis of generated code from Simulink or MATLAB, Polyspace automatically configures these options in order to perform an accurate analysis. To enable Polyspace to configure the options automatically, integrate Polyspace with MATLAB and Simulink.

You can generate an options file that lists the options used for analyzing the generated code, including the preceding options, using the MATLAB function polyspacePackNGo.

Build Options

The build options specify how to build the generated code correctly.

Sources and Includes

Polyspace automatically configures the generated source files, header files, and include files correctly for the analysis. The automatically configured options are:

Include paths (-I) — Set to the include folders of the generated code.
Application source files (-sources) — Set to the source files in the generated code.

If you specify any additional value for these build options, they are appended to the existing configuration. For example, if you specify an additional path as Include paths, the path is appended tot he list of include paths for the analysis.

Toolchain

When running static analysis on the code generated by Embedded Coder^®, Polyspace automatically extracts the toolchain information from the Simulink model configuration and sets these options:

Compilation toolchain (Static analysis) — Set to generic.
Processor (-custom-target)— Polyspace mimics the hardware implementation specified by the simulink configuration parameters Device vendor and Device type.
Preprocessor definitions (-D) — Set to specify required preprocessor definitions to compile the generated code.
Disabled preprocessor definitions (-U) — Set to disable preprocessor definitions if it is necessary to compile the generated code.

Code Description Options

The code generated by Embedded Coder typically has a predictable data flow. For example, the generated code typically contains a step function, which is called in a loop after the initialization functions has been called. Polyspace automatically configures the code description options to specify the dataflow of the generated code. If you specify a different value for these options, Polyspace ignores the value you specified and analyzes the code using the values that are set automatically. Examples of automatically configured code description options include:

Verify model generated code (-main-generator) — Enabled when analyzing generated code.
Step functions (-functions-called-in-loop) — Set to the step function.
Initialization functions (-functions-called-before-loop) — Set to the initialization function.
Termination functions (-functions-called-after-loop) — Set to the terminating function.
Inputs (-variables-written-in-loop) — Set to the input variables of the step function.
Parameters (-variables-written-before-loop) — Set to the values that are initialized before the before the cyclic code loop begins.
Source code language (-lang) — When running a Polyspace Code Prover™ analysis, Polyspace sets Source code language to the same value as the configuration parameter Language (Simulink Coder).
Overflow mode for signed integer (-signed-integer-overflows) — Embedded Coder performs a wraparound of the variables in the generated code that might overflow. To configure the analysis to handle the wraparound, this option is set to warn-with-wrap-around.
Overflow mode for unsigned integer (-unsigned-integer-overflows) — Embedded Coder performs a wraparound of the variables in the generated code that might overflow. To configure the analysis to handle the wraparound, this option is set to allow.
Functions to stub (-functions-to-stub) — Set to specific helper functions in generated code that can cause imprecision in static analysis. Examples of stubbed function include rtIsNaN(), rtIsInf, or rtIsNaN().
-results-dir — Set to the folder results inside the current folder.
Consider non finite floats (-allow-non-finite-floats) — Enabled if the simulink configuration parameter Support: non-finite numbers (Simulink Coder) is set to On and Support: floating-point numbers (Embedded Coder) is set to Off.

For details about how Polyspace interprets the generated code, see How Polyspace Analysis of Generated Code Works.

Static Analysis Options

Using Polyspace, you can check for coding rule violations, code defects, or runtime errors. By Default, Polyspace checks for runtime errors in the generated code using Polyspace Code Prover.

Polyspace automatically configures the static analysis based on the values of these Simulink configuration parameters:

For details about how you can manually configure the static analysis options for generated code, see Configure Polyspace Options in Simulink.

Constraint Specification Options

Polyspace automatically creates a data range specification file using information from the MATLAB workspace and block parameters. You can constrain inputs, parameters, and outputs to lie within specified ranges. Polyspace automatically generates the external constraints for the generated code based on the values of these Simulink configuration 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.