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:36:51 +0100 |
commit | 402a7c3eead452af1d40a2cf5d51907a07473640 (patch) | |
tree | 79f5e2413dca4bb477a81c37ad7497674e288b38 | |
parent | bac833845208a4c0b0e28ddace1b34a1a5598e64 (diff) | |
download | compcert-kvx-402a7c3eead452af1d40a2cf5d51907a07473640.tar.gz compcert-kvx-402a7c3eead452af1d40a2cf5d51907a07473640.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 |