102 lines
3.3 KiB
Makefile
102 lines
3.3 KiB
Makefile
PROOF_MODE ?= all
|
|
|
|
jobs ?= 4
|
|
|
|
$(foreach dep,$($(name)-deplibs), \
|
|
$(eval SPARKFLAGS += -aP=$($(dep)-dir)))
|
|
|
|
SPARKFLAGS += -j$(jobs)
|
|
SPARKFLAGS += -k
|
|
SPARKFLAGS += -m
|
|
SPARKFLAGS += --mode=$(PROOF_MODE)
|
|
SPARKFLAGS += --report=fail
|
|
SPARKFLAGS += --warnings=error
|
|
SPARKFLAGS += --no-inlining
|
|
SPARKFLAGS += --prover=z3 --steps=500 --timeout=1 # FIXME: timeout used because steps seems broken
|
|
|
|
quote-list = $(subst $(space),$(comma),$(patsubst %,"%",$(1)))
|
|
|
|
$(name)-exclude-srcs = \
|
|
$(filter-out \
|
|
$(sort $(notdir $($(name)-proof) \
|
|
$($(name)-srcs) $($(name)-gens) $($(name)-extra-specs) $($(name)-extra-gens))), \
|
|
$(sort $(notdir \
|
|
$(wildcard $(addsuffix *.ad[sb],$($(name)-proof-dirs))))))
|
|
|
|
# Has to reside in the working directory. gnatprove takes paths relative
|
|
# to the directory wher it's placed and reports internal errors if used
|
|
# with absolute paths.
|
|
gpr := $(name).gpr
|
|
gpr-name = $(subst -,_,$(subst .,_,$(basename $(notdir $@))))
|
|
|
|
# Will be installed for inclusion
|
|
libgpr := $(obj)/lib$(name).gpr
|
|
|
|
.SECONDEXPANSION:
|
|
|
|
$(gpr):
|
|
@printf " GENERATE $(subst $(obj)/,,$@)\n"
|
|
printf '$(if $($(name)-deplibs),with "%s";\n)' $($(name)-deplibs) >$@
|
|
echo 'library project $(gpr-name) is' >>$@
|
|
echo ' for Library_Name use "$(name)";' >>$@
|
|
echo ' for Library_Dir use "$(obj)/adalib";' >>$@
|
|
echo ' for Source_Dirs use' \
|
|
'($(call quote-list,$($(name)-proof-dirs)));' >>$@
|
|
echo ' for Object_Dir use "$(obj)";' >>$@
|
|
echo ' package Builder is' >>$@
|
|
echo ' for Global_Configuration_Pragmas use' \
|
|
'"$(abspath $(libhw-dir)/spark.adc)";' >>$@
|
|
echo ' end Builder;' >>$@
|
|
echo ' for Excluded_Source_Files use' \
|
|
'($(call quote-list,$($(name)-exclude-srcs)));' >>$@
|
|
echo 'end $(gpr-name);' >>$@
|
|
|
|
.INTERMEDIATE: $(gpr)
|
|
|
|
$(libgpr): $$(MAKEFILE_LIST)
|
|
@printf " GENERATE $(subst $(obj)/,,$@)\n"
|
|
printf '$(if $($(name)-deplibs),with "%s";\n)' $($(name)-deplibs) >$@
|
|
echo 'library project lib$(name) is' >>$@
|
|
echo ' for Library_Name use "$(name)";' >>$@
|
|
echo ' for Library_Dir use "lib";' >>$@
|
|
echo ' for Library_ALI_Dir use "lib";' >>$@
|
|
echo ' for Source_Dirs use ("proof");' >>$@
|
|
echo ' for Object_Dir use external ("obj", "build");' >>$@
|
|
echo 'end lib$(name);' >>$@
|
|
|
|
$(obj)/gnatprove/gnatprove.out: $$($(name)-srcs) $$($(name)-gens)
|
|
$(obj)/gnatprove/gnatprove.out: $$($(name)-extra-specs) $$($(name)-extra-gens)
|
|
$(obj)/gnatprove/gnatprove.out: $(gpr) $(obj)/proofmode
|
|
gnatprove -P$< $(SPARKFLAGS) -Xobj=$(abspath $(obj))
|
|
|
|
proof:
|
|
if [ "$(PROOF_MODE)" != "$$(cat $(obj)/proofmode 2>/dev/null)" ]; then \
|
|
echo "$(PROOF_MODE)" >$(obj)/proofmode; \
|
|
fi
|
|
$(MAKE) $(obj)/gnatprove/gnatprove.out
|
|
|
|
check: export override PROOF_MODE=check
|
|
check: proof
|
|
|
|
flow: export override PROOF_MODE=flow
|
|
flow: proof
|
|
|
|
full: export override PROOF_MODE=all
|
|
full: proof
|
|
|
|
allconfigs = $(wildcard configs/*)
|
|
allconfigs-targets = $(addprefix allconfigs-,$(notdir $(allconfigs)))
|
|
|
|
$(allconfigs-targets): allconfigs-%: configs/%
|
|
rm -rf proof-allconfigs/$* $(name)_$*.gpr
|
|
mkdir -p proof-allconfigs/$*
|
|
echo "$(PROOF_MODE)" >proof-allconfigs/$*/proofmode
|
|
$(MAKE) obj=proof-allconfigs/$* cnf=configs/$* gpr=$(name)_$*.gpr jobs=1 proof-allconfigs/$*/gnatprove/gnatprove.out
|
|
|
|
proof-allconfigs: $(allconfigs-targets)
|
|
|
|
clean::
|
|
rm -rf proof-allconfigs/
|
|
|
|
.PHONY: proof check flow full $(allconfigs-targets) proof-allconfigs
|