diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-22 22:36:51 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-22 22:37:43 +0100 |
commit | 54660295442d0608fa0b56659dd3b17f34ffbc70 (patch) | |
tree | 0790e6b10e97b386dc3faf30df89bb58f0b5fad2 | |
parent | 85f61cd1790d588b933841b6bbe113dabe144301 (diff) | |
download | compcert-kvx-54660295442d0608fa0b56659dd3b17f34ffbc70.tar.gz compcert-kvx-54660295442d0608fa0b56659dd3b17f34ffbc70.zip |
for testing with quest
-rw-r--r-- | test/monniaux/quest/Makefile | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/monniaux/quest/Makefile b/test/monniaux/quest/Makefile new file mode 100644 index 00000000..c049238b --- /dev/null +++ b/test/monniaux/quest/Makefile @@ -0,0 +1,24 @@ +# install Quest using: opam install quest +MAX=300 + +include ../rules.mk + +QUEST=quest +K1C_CCOMPFLAGS += -fstruct-passing -fbitfields + +PREFIX=ran%06.f +TARGETS_C=$(shell seq --format $(PREFIX).c 0 $(MAX)) +TARGETS_OUT=$(shell seq --format $(PREFIX).ccomp.k1c.out 0 $(MAX)) + +all: $(TARGETS_C) $(TARGETS_OUT) + +ran%.c : + $(QUEST) -seed $* -test ansi > $@ + +%.ccomp.k1c : %.ccomp.k1c.s + $(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@ + +clean: + -rm -f $(TARGETS_C) $(TARGETS_OUT) + +.PHONY: all clean |