diff options
| author | Kareem Khazem <karkhaz@karkhaz.com> | 2023-01-13 21:03:06 +0000 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-01-13 13:03:06 -0800 |
| commit | c7b3124565d9591640c491d296ff2da665e5eb9a (patch) | |
| tree | 509a9ebc79c489dead1433e330412ca8f98c736a | |
| parent | 2ec3cb5a0fcdd974f0c7efd66ffdb6c717168899 (diff) | |
| download | freertos-git-c7b3124565d9591640c491d296ff2da665e5eb9a.tar.gz | |
Use CBMC XML output to enable VSCode debugger (#912)
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>
| -rw-r--r-- | FreeRTOS/Test/CBMC/proofs/Makefile.template | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/FreeRTOS/Test/CBMC/proofs/Makefile.template b/FreeRTOS/Test/CBMC/proofs/Makefile.template index c7692c9b4..93369d699 100644 --- a/FreeRTOS/Test/CBMC/proofs/Makefile.template +++ b/FreeRTOS/Test/CBMC/proofs/Makefile.template @@ -119,8 +119,8 @@ goto: # 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 # the entire job using the check-cbmc-result rule. -cbmc.txt: $(ENTRY).goto - -cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1 +cbmc.xml: $(ENTRY).goto + -cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace --xml-ui @RULE_INPUT@ > $@ 2>&1 property.xml: $(ENTRY).goto cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1 @@ -128,28 +128,27 @@ property.xml: $(ENTRY).goto coverage.xml: $(ENTRY).goto cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1 -cbmc: cbmc.txt +cbmc: cbmc.xml property: property.xml coverage: coverage.xml -report: cbmc.txt property.xml coverage.xml +report: cbmc.xml property.xml coverage.xml $(VIEWER) \ --goto $(ENTRY).goto \ --srcdir $(FREERTOS) \ - --htmldir html \ - --srcexclude "(.@FORWARD_SLASH@Demo)" \ - --result cbmc.txt \ + --reportdir html \ + --result cbmc.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 # intended to fail if and only if the CBMC safety check that emits -# cbmc.txt yielded a proof failure. -check-cbmc-result: cbmc.txt - grep -e "^VERIFICATION SUCCESSFUL" $^ +# cbmc.xml yielded a proof failure. +check-cbmc-result: cbmc.xml + grep -e "<cprover-status>SUCCESS</cprover-status>" $^ # ____________________________________________________________________ # Rules @@ -159,7 +158,7 @@ check-cbmc-result: cbmc.txt clean: @RM@ $(OBJS) $(ENTRY).goto @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@ queue_datastructure.h |