summaryrefslogtreecommitdiff
path: root/FreeRTOS/Test/CBMC/proofs/Makefile.template
diff options
context:
space:
mode:
Diffstat (limited to 'FreeRTOS/Test/CBMC/proofs/Makefile.template')
-rw-r--r--FreeRTOS/Test/CBMC/proofs/Makefile.template6
1 files changed, 3 insertions, 3 deletions
diff --git a/FreeRTOS/Test/CBMC/proofs/Makefile.template b/FreeRTOS/Test/CBMC/proofs/Makefile.template
index 01d518ed5..c7692c9b4 100644
--- a/FreeRTOS/Test/CBMC/proofs/Makefile.template
+++ b/FreeRTOS/Test/CBMC/proofs/Makefile.template
@@ -138,11 +138,11 @@ report: cbmc.txt property.xml coverage.xml
$(VIEWER) \
--goto $(ENTRY).goto \
--srcdir $(FREERTOS) \
- --reportdir html \
- --exclude "(.@FORWARD_SLASH@Demo)" \
+ --htmldir html \
+ --srcexclude "(.@FORWARD_SLASH@Demo)" \
--result cbmc.txt \
--property property.xml \
- --coverage coverage.xml
+ --block coverage.xml
# This rule depends only on cbmc.txt and has no dependents, so it will
# not block the report from being generated if it fails. This rule is