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:
###################