diff --git a/FreeRTOS/Test/CBMC/proofs/Makefile.template b/FreeRTOS/Test/CBMC/proofs/Makefile.template index fa727023c..f70045426 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