From 07247055911bc1a436e469a3114649d3bb317d73 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Apr 2020 14:19:33 +0200
Subject: for profiling

---
 test/monniaux/minisat/Makefile.profiled | 33 +++++++++++++++++++++++++++------
 test/monniaux/minisat/clock.c           |  1 +
 2 files changed, 28 insertions(+), 6 deletions(-)
 create mode 120000 test/monniaux/minisat/clock.c

(limited to 'test')

diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled
index febac0d5..08283c8a 100644
--- a/test/monniaux/minisat/Makefile.profiled
+++ b/test/monniaux/minisat/Makefile.profiled
@@ -1,21 +1,42 @@
-CFILES=main.c solver.c ../clock.c
+CFILES=main.c solver.c clock.c
+GCDAFILES=$(CFILES:.c=.gcda)
 CCOMP=../../../ccomp
-CCOMPFLAGS=
+GCC=k1-cos-gcc
+LIBS=-lm
 PROFILING_DAT=compcert_profiling.dat
 EXECUTE=k1-cluster --
 EXAMPLE=sudoku.sat
 
-all: minisat.ccomp minisat.branch_linearize minisat.profiled
+ALL=minisat.ccomp minisat.branch_linearize minisat.profiled minisat.gcc-O3 minisat.gcc-O3.profiled
+
+all: $(ALL)
 
 minisat.ccomp: $(CFILES)
-	$(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@
+	$(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@ $(LIBS)
+
+minisat.gcc-O3: $(CFILES)
+	$(GCC) $(GCCFLAGS) -O3 $(CFILES) -o $@ $(LIBS)
+
+minisat.gcc-O3.profile-arcs: $(CFILES)
+	$(GCC) $(GCCFLAGS) -fprofile-arcs -O3 $(CFILES) -o $@ $(LIBS)
+
+$(GCDAFILES): minisat.gcc-O3.profile-arcs
+	$(EXECUTE) $< $(EXAMPLE)
+
+minisat.gcc-O3.profiled: $(CFILES) $(GCDAFILES)
+	$(GCC) $(GCCFLAGS) -O3 -fprofile-use $(CFILES) -o $@ $(LIBS)
 
 minisat.branch_linearize: $(CFILES)
-	$(CCOMP) $(CCOMPFLAGS) -fbranchlinearize $(CFILES) -o $@
+	$(CCOMP) $(CCOMPFLAGS) -fbranchlinearize $(CFILES) -o $@ $(LIBS)
 
 $(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 $@
+	$(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -fbranchlinearize $(CFILES) -o $@ $(LIBS)
+
+clean:
+	-rm -f $(ALL) $(PROFILING_DAT) $(GCDAFILES)
+
+.PHONY: clean
diff --git a/test/monniaux/minisat/clock.c b/test/monniaux/minisat/clock.c
new file mode 120000
index 00000000..d6bade99
--- /dev/null
+++ b/test/monniaux/minisat/clock.c
@@ -0,0 +1 @@
+../clock.c
\ No newline at end of file
-- 
cgit