[coreboot-gerrit] Change in ...libhwbase[master]: Makefile: Revise support for generated sources

[Nico Huber (Code Review)]

Nico Huber has submitted this change and it was merged. ( https://review.coreboot.org/c/libhwbase/+/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.

As with the source file list, we filter the list of generated sources,
`$(name)-gens`: All spec (.ads) files that have a respective body file
(.adb), are moved into `$(name)-extra-gens`. This way, we can still
add these files as dependencies to all pre-existing source files.

Change-Id: I5479c436f39088ae9d0ebddf9a97446be0f191f3
Signed-off-by: Nico Huber 
Reviewed-on: https://review.coreboot.org/c/libhwbase/+/27139
Reviewed-by: Angel Pons 
Reviewed-by: Stefan Reinauer 
Reviewed-by: Patrick Georgi 
---
M Makefile
M Makefile.proof
2 files changed, 16 insertions(+), 9 deletions(-)

Approvals:
  Nico Huber: Verified
  Patrick Georgi: Looks good to me, approved
  Stefan Reinauer: Looks good to me, approved
  Angel Pons: Looks good to me, but someone else must approve

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 729ecab..593b41e 100644
--- a/Makefile.proof
+++ b/Makefile.proof
@@ -18,7 +18,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))))))

@@ -63,7 +64,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: