aboutsummaryrefslogtreecommitdiffstats
path: root/test/monniaux/minisat
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-06-06 22:27:16 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-06-06 22:27:16 +0200
commita7403ea5e4fe72bb3cd62a71cf5148e0f4f2097d (patch)
treedab00d21c35619559ab8d07e84c0d319c59de3fe /test/monniaux/minisat
parent960bd0a18b8422f623ccdff19f5aca9f424b895c (diff)
downloadcompcert-kvx-a7403ea5e4fe72bb3cd62a71cf5148e0f4f2097d.tar.gz
compcert-kvx-a7403ea5e4fe72bb3cd62a71cf5148e0f4f2097d.zip
compilation
Diffstat (limited to 'test/monniaux/minisat')
-rw-r--r--test/monniaux/minisat/Makefile36
-rw-r--r--test/monniaux/minisat/make.proto2
2 files changed, 38 insertions, 0 deletions
diff --git a/test/monniaux/minisat/Makefile b/test/monniaux/minisat/Makefile
new file mode 100644
index 00000000..f98b69b7
--- /dev/null
+++ b/test/monniaux/minisat/Makefile
@@ -0,0 +1,36 @@
+
+include ../rules.mk
+
+EXECUTE_ARGS=sudoku.sat
+
+src=main.c solver.c
+
+PRODUCTS?=minisat.gcc.host minisat.ccomp.host minisat.gcc.k1c minisat.gcc.o1.k1c minisat.ccomp.k1c
+PRODUCTS_OUT=$(addsuffix .out,$(PRODUCTS))
+
+all: $(PRODUCTS)
+
+.PHONY:
+run: measures.csv
+
+LIBS=-lm
+
+minisat.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o
+ $(CC) $(CFLAGS) $+ $(LIBS) -o $@
+minisat.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o
+ $(CCOMP) $(CCOMPFLAGS) $+ $(LIBS) -o $@
+minisat.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o
+ $(K1C_CC) $(K1C_CFLAGS) $+ $(LIBS) -o $@
+minisat.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o
+ $(K1C_CC) $(K1C_CFLAGS_O1) $+ $(LIBS) -o $@
+minisat.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o
+ $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ $(LIBS) -o $@
+measures.csv: $(PRODUCTS_OUT)
+ echo "benches, gcc host,ccomp host,gcc k1c,gcc o1 k1c,ccomp k1c" > $@
+
+.SECONDARY:
+
+.PHONY:
+clean:
+ rm -f *.o *.s *.k1c *.csv
+
diff --git a/test/monniaux/minisat/make.proto b/test/monniaux/minisat/make.proto
new file mode 100644
index 00000000..d86da4de
--- /dev/null
+++ b/test/monniaux/minisat/make.proto
@@ -0,0 +1,2 @@
+sources: main.c solver.c
+target: minisat \ No newline at end of file