mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-10-15 17:27:46 -04:00
c7b3124565
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>
172 lines
4.6 KiB
Text
172 lines
4.6 KiB
Text
default: report
|
|
|
|
# ____________________________________________________________________
|
|
# CBMC binaries
|
|
#
|
|
|
|
GOTO_CC = @GOTO_CC@
|
|
GOTO_INSTRUMENT = goto-instrument
|
|
GOTO_ANALYZER = goto-analyzer
|
|
VIEWER = cbmc-viewer
|
|
|
|
# ____________________________________________________________________
|
|
# Variables
|
|
#
|
|
# Naming scheme:
|
|
# ``````````````
|
|
# FOO is the concatenation of the following:
|
|
# FOO2: Set of command line
|
|
# C_FOO: Value of $FOO common to all harnesses, set in this file
|
|
# O_FOO: Value of $FOO specific to the OS we're running on, set in the
|
|
# makefile for the operating system
|
|
# H_FOO: Value of $FOO specific to a particular harness, set in the
|
|
# makefile for that harness
|
|
|
|
ENTRY = $(H_ENTRY)
|
|
OBJS = $(H_OBJS)
|
|
|
|
INC = \
|
|
$(INC2) \
|
|
$(C_INC) $(O_INC) $(H_INC) \
|
|
# empty
|
|
|
|
CFLAGS = \
|
|
$(CFLAGS2) \
|
|
$(C_DEF) $(O_DEF) $(H_DEF) $(DEF) \
|
|
$(C_OPT) $(O_OPT) $(H_OPT) $(OPT) \
|
|
-m32 \
|
|
# empty
|
|
|
|
CBMCFLAGS = \
|
|
$(CBMCFLAGS2) \
|
|
$(C_CBMCFLAGS) $(O_CBMCFLAGS) $(H_CBMCFLAGS) \
|
|
# empty
|
|
|
|
INSTFLAGS = \
|
|
$(INSTFLAGS2) \
|
|
$(C_INSTFLAGS) $(O_INSTFLAGS) $(H_INSTFLAGS) \
|
|
# empty
|
|
|
|
# ____________________________________________________________________
|
|
# Rules
|
|
#
|
|
# Rules for patching
|
|
|
|
patch:
|
|
cd $(PROOFS)/../patches && ./patch.py
|
|
|
|
unpatch:
|
|
cd $(PROOFS)/../patches && ./unpatch.py
|
|
|
|
# ____________________________________________________________________
|
|
# Rules
|
|
#
|
|
# Rules for building the CBMC harness
|
|
|
|
C_SOURCES = $(patsubst %.goto,%.c,$(H_OBJS_EXCEPT_HARNESS))
|
|
|
|
# Build each goto-binary out-of-source (i.e. in a 'gotos' directory
|
|
# underneath each proof directory, to make it safe to build all proofs
|
|
# in parallel
|
|
OOS_OBJS = $(patsubst %.c,gotos/%.goto,$(C_SOURCES))
|
|
|
|
CWD=$(abspath .)
|
|
|
|
gotos/%.goto: %.c
|
|
mkdir -p $(dir $@)
|
|
$(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) @RULE_INPUT@
|
|
|
|
queue_datastructure.h: gotos/$(FREERTOS)/Source/queue.goto
|
|
python3 @TYPE_HEADER_SCRIPT@ --binary $(CWD)/gotos$(FREERTOS)/Source/queue.goto --c-file $(FREERTOS)/Source/queue.c
|
|
|
|
$(ENTRY)_harness.goto: $(ENTRY)_harness.c $(H_GENERATE_HEADER)
|
|
$(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) $(ENTRY)_harness.c
|
|
|
|
$(ENTRY)1.goto: $(ENTRY)_harness.goto $(OOS_OBJS)
|
|
$(GOTO_CC) @COMPILE_LINK@ @RULE_OUTPUT@ --function harness @RULE_INPUT@
|
|
|
|
$(ENTRY)2.goto: $(ENTRY)1.goto
|
|
$(GOTO_INSTRUMENT) --add-library @RULE_INPUT@ @RULE_OUTPUT@ \
|
|
> $(ENTRY)2.txt 2>&1
|
|
|
|
$(ENTRY)3.goto: $(ENTRY)2.goto
|
|
$(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \
|
|
> $(ENTRY)3.txt 2>&1
|
|
|
|
$(ENTRY)4.goto: $(ENTRY)3.goto
|
|
$(GOTO_INSTRUMENT) $(INSTFLAGS) --slice-global-inits @RULE_INPUT@ @RULE_OUTPUT@ \
|
|
> $(ENTRY)4.txt 2>&1
|
|
# ____________________________________________________________________
|
|
# After running goto-instrument to remove function bodies the unused
|
|
# functions need to be dropped again.
|
|
|
|
$(ENTRY)5.goto: $(ENTRY)4.goto
|
|
$(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \
|
|
> $(ENTRY)5.txt 2>&1
|
|
|
|
$(ENTRY).goto: $(ENTRY)5.goto
|
|
@CP@ @RULE_INPUT@ @RULE_OUTPUT@
|
|
|
|
# ____________________________________________________________________
|
|
# Rules
|
|
#
|
|
# Rules for running CBMC
|
|
|
|
goto:
|
|
$(MAKE) patch
|
|
$(MAKE) -B $(ENTRY).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.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
|
|
|
|
coverage.xml: $(ENTRY).goto
|
|
cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1
|
|
|
|
cbmc: cbmc.xml
|
|
|
|
property: property.xml
|
|
|
|
coverage: coverage.xml
|
|
|
|
report: cbmc.xml property.xml coverage.xml
|
|
$(VIEWER) \
|
|
--goto $(ENTRY).goto \
|
|
--srcdir $(FREERTOS) \
|
|
--reportdir html \
|
|
--result cbmc.xml \
|
|
--property property.xml \
|
|
--coverage coverage.xml
|
|
|
|
# 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.xml yielded a proof failure.
|
|
check-cbmc-result: cbmc.xml
|
|
grep -e "<cprover-status>SUCCESS</cprover-status>" $^
|
|
|
|
# ____________________________________________________________________
|
|
# Rules
|
|
#
|
|
# Rules for cleaning up
|
|
|
|
clean:
|
|
@RM@ $(OBJS) $(ENTRY).goto
|
|
@RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt
|
|
@RM@ cbmc.xml property.xml coverage.xml TAGS TAGS-*
|
|
@RM@ *~ \#*
|
|
@RM@ queue_datastructure.h
|
|
|
|
|
|
veryclean: clean
|
|
@RM_RECURSIVE@ html
|
|
@RM_RECURSIVE@ gotos
|
|
|
|
distclean: veryclean
|
|
cd $(PROOFS)/../patches && ./unpatch.py
|
|
cd $(PROOFS) && ./make-remove-makefiles.py
|