1 files changed, 44 insertions, 0 deletions
diff --git a/test/clightgen/Makefile b/test/clightgen/Makefile
new file mode 100644
index 00000000..0607e2fa
--- /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) $(CFLAGS) -o $@ $<
+
+%.v: ../c/%.c
+	$(CLIGHTGEN) $(CFLAGS) -o $@ $<
+
+%.v: ../raytracer/%.c
+	$(CLIGHTGEN) -I../raytracer -fall $(CFLAGS) -o $@ $<
+
+%.vo: %.v
+	$(COQC) $(COQINCLUDES) -noglob $<
+
+.SECONDARY: $(SRC:.c=.v)
+
+clean:
+	rm -f *.v *.vo .*.aux