From 112beeee204d4a06b8c39e9554255261365f3fed Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Apr 2020 14:09:21 +0200
Subject: Makefile for profiling

---
 test/monniaux/minisat/Makefile.profiled | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 test/monniaux/minisat/Makefile.profiled

(limited to 'test/monniaux/minisat/Makefile.profiled')

diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled
new file mode 100644
index 00000000..febac0d5
--- /dev/null
+++ b/test/monniaux/minisat/Makefile.profiled
@@ -0,0 +1,21 @@
+CFILES=main.c solver.c ../clock.c
+CCOMP=../../../ccomp
+CCOMPFLAGS=
+PROFILING_DAT=compcert_profiling.dat
+EXECUTE=k1-cluster --
+EXAMPLE=sudoku.sat
+
+all: minisat.ccomp minisat.branch_linearize minisat.profiled
+
+minisat.ccomp: $(CFILES)
+	$(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@
+
+minisat.branch_linearize: $(CFILES)
+	$(CCOMP) $(CCOMPFLAGS) -fbranchlinearize $(CFILES) -o $@
+
+$(PROFILING_DAT): minisat.profile_arcs
+	-rm -f $(PROFILING_DAT)
+	$(EXECUTE) $< $(EXAMPLE)
+
+minisat.profiled: $(CFILES) $(PROFILING_DAT)
+	$(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -fbranchlinearize $(CFILES) -o $@
-- 
cgit