1.. _polyspace:
2
3Polyspace support
4#################
5
6`Polyspace® <https://mathworks.com/products/polyspace.html>`__ is
7a commercial static code analysis tool from MathWorks, which is certified
8for use in highest safety contexts. It can check compliance to coding
9guidelines like MISRA C and CERT C, find CWEs, detect bugs and calculate
10code complexity metrics. Optionally, it can run a formal proof to verify
11the absence of run-time errors like array out of bounds access, overflows,
12race conditions and more, and thus help achieving memory safety.
13
14Installing
15**********
16
17The Polyspace tools must be installed and made available in the
18operating system's or container's PATH variable. Specifically, the path
19``<polyspace_root>/polyspace/bin`` must be on the list.
20
21For installation instructions, see
22`here <https://mathworks.com/help/bugfinder/install-polyspace.html>`__.
23To use formal verification (proving the *absence* of defects), you
24additionally need to install
25`this <https://mathworks.com/help/codeprover/install-polyspace.html>`__.
26
27A license file must be available
28in the installation folder. To request a trial license, visit `this
29page <https://www.mathworks.com/campaigns/products/trials.html>`__.
30
31Running
32*******
33
34The code analysis can be triggered through the ``west`` command by
35appending the option ``-DZEPHYR_SCA_VARIANT=polyspace`` to the build,
36for example:
37
38.. code-block:: shell
39
40   west build -b qemu_x86 samples/hello_world -- -DZEPHYR_SCA_VARIANT=polyspace
41
42Reviewing results
43*****************
44
45The identified issues are summarized at the end of the build and printed
46in the console window, along with the path of the folder containing
47detailed results.
48
49For an efficient review, the folder should be opened in the
50`Polyspace user interface <https://mathworks.com/help/bugfinder/review-results-1.html>`__
51or `uploaded to the web interface <https://mathworks.com/help/bugfinder/gs/run-bug-finder-on-server.html>`__
52and reviewed there.
53
54For programmatic access of the results, e.g., in the CI pipeline, the
55individual issues are also described in a CSV file in the results folder.
56
57Configuration
58*************
59
60By default, Polyspace scans for typical programming defects on all C and C++ sources.
61The following options are available to customize the default behavior:
62
63.. list-table::
64   :widths: 20 40 30
65   :header-rows: 1
66
67   * - Option
68     - Effect
69     - Example
70   * - ``POLYSPACE_ONLY_APP``
71     - If set, only user code is analyzed and Zephyr sources are ignored.
72     - ``-DPOLYSPACE_ONLY_APP=1``
73   * - ``POLYSPACE_OPTIONS``
74     - Provide additional command line flags, e.g., for selection of coding
75       rules. Separate the options and their values by semicolon. For a list
76       of options, see `here <https://mathworks.com/help/bugfinder/referencelist.html?type=analysisopt&s_tid=CRUX_topnav>`__.
77     - ``-DPOLYSPACE_OPTIONS="-misra3;mandatory-required;-checkers;all"``
78   * - ``POLYSPACE_OPTIONS_FILE``
79     - Command line flags can also be provided in a text file, line by
80       line. Provide the absolute path to the file.
81     - ``-DPOLYSPACE_OPTIONS_FILE=/workdir/zephyr/myoptions.txt``
82   * - ``POLYSPACE_MODE``
83     - Switch between bugfinding and proving mode. Default is bugfinding.
84       See `here <https://mathworks.com/help/bugfinder/gs/use-bug-finder-and-code-prover.html>`__ for more details.
85     - ``-DPOLYSPACE_MODE=prove``
86   * - ``POLYSPACE_PROG_NAME``
87     - Override the name of the analyzed application. Default is board
88       and application name.
89     - ``-DPOLYSPACE_PROG_NAME=myapp``
90   * - ``POLYSPACE_PROG_VERSION``
91     - Override the version of the analyzed application. Default is taken
92       from git-describe.
93     - ``-DPOLYSPACE_PROG_VERSION=v1.0b-28f023``
94