You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
93 lines
3.7 KiB
93 lines
3.7 KiB
.. _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``
|
|
|