build(tools/cbmc): integrate cbmc-viewer
Add option to the build system to call cbmc-viewer. The following
changes were necessary:
- Add option to make call of cbmc-viewer optional
- Update CBMC Application note with cbmc-viewer
- Separate CBMC run to 2 steps: compiling to GOTO program, and call
CBMC on the resulting goto program. This is necessary becasue
cbmc-viewer operates on the GOTO program.
- Rewrite extraction of summary, as XML output (required by CBMC) files
doesn't contain summary
Change-Id: Ieb2623d3b03845dcb4ab74baead81d3c0fc6dee8
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 6dab78d..de0e8cc 100644
--- a/docs/getting_started/build-options.rst
+++ b/docs/getting_started/build-options.rst
@@ -281,6 +281,7 @@
HOST_MEM_SIZE , ,0x40000000 ,"Host memory size that will be used as physical granules"
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"
.. _llvm_build: