ContextQMD
Back to Zephyr

Polyspace support

doc/develop/sca/polyspace.rst

4.4.03.7 KB
Original Source

.. _polyspace:

Polyspace support #################

Polyspace® <https://mathworks.com/products/polyspace.html>__ is a commercial static code analysis tool from MathWorks, which is certified for use in highest safety contexts. It can check compliance to coding guidelines like MISRA C and CERT C, find CWEs, detect bugs and calculate code complexity metrics. Optionally, it can run a formal proof to verify the absence of run-time errors like array out of bounds access, overflows, race conditions and more, and thus help achieving memory safety.

Installing

The Polyspace tools must be installed and made available in the operating system's or container's PATH variable. Specifically, the path <polyspace_root>/polyspace/bin must be on the list.

For installation instructions, see here <https://mathworks.com/help/bugfinder/install-polyspace.html>. To use formal verification (proving the absence of defects), you additionally need to install this <https://mathworks.com/help/codeprover/install-polyspace.html>.

A license file must be available in the installation folder. To request a trial license, visit this page <https://www.mathworks.com/campaigns/products/trials.html>__.

Running

The code analysis can be triggered through the west command by appending the option -DZEPHYR_SCA_VARIANT=polyspace to the build, for example:

.. code-block:: shell

west build -b qemu_x86 samples/hello_world -- -DZEPHYR_SCA_VARIANT=polyspace

Reviewing results

The identified issues are summarized at the end of the build and printed in the console window, along with the path of the folder containing detailed results.

For an efficient review, the folder should be opened in the Polyspace user interface <https://mathworks.com/help/bugfinder/review-results-1.html>__ or uploaded to the web interface <https://mathworks.com/help/bugfinder/gs/run-bug-finder-on-server.html>__ and reviewed there.

For programmatic access of the results, e.g., in the CI pipeline, the individual issues are also described in a CSV file in the results folder.

Configuration

By default, Polyspace scans for typical programming defects on all C and C++ sources. The following options are available to customize the default behavior:

.. list-table:: :widths: 20 40 30 :header-rows: 1

    • Option
    • Effect
    • Example
    • POLYSPACE_ONLY_APP
    • If set, only user code is analyzed and Zephyr sources are ignored.
    • -DPOLYSPACE_ONLY_APP=1
    • POLYSPACE_OPTIONS
    • Provide additional command line flags, e.g., for selection of coding rules. Separate the options and their values by semicolon. For a list of options, see here <https://mathworks.com/help/bugfinder/referencelist.html?type=analysisopt&s_tid=CRUX_topnav>__.
    • -DPOLYSPACE_OPTIONS="-misra3;mandatory-required;-checkers;all"
    • POLYSPACE_OPTIONS_FILE
    • Command line flags can also be provided in a text file, line by line. Provide the absolute path to the file.
    • -DPOLYSPACE_OPTIONS_FILE=/workdir/zephyr/myoptions.txt
    • POLYSPACE_MODE
    • Switch between bugfinding and proving mode. Default is bugfinding. See here <https://mathworks.com/help/bugfinder/gs/use-bug-finder-and-code-prover.html>__ for more details.
    • -DPOLYSPACE_MODE=prove
    • POLYSPACE_PROG_NAME
    • Override the name of the analyzed application. Default is board and application name.
    • -DPOLYSPACE_PROG_NAME=myapp
    • POLYSPACE_PROG_VERSION
    • Override the version of the analyzed application. Default is taken from git-describe.
    • -DPOLYSPACE_PROG_VERSION=v1.0b-28f023