Add profile feedback build to git

diff --git a/Makefile b/Makefile
index 03b4499d52c8f0870479ec265fb23dce111f853d..2d7f6ba122ec93e8006937a94340d01c6816546e 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -2492,3 +2492,19 @@ cover_db: coverage-report
 
 cover_db_html: cover_db
        cover -report html -outputdir cover_db_html cover_db
+
+### profile feedback build
+#
+.PHONY: profile-all profile-clean
+
+PROFILE_GEN_CFLAGS := $(CFLAGS) -fprofile-generate -DNO_NORETURN=1
+PROFILE_USE_CFLAGS := $(CFLAGS) -fprofile-use -fprofile-correction -DNO_NORETURN=1
+
+profile-clean:
+       $(RM) $(addsuffix *.gcda,$(object_dirs))
+       $(RM) $(addsuffix *.gcno,$(object_dirs))
+
+profile-all: profile-clean
+       $(MAKE) CFLAGS="$(PROFILE_GEN_CFLAGS)" all
+       $(MAKE) CFLAGS="$(PROFILE_GEN_CFLAGS)" -j1 test
+       $(MAKE) CFLAGS="$(PROFILE_USE_CFLAGS)" all