Mirrors_Framework/FreeRTOS
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS.git synced 2026-09-27 22:31:16 +08:00
Code Issues Packages Projects Releases Wiki Activity

Use CBMC XML output to enable VSCode debugger (#912)

Browse Source 
Prior to this commit, CBMC would emit logging information in plain text
format, which does not contain information required for the CBMC VSCode
debugger. This commit makes CBMC use XML instead of plain text.

Co-authored-by: Mark Tuttle <tuttle@acm.org>
This commit is contained in:
Kareem Khazem
2023-01-13 13:03:06 -08:00
committed by GitHub
co-authored by Mark Tuttle
parent 2ec3cb5a0f
commit c7b3124565
1 changed files with 12 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files
FreeRTOS/Test/CBMC/proofs/Makefile.template
+12 -13
View File
@@ -119,8 +119,8 @@ goto:
# Ignore the return code for CBMC, so that we can still generate the # Ignore the return code for CBMC, so that we can still generate the
# report if the proof failed. If the proof failed, we separately fail # report if the proof failed. If the proof failed, we separately fail
# the entire job using the check-cbmc-result rule. # the entire job using the check-cbmc-result rule.
cbmc.txt: $(ENTRY).goto cbmc.xml: $(ENTRY).goto
-cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1 -cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace --xml-ui @RULE_INPUT@ > $@ 2>&1
property.xml: $(ENTRY).goto property.xml: $(ENTRY).goto
cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1 cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1
@@ -128,28 +128,27 @@ property.xml: $(ENTRY).goto
coverage.xml: $(ENTRY).goto coverage.xml: $(ENTRY).goto
cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1 cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1
cbmc: cbmc.txt cbmc: cbmc.xml
property: property.xml property: property.xml
coverage: coverage.xml coverage: coverage.xml
report: cbmc.txt property.xml coverage.xml report: cbmc.xml property.xml coverage.xml
$(VIEWER) \ $(VIEWER) \
--goto $(ENTRY).goto \ --goto $(ENTRY).goto \
--srcdir $(FREERTOS) \ --srcdir $(FREERTOS) \
--htmldir html \ --reportdir html \
--srcexclude "(.@FORWARD_SLASH@Demo)" \ --result cbmc.xml \
--result cbmc.txt \
--property property.xml \ --property property.xml \
--block coverage.xml --coverage coverage.xml
# This rule depends only on cbmc.txt and has no dependents, so it will # This rule depends only on cbmc.xml and has no dependents, so it will
# not block the report from being generated if it fails. This rule is # not block the report from being generated if it fails. This rule is
# intended to fail if and only if the CBMC safety check that emits # intended to fail if and only if the CBMC safety check that emits
# cbmc.txt yielded a proof failure. # cbmc.xml yielded a proof failure.
check-cbmc-result: cbmc.txt check-cbmc-result: cbmc.xml
grep -e "^VERIFICATION SUCCESSFUL" $^ grep -e "<cprover-status>SUCCESS</cprover-status>" $^
# ____________________________________________________________________ # ____________________________________________________________________
# Rules # Rules
@@ -159,7 +158,7 @@ check-cbmc-result: cbmc.txt
clean: clean:
@RM@ $(OBJS) $(ENTRY).goto @RM@ $(OBJS) $(ENTRY).goto
@RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt @RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt
@RM@ cbmc.txt property.xml coverage.xml TAGS TAGS-* @RM@ cbmc.xml property.xml coverage.xml TAGS TAGS-*
@RM@ *~ \#* @RM@ *~ \#*
@RM@ queue_datastructure.h @RM@ queue_datastructure.h