2871f1abef
Add the cmake files for running static code analysis with the Polyspace tools in the west build. The analysis leverages the compilation database. Options for the analysis are documented in doc/develop/sca/polyspace.rst. Analysis results are printed as command line output and provided as CSV. Manually tested on v4.0.0 with various sample applications. Signed-off-by: Martin Becker <mbecker@mathworks.com>
93 lines
3.7 KiB
ReStructuredText
93 lines
3.7 KiB
ReStructuredText
.. _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``
|