feat(tools/cbmc): add option to test a single testbench
This feature becomes useful when working on a single testbench. There is
no need to wait for the other testbenches to finish analysis.
Change-Id: I277b37ef796c66c26c03c4b3ca2cd29c705cfc88
Signed-off-by: Mate Toth-Pal <mate.toth-pal@arm.com>
diff --git a/docs/getting_started/build-options.rst b/docs/getting_started/build-options.rst
index de0e8cc..805482b 100644
--- a/docs/getting_started/build-options.rst
+++ b/docs/getting_started/build-options.rst
@@ -282,6 +282,7 @@
RMM_COVERAGE ,ON | OFF ,OFF ,"Enable coverage analysis"
RMM_HTML_COV_REPORT ,ON | OFF ,ON ,"Enable HTML output report for coverage analysis"
RMM_CBMC_VIEWER_OUTPUT ,ON | OFF ,OFF ,"Generate report of CBMC results using the tool cbmc-viewer"
+ RMM_CBMC_SINGLE_TESTBENCH , ,OFF ,"Run CBMC on a single testbench instead on all of them"
.. _llvm_build:
diff --git a/docs/resources/application-notes/cbmc.rst b/docs/resources/application-notes/cbmc.rst
index 0564ef3..60569be 100644
--- a/docs/resources/application-notes/cbmc.rst
+++ b/docs/resources/application-notes/cbmc.rst
@@ -53,6 +53,12 @@
For an example build command please refer to :ref:`RMM Build Examples`
+The CMake system by default runs CBMC on all the testbenches. This can take a
+long time, and it can be convenient to run a single testcase at once. This can
+be achieved using the option ``-DRMM_CBMC_SINGLE_TESTBENCH="testbench_name"``.
+The list of possible ``testbench_name``s can be listed by using the option
+``-DRMM_CBMC_SINGLE_TESTBENCH="help"``.
+
The CMake system provides different modes in which CBMC can be called, along
with their respective build targets.