diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-06 22:27:16 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-06 22:27:16 +0200 |
| commit | a7403ea5e4fe72bb3cd62a71cf5148e0f4f2097d (patch) | |
| tree | dab00d21c35619559ab8d07e84c0d319c59de3fe /test/monniaux/minisat | |
| parent | 960bd0a18b8422f623ccdff19f5aca9f424b895c (diff) | |
| download | compcert-kvx-a7403ea5e4fe72bb3cd62a71cf5148e0f4f2097d.tar.gz compcert-kvx-a7403ea5e4fe72bb3cd62a71cf5148e0f4f2097d.zip | |
compilation
Diffstat (limited to 'test/monniaux/minisat')
| -rw-r--r-- | test/monniaux/minisat/Makefile | 36 | ||||
| -rw-r--r-- | test/monniaux/minisat/make.proto | 2 |
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 |