From 1348bc74b48ea8cb366a8bfab379699137276292 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Apr 2020 22:33:26 +0200
Subject: fixing Makefile

---
 test/monniaux/minisat/Makefile.profiled | 14 +++++++++-----
 test/monniaux/minisat/k1c.inline_50.log | 14 ++++++++++++++
 2 files changed, 23 insertions(+), 5 deletions(-)
 create mode 100644 test/monniaux/minisat/k1c.inline_50.log

(limited to 'test/monniaux/minisat')

diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled
index 64e7cb80..b3b3c2fc 100644
--- a/test/monniaux/minisat/Makefile.profiled
+++ b/test/monniaux/minisat/Makefile.profiled
@@ -3,11 +3,15 @@
 CFILES=main.c solver.c clock.c
 GCDAFILES=$(CFILES:.c=.gcda)
 CCOMP=../../../ccomp
-GCC=aarch64-linux-gnu-gcc  # k1-cos-gcc
+
+GCC=aarch64-linux-gnu-gcc
+GCC=k1-cos-gcc
+EXECUTE=qemu-aarch64
+EXECUTE=k1-cluster --
+EXECUTE_CYCLES=k1-cluster --cycle-based --
+
 LIBS=-lm
 PROFILING_DAT=compcert_profiling.dat
-EXECUTE=qemu-aarch64 # k1-cluster --
-EXECUTE_CYCLES=k1-cluster --cycle-based --
 EXAMPLE=sudoku.sat
 CCOMPFLAGS=-finline-auto-threshold 50 -static -finline-asm
 GCCFLAGS=-static
@@ -37,11 +41,11 @@ minisat.gcc-O3.profiled.exe: $(CFILES) $(GCDAFILES)
 	$(GCC) $(GCCFLAGS) -O3 -fprofile-use $(CFILES) -o $@ $(LIBS)
 
 minisat.ccomp.trace-linearize.exe: $(CFILES)
-	$(CCOMP) $(CCOMPFLAGS) -ftracelinearize $(CFILES) -o $@ $(LIBS)
+	$(CCOMP) $(CCOMPFLAGS) -fduplicate 0 -ftracelinearize $(CFILES) -o $@ $(LIBS)
 
 $(PROFILING_DAT): minisat.ccomp.profile-arcs.exe
 	-rm -f $(PROFILING_DAT)
-	$(EXECUTE) $< $(EXAMPLE) || true
+	$(EXECUTE) $< $(EXAMPLE)
 
 minisat.ccomp.profiled.exe: $(CFILES) $(PROFILING_DAT)
 	$(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -ftracelinearize $(CFILES) -o $@ $(LIBS)
diff --git a/test/monniaux/minisat/k1c.inline_50.log b/test/monniaux/minisat/k1c.inline_50.log
new file mode 100644
index 00000000..438a06b4
--- /dev/null
+++ b/test/monniaux/minisat/k1c.inline_50.log
@@ -0,0 +1,14 @@
+==> minisat.ccomp.log <==
+time cycles: 3252345
+
+==> minisat.ccomp.profiled.log <==
+time cycles: 3150170
+
+==> minisat.ccomp.trace-linearize.log <==
+time cycles: 3192299
+
+==> minisat.gcc-O3.log <==
+time cycles: 2780324
+
+==> minisat.gcc-O3.profiled.log <==
+time cycles: 2487533
-- 
cgit