feat(cbmc): add initial support for CBMC
This commit adds initial, partial support for analysing RMM source code
with CBMC (https://www.cprover.org/cbmc/)
Signed-off-by: Shale Xiong <shale.xiong@arm.com>
Signed-off-by: Mate Toth-Pal <mate.toth-pal@arm.com>
Change-Id: I1c66838328782cb2db630769830809c5b0847a81
diff --git a/docs/getting_started/build-options.rst b/docs/getting_started/build-options.rst
index 985fc6b..58edeb7 100644
--- a/docs/getting_started/build-options.rst
+++ b/docs/getting_started/build-options.rst
@@ -234,6 +234,16 @@
`build/Debug/coverage` within the build directory. The HTML generation can be
disabled by setting `RMM_HTML_COV_REPORT=OFF`.
+17. Run CBMC analysis:
+
+Run ``COVERAGE``, ``ANALYSIS`` and ``ASSERT`` targets for CBMC. The results
+are generated in ``${RMM_BUILD_DIR}/tools/cbmc/cbmc_coverage_results``.
+
+.. code-block:: bash
+
+ cmake -DRMM_CONFIG=host_defcfg -DHOST_VARIANT=host_cbmc -S ${RMM_SOURCE_DIR} -B ${RMM_BUILD_DIR}
+ cmake --build ${RMM_BUILD_DIR} -- cbmc-coverage cbmc-analysis cbmc-assert
+
.. _build_options_table:
###################
diff --git a/docs/getting_started/getting-started.rst b/docs/getting_started/getting-started.rst
index 88747c9..bbf744e 100644
--- a/docs/getting_started/getting-started.rst
+++ b/docs/getting_started/getting-started.rst
@@ -50,6 +50,7 @@
"Graphviz dot",">v2.38.0","Documentation"
"docutils",">v2.38.0","Documentation"
"gcovr",">=v4.2","Tools(Coverage analysis)"
+ "CBMC",">=5.84.0","Tools(CBMC analysis)"
.. _getting_started_toolchain:
@@ -225,6 +226,19 @@
sudo mkdir /usr/local/share/Cppcheck/misra
sudo cp -a <path to the misra rules file>/<file name> /usr/local/share/Cppcheck/misra/misra.rules
+############
+Install CBMC
+############
+
+.. note::
+
+ The installation of CBMC is an optional step. This is required only
+ if running source code analysis with CBMC.
+
+Follow the public documentation to install CBMC either from the official
+website https://www.cprover.org/cbmc/ or from the official github
+https://github.com/diffblue/cbmc
+
###########################
Performing an Initial Build
###########################