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