Nico Huber has uploaded this change for review. ( https://review.coreboot.org/27139
Change subject: Makefile: Revise support for generated sources ......................................................................
Makefile: Revise support for generated sources
Handle generated source files more independently from normal source files. This allows mixing of generated specs with existing source bodies.
Change-Id: I5479c436f39088ae9d0ebddf9a97446be0f191f3 Signed-off-by: Nico Huber nico.h@gmx.de --- M Makefile M Makefile.proof 2 files changed, 16 insertions(+), 9 deletions(-)
git pull ssh://review.coreboot.org:29418/libhwbase refs/changes/39/27139/1
diff --git a/Makefile b/Makefile index 09881e5..a25deb6 100644 --- a/Makefile +++ b/Makefile @@ -190,12 +190,16 @@ # *-srcs. Extract / filter all specification files that have a matching # body (.adb) file here (specifications without a body are valid sources # in Ada). -$(name)-extra-specs := \ +# $1 source list +filter_extra_specs = \ $(filter \ - $(addprefix %/,$(patsubst %.adb,%.ads,$(notdir $(filter %.adb,$($(name)-srcs))))), \ - $(filter %.ads,$($(name)-srcs) $($(name)-gens))) + $(addprefix %/,$(patsubst %.adb,%.ads, \ + $(notdir $(filter %.adb,$($(name)-srcs) $($(name)-gens))))), \ + $(filter %.ads,$(1))) +$(name)-extra-specs := $(call filter_extra_specs,$($(name)-srcs)) $(name)-srcs := $(filter-out $($(name)-extra-specs),$($(name)-srcs)) -$(name)-gens := $(filter-out $($(name)-extra-specs),$($(name)-gens)) +$(name)-extra-gens := $(call filter_extra_specs,$($(name)-gens)) +$(name)-gens := $(filter-out $($(name)-extra-gens),$($(name)-gens))
$(name)-objs := $(call src-to-obj,,$($(name)-srcs) $($(name)-gens)) $(name)-alis := $(call src-to-ali,,$($(name)-srcs) $($(name)-gens)) @@ -216,8 +220,8 @@ $(if $(wildcard $(1)),\ $(filter \ $(addprefix %/,$(shell sed -ne's/^D ([^\t]+).*$$/\1/p' $(1) 2>/dev/null)), \ - $($(name)-srcs) $($(name)-gens) $($(name)-extra-specs)), \ - $($(name)-gens)) + $($(name)-srcs) $($(name)-gens) $($(name)-extra-specs) $($(name)-extra-gens)), \ + $($(name)-gens) $($(name)-extra-gens))
# Adds dependency rules # $1 source file @@ -283,7 +287,7 @@ $(shell mkdir -p $(alldirs))
$(name)-install-srcs = $(sort \ - $($(name)-extra-specs) $(filter %.ads,$($(name)-srcs) $($(name)-gens)) \ + $($(name)-extra-specs) $($(name)-extra-gens) $(filter %.ads,$($(name)-srcs) $($(name)-gens)) \ $(foreach adb,$(filter %.adb,$($(name)-srcs)), \ $(shell grep -q '^U .*<BN>' $(call src-to-ali,,$(adb)) 2>/dev/null && echo $(adb))))
diff --git a/Makefile.proof b/Makefile.proof index 45523c3..3d30c2b 100644 --- a/Makefile.proof +++ b/Makefile.proof @@ -17,7 +17,8 @@
$(name)-exclude-srcs = \ $(filter-out \ - $(sort $(notdir $($(name)-proof) $($(name)-srcs) $($(name)-gens) $($(name)-extra-specs))), \ + $(sort $(notdir $($(name)-proof) \ + $($(name)-srcs) $($(name)-gens) $($(name)-extra-specs) $($(name)-extra-gens))), \ $(sort $(notdir \ $(wildcard $(addsuffix *.ad[sb],$($(name)-proof-dirs))))))
@@ -62,7 +63,9 @@ echo ' for Object_Dir use external ("obj", "build");' >>$@ echo 'end lib$(name);' >>$@
-$(obj)/gnatprove/gnatprove.out: $(gpr) $$($(name)-srcs) $$($(name)-gens) $(obj)/proofmode +$(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: