Makefile.proof: Add full paths and config to diagnostic output
GCC and GNATprove only print the file name in diagnostic messages, not
its full path. We'll replace the file name for all known files in the
configuration built for. For the `proof-allconfigs` target, we also
prefix the line with the current configuration (e.g. `linux::`).
Change-Id: Ia71ee4b780d61ad6c583515d74e8669d1a259675
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.sourcearcade.org/c/libhwbase/+/472
Tested-by: Ada SPARK <gnatbot@sourcearcade.org>
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
diff --git a/Makefile.proof b/Makefile.proof
index 593b41e..a08e91c 100644
--- a/Makefile.proof
+++ b/Makefile.proof
@@ -64,11 +64,21 @@
echo ' for Object_Dir use external ("obj", "build");' >>$@
echo 'end lib$(name);' >>$@
+# We want to filter gnatprove's command-line output through `sed`,
+# and *also* capture its return value. Not that easy, we'll pipe the
+# return code through file descriptor #3.
+#
+# 1: command w/ return value
+# 2: filter command, ignore return value
+#
+filter-output = { { { { $(1); } 2>&1; echo $$? >&3; } | $(2) >&2; } 3>&1 | { read ret; exit $${ret}; }; } 2>&1
+
$(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))
-
+ $(call filter-output, \
+ gnatprove -P$< $(SPARKFLAGS) -Xobj=$(abspath $(obj)), \
+ sed $(foreach file,$^,-e 's|$(notdir $(file)):[0-9]\+:[0-9]\+:|$(dir $(file))&|'))
proof:
if [ "$(PROOF_MODE)" != "$$(cat $(obj)/proofmode 2>/dev/null)" ]; then \
echo "$(PROOF_MODE)" >$(obj)/proofmode; \
@@ -91,7 +101,10 @@
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
+ $(call filter-output, \
+ $(MAKE) obj=proof-allconfigs/$* cnf=configs/$* gpr=$(name)_$*.gpr jobs=1 \
+ proof-allconfigs/$*/gnatprove/gnatprove.out, \
+ sed 's/^[^[:space:]]\+:[0-9]\+:[0-9]\+:/$*::&/')
proof-allconfigs: $(allconfigs-targets)