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

---
 test/monniaux/minisat/Makefile.profiled | 28 +++++++++++++++++-----------
 1 file changed, 17 insertions(+), 11 deletions(-)

(limited to 'test')

diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled
index c5f68fe8..abd63d32 100644
--- a/test/monniaux/minisat/Makefile.profiled
+++ b/test/monniaux/minisat/Makefile.profiled
@@ -5,43 +5,49 @@ GCC=k1-cos-gcc
 LIBS=-lm
 PROFILING_DAT=compcert_profiling.dat
 EXECUTE=k1-cluster --
+EXECUTE_CYCLES=k1-cluster --cycle-based --
 EXAMPLE=sudoku.sat
 
-ALL=minisat.ccomp minisat.branch_linearize minisat.profiled minisat.gcc-O3 minisat.gcc-O3.profiled minisat.gcc-O3.profile-arcs minisat.profile-arcs
+ALL=minisat.ccomp.log minisat.branch_linearize.log minisat.profiled.log minisat.gcc-O3.log minisat.gcc-O3.profiled.log
 
 all: $(ALL)
 
-minisat.ccomp: $(CFILES)
+minisat.ccomp.exe: $(CFILES)
 	$(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@ $(LIBS)
 
-minisat.profile-arcs: $(CFILES)
+minisat.ccomp.profile-arcs.exe: $(CFILES)
 	$(CCOMP) $(CCOMPFLAGS) -fprofile-arcs $(CFILES) -o $@ $(LIBS)
 
-minisat.gcc-O3: $(CFILES)
+minisat.gcc-O3.exe: $(CFILES)
 	$(GCC) $(GCCFLAGS) -O3 $(CFILES) -o $@ $(LIBS)
 
-minisat.gcc-O3.profile-arcs: $(CFILES)
+minisat.gcc-O3.profile-arcs.exe: $(CFILES)
 	$(GCC) $(GCCFLAGS) -fprofile-arcs -O3 $(CFILES) -o $@ $(LIBS)
 
-gcda: minisat.gcc-O3.profile-arcs
+gcda: minisat.gcc-O3.profile-arcs.exe
 	$(EXECUTE) $< $(EXAMPLE)
 
 $(GCDAFILES): gcda
 
-minisat.gcc-O3.profiled: $(CFILES) $(GCDAFILES)
+minisat.gcc-O3.profiled.exe: $(CFILES) $(GCDAFILES)
 	$(GCC) $(GCCFLAGS) -O3 -fprofile-use $(CFILES) -o $@ $(LIBS)
 
-minisat.branch_linearize: $(CFILES)
+minisat.ccomp.trace_linearize.exe: $(CFILES)
 	$(CCOMP) $(CCOMPFLAGS) -ftracelinearize $(CFILES) -o $@ $(LIBS)
 
-$(PROFILING_DAT): minisat.profile-arcs
+$(PROFILING_DAT): minisat.ccomp.profile-arcs.exe
 	-rm -f $(PROFILING_DAT)
 	$(EXECUTE) $< $(EXAMPLE)
 
-minisat.profiled: $(CFILES) $(PROFILING_DAT)
-	$(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -fbranchlinearize $(CFILES) -o $@ $(LIBS)
+minisat.ccomp.profiled.exe: $(CFILES) $(PROFILING_DAT)
+	$(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -ftracelinearize $(CFILES) -o $@ $(LIBS)
+
+%.log : %.exe
+	$(EXECUTE_CYCLES) $< $(EXAMPLE) 2>&1 | tee $@
 
 clean:
 	-rm -f $(ALL) $(PROFILING_DAT) $(GCDAFILES)
 
 .PHONY: clean gcda
+
+.SECONDARY:
-- 
cgit