From 95ae7c65758a9473ea16ab08182f056f72331de2 Mon Sep 17 00:00:00 2001 From: markrtuttle Date: Wed, 29 Apr 2020 04:27:45 +0000 Subject: [PATCH] Change cbmc-viewer invocation in CBMC makefile (#63) * Exclude FreeRTOS/Demo from CBMC proof reports. The script cbmc-viewer generates the CBMC proof reports. The script searches source files for symbol definitions and annotates source files with coverage information. This patch causes cbmc-viewer to ignore the directory FreeRTOS/Demo containing 348M of data. The script now terminates in a few seconds. * Make report default target for CBMC Makefile. Modify the Makefile for CBMC proofs to generate the report by default (and not just property checking) and modify property checking to ignore failures (due to property assertions failing) and terminating report generation. Co-authored-by: Mark R. Tuttle --- FreeRTOS/Test/CBMC/proofs/Makefile.template | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/FreeRTOS/Test/CBMC/proofs/Makefile.template b/FreeRTOS/Test/CBMC/proofs/Makefile.template index fa727023c3..f700454261 100644 --- a/FreeRTOS/Test/CBMC/proofs/Makefile.template +++ b/FreeRTOS/Test/CBMC/proofs/Makefile.template @@ -1,4 +1,4 @@ -default: cbmc +default: report # ____________________________________________________________________ # CBMC binaries @@ -114,7 +114,7 @@ goto: $(MAKE) $(ENTRY).goto cbmc.txt: $(ENTRY).goto - cbmc $(CBMCFLAGS) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1 + - cbmc $(CBMCFLAGS) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1 property.xml: $(ENTRY).goto cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ \ @@ -135,7 +135,7 @@ report: cbmc.txt property.xml coverage.xml --srcdir $(FREERTOS) \ --blddir $(FREERTOS) \ --htmldir html \ - --srcexclude "(.@FORWARD_SLASH@doc|.@FORWARD_SLASH@tests|.@FORWARD_SLASH@vendors)" \ + --srcexclude "(.@FORWARD_SLASH@Demo)" \ --result cbmc.txt \ --property property.xml \ --block coverage.xml