| Nico Huber | 5e9b1b5 | 2016-10-08 22:09:33 +0200 | [diff] [blame^] | 1 | PROOF_MODE ?= all |
| 2 | |
| 3 | jobs ?= 4 |
| 4 | |
| 5 | $(foreach dep,$($(name)-deplibs), \ |
| 6 | $(eval SPARKFLAGS += -aP=$($(dep)-dir))) |
| 7 | |
| 8 | SPARKFLAGS += -j$(jobs) |
| 9 | SPARKFLAGS += -k |
| 10 | SPARKFLAGS += -m |
| 11 | SPARKFLAGS += --mode=$(PROOF_MODE) |
| 12 | SPARKFLAGS += --report=fail |
| 13 | SPARKFLAGS += --warnings=error |
| 14 | SPARKFLAGS += --prover=cvc4,z3 --steps=500 --timeout=1 # FIXME: timeout used because steps seems broken |
| 15 | |
| 16 | quote-list = $(subst $(space),$(comma),$(patsubst %,"%",$(1))) |
| 17 | |
| 18 | $(name)-exclude-srcs = \ |
| 19 | $(filter-out \ |
| 20 | $(sort $(notdir $($(name)-proof) $($(name)-srcs) $($(name)-gens) $($(name)-extra-specs))), \ |
| 21 | $(sort $(notdir \ |
| 22 | $(wildcard $(addsuffix *.ad[sb],$($(name)-proof-dirs)))))) |
| 23 | |
| 24 | # Has to reside in the working directory. gnatprove takes paths relative |
| 25 | # to the directory wher it's placed and reports internal errors if used |
| 26 | # with absolute paths. |
| 27 | gpr := $(name).gpr |
| 28 | gpr-name = $(subst -,_,$(subst .,_,$(basename $(notdir $@)))) |
| 29 | |
| 30 | # Will be installed for inclusion |
| 31 | libgpr := $(obj)/lib$(name).gpr |
| 32 | |
| 33 | .SECONDEXPANSION: |
| 34 | |
| 35 | $(gpr): |
| 36 | @printf " GENERATE $(subst $(obj)/,,$@)\n" |
| 37 | printf '$(if $($(name)-deplibs),with "%s";\n)' $($(name)-deplibs) >$@ |
| 38 | echo 'library project $(gpr-name) is' >>$@ |
| 39 | echo ' for Library_Name use "$(name)";' >>$@ |
| 40 | echo ' for Library_Dir use "$(obj)/adalib";' >>$@ |
| 41 | echo ' for Source_Dirs use' \ |
| 42 | '($(call quote-list,$($(name)-proof-dirs)));' >>$@ |
| 43 | echo ' for Object_Dir use "$(obj)";' >>$@ |
| 44 | echo ' package Builder is' >>$@ |
| 45 | echo ' for Global_Configuration_Pragmas use' \ |
| 46 | '"$(abspath $(libhw-dir)/spark.adc)";' >>$@ |
| 47 | echo ' end Builder;' >>$@ |
| 48 | echo ' for Excluded_Source_Files use' \ |
| 49 | '($(call quote-list,$($(name)-exclude-srcs)));' >>$@ |
| 50 | echo 'end $(gpr-name);' >>$@ |
| 51 | |
| 52 | .INTERMEDIATE: $(gpr) |
| 53 | |
| 54 | $(libgpr): $$(MAKEFILE_LIST) |
| 55 | @printf " GENERATE $(subst $(obj)/,,$@)\n" |
| 56 | printf '$(if $($(name)-deplibs),with "%s";\n)' $($(name)-deplibs) >$@ |
| 57 | echo 'library project lib$(name) is' >>$@ |
| 58 | echo ' for Library_Name use "$(name)";' >>$@ |
| 59 | echo ' for Library_Dir use "lib";' >>$@ |
| 60 | echo ' for Library_ALI_Dir use "lib";' >>$@ |
| 61 | echo ' for Source_Dirs use ("proof");' >>$@ |
| 62 | echo ' for Object_Dir use external ("obj", "build");' >>$@ |
| 63 | echo 'end lib$(name);' >>$@ |
| 64 | |
| 65 | $(obj)/gnatprove/gnatprove.out: $(gpr) $$($(name)-gens) $(obj)/proofmode |
| 66 | gnatprove -P$< $(SPARKFLAGS) -Xobj=$(abspath $(obj)) |
| 67 | |
| 68 | proof: |
| 69 | if [ "$(PROOF_MODE)" != "$$(cat $(obj)/proofmode 2>/dev/null)" ]; then \ |
| 70 | echo "$(PROOF_MODE)" >$(obj)/proofmode; \ |
| 71 | fi |
| 72 | $(MAKE) $(obj)/gnatprove/gnatprove.out |
| 73 | |
| 74 | check: export override PROOF_MODE=check |
| 75 | check: proof |
| 76 | |
| 77 | flow: export override PROOF_MODE=flow |
| 78 | flow: proof |
| 79 | |
| 80 | full: export override PROOF_MODE=all |
| 81 | full: proof |
| 82 | |
| 83 | allconfigs = $(wildcard configs/*) |
| 84 | allconfigs-targets = $(addprefix allconfigs-,$(notdir $(allconfigs))) |
| 85 | |
| 86 | $(allconfigs-targets): allconfigs-%: configs/% |
| 87 | rm -rf proof-allconfigs/$* $(name)_$*.gpr |
| 88 | mkdir -p proof-allconfigs/$* |
| 89 | echo "$(PROOF_MODE)" >proof-allconfigs/$*/proofmode |
| 90 | $(MAKE) obj=proof-allconfigs/$* cnf=configs/$* gpr=$(name)_$*.gpr jobs=1 proof-allconfigs/$*/gnatprove/gnatprove.out |
| 91 | |
| 92 | proof-allconfigs: $(allconfigs-targets) |
| 93 | |
| 94 | clean:: |
| 95 | rm -rf proof-allconfigs/ |
| 96 | |
| 97 | .PHONY: proof check flow full $(allconfigs-targets) proof-allconfigs |