175 lines
4.7 KiB
Makefile
175 lines
4.7 KiB
Makefile
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 = \
|
|
--flush \
|
|
$(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)/freertos_kernel/queue.goto
|
|
python3 @TYPE_HEADER_SCRIPT@ --binary $(CWD)/gotos$(FREERTOS)/freertos_kernel/queue.goto --c-file $(FREERTOS)/freertos_kernel/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) -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.txt: $(ENTRY).goto
|
|
-cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace @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.txt
|
|
|
|
property: property.xml
|
|
|
|
coverage: coverage.xml
|
|
|
|
report: cbmc.txt property.xml coverage.xml
|
|
$(VIEWER) \
|
|
--goto $(ENTRY).goto \
|
|
--srcdir $(FREERTOS_PLUS_TCP) \
|
|
--blddir $(FREERTOS_PLUS_TCP) \
|
|
--htmldir html \
|
|
--srcexclude "(.@FORWARD_SLASH@doc|.@FORWARD_SLASH@tests|.@FORWARD_SLASH@vendors)" \
|
|
--result cbmc.txt \
|
|
--property property.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
|
|
# 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" $^
|
|
|
|
# ____________________________________________________________________
|
|
# Rules
|
|
#
|
|
# Rules for cleaning up
|
|
|
|
clean:
|
|
@RM@ $(OBJS) $(ENTRY).goto
|
|
@RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt
|
|
@RM@ cbmc.txt 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
|