Initial upstream commit
The history contained unlicensed code so everything got squashed, sorry.
Change-Id: Ie1335ecfcee7f740bb6de2e9887606be30a2deff
Signed-off-by: Nico Huber <nico.huber@secunet.com>
diff --git a/Makefile.proof b/Makefile.proof
new file mode 100644
index 0000000..91b98c9
--- /dev/null
+++ b/Makefile.proof
@@ -0,0 +1,97 @@
+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 += --prover=cvc4,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))), \
+ $(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: $(gpr) $$($(name)-gens) $(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