diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-01 10:22:31 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-01 10:23:38 +0200 |
commit | ffc03f2dcb24438d2900743848005c9a058e649c (patch) | |
tree | cc861e334a4dbd0990038e870d34ff185ecafe7c /test/clightgen/Makefile | |
parent | 27ff8beb35cc4fd1e6a05c6685a7903e9e64ecdf (diff) | |
download | compcert-ffc03f2dcb24438d2900743848005c9a058e649c.tar.gz compcert-ffc03f2dcb24438d2900743848005c9a058e649c.zip |
Add tests for clightgen
Also: add "parallel" entry to test/Makefile for parallel execution of tests.
Diffstat (limited to 'test/clightgen/Makefile')
-rw-r--r-- | test/clightgen/Makefile | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/test/clightgen/Makefile b/test/clightgen/Makefile new file mode 100644 index 00000000..208c2d0d --- /dev/null +++ b/test/clightgen/Makefile @@ -0,0 +1,44 @@ +include ../../Makefile.config + +ifeq ($(wildcard ../../$(ARCH)_$(BITSIZE)),) +ARCHDIRS=$(ARCH) +else +ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) +endif +RECDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight +COQINCLUDES=$(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d)) + +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 + +all: $(SRC:.c=.vo) + +test: + +%.v: %.c $(CLIGHTGEN) + $(CLIGHTGEN) $(CFLAGS) -o $@ $< + +%.v: ../c/%.c $(CLIGHTGEN) + $(CLIGHTGEN) $(CFLAGS) -o $@ $< + +%.v: ../raytracer/%.c $(CLIGHTGEN) + $(CLIGHTGEN) -I../raytracer -fall $(CFLAGS) -o $@ $< + +%.vo: %.v + $(COQC) $(COQINCLUDES) -noglob $< + +.SECONDARY: $(SRC:.c=.v) + +clean: + rm -f *.v *.vo |