diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-09-30 13:23:42 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-09-30 13:23:42 +0200 |
commit | ef508dae3e880bdd30e9d57ca2a8b3e257b1203b (patch) | |
tree | 0cb08c27aeef48ca154525378419f5b129793b2b /test/export/Makefile | |
parent | dbada6c41e51a03848b14260576ba825c3102313 (diff) | |
parent | 539b81a1a8823fb4aac64a9493bf0bafea2f2560 (diff) | |
download | compcert-kvx-ef508dae3e880bdd30e9d57ca2a8b3e257b1203b.tar.gz compcert-kvx-ef508dae3e880bdd30e9d57ca2a8b3e257b1203b.zip |
Merge branch 'towards_2.10' of ../towards_3.10 into kvx-work
Diffstat (limited to 'test/export/Makefile')
-rw-r--r-- | test/export/Makefile | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/test/export/Makefile b/test/export/Makefile new file mode 100644 index 00000000..d1228bf9 --- /dev/null +++ b/test/export/Makefile @@ -0,0 +1,68 @@ +include ../../Makefile.config + +ifeq ($(wildcard ../../$(ARCH)_$(BITSIZE)),) +ARCHDIRS=$(ARCH) +else +ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) +endif +RECDIRS := lib common $(ARCHDIRS) cfrontend export +COQINCLUDES := $(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d)) +ifeq ($(LIBRARY_FLOCQ),local) +COQINCLUDES += -R ../../flocq Flocq +endif +COQINCLUDES += -R ./clight compcert.test.clight +COQINCLUDES += -R ./csyntax compcert.test.csyntax + +CLIGHTGEN=../../clightgen +COQC=coqc + +# Regression tests in the current directory +SRC=$(wildcard *.c) +# From ../c +SRC+=aes.c almabench.c binarytrees.c bisect.c chomp.c fannkuch.c fft.c \ + fftsp.c fftw.c fib.c integr.c knucleotide.c lists.c mandelbrot.c \ + nbody.c nsievebits.c nsieve.c perlin.c qsort.c sha1.c sha3.c \ + siphash24.c spectral.c vmach.c +# From ../raytracer +SRC+=arrays.c eval.c gmllexer.c gmlparser.c intersect.c light.c main.c \ + matrix.c memory.c object.c render.c simplify.c surface.c vector.c + +GENERATED=$(SRC:%.c=clight/%.v) $(SRC:%.c=csyntax/%.v) + +CFLAGS=-DSYSTEM_$(SYSTEM) + +aes.vo almabench.vo binarytrees.vo bisect.vo chomp.vo: CFLAGS += -short-idents + +fft.vo fftsp.vo fftw.vo fib.vo integr.vo knucleotide.vo: CFLAGS += -short-idents -normalize + +qsort.vo sha1.vo sha3.vo siphash24.vo spectral.vo vmach.vo: CFLAGS += -normalize + +all: $(GENERATED:.v=.vo) + +test: + +clight/%.v: %.c + $(CLIGHTGEN) -clight $(CFLAGS) -o $@ $< + +clight/%.v: ../c/%.c + $(CLIGHTGEN) -clight $(CFLAGS) -o $@ $< + +clight/%.v: ../raytracer/%.c + $(CLIGHTGEN) -clight -I../raytracer -fall $(CFLAGS) -o $@ $< + +csyntax/%.v: %.c + $(CLIGHTGEN) -csyntax $(CFLAGS) -o $@ $< + +csyntax/%.v: ../c/%.c + $(CLIGHTGEN) -csyntax $(CFLAGS) -o $@ $< + +csyntax/%.v: ../raytracer/%.c + $(CLIGHTGEN) -csyntax -I../raytracer -fall $(CFLAGS) -o $@ $< + +%.vo: %.v + $(COQC) $(COQINCLUDES) -noglob $< + +.SECONDARY: $(GENERATED) + +clean: + for d in clight csyntax; do rm -f $$d/*.v $$d/*.vo $$d/.*.aux; done |