diff options
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 |