Add support to clightgen for generating Csyntax AST as .v files

As proposed in #404.

This is presented as a new option `-clight` to the existing `clightgen` tool.

Revise clightgen testing to test the Csyntax output in addition to
the Clight output.

10 files changed, 23 insertions, 11 deletions

diff --git a/test/Makefile b/test/Makefile
index fa1fef30..ccf8fcd7 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -2,7 +2,7 @@ include ../Makefile.config
 
 DIRS=c compression raytracer spass regression abi
 ifeq ($(CLIGHTGEN),true)
-DIRS+=clightgen
+DIRS+=export
 endif
 
 all:
diff --git a/test/clightgen/Makefile b/test/export/Makefile
index 83ba0fd3..d1228bf9 100644
--- a/test/clightgen/Makefile
+++ b/test/export/Makefile
@@ -10,7 +10,8 @@ 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
@@ -26,6 +27,8 @@ SRC+=aes.c almabench.c binarytrees.c bisect.c chomp.c fannkuch.c fft.c \
 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
@@ -34,23 +37,32 @@ fft.vo fftsp.vo fftw.vo fib.vo integr.vo knucleotide.vo: CFLAGS += -short-idents
 
 qsort.vo sha1.vo sha3.vo siphash24.vo spectral.vo vmach.vo: CFLAGS += -normalize
 
-all: $(SRC:.c=.vo)
+all: $(GENERATED:.v=.vo)
 
 test:
 
-%.v: %.c
-	$(CLIGHTGEN) $(CFLAGS) -o $@ $<
+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 $@ $<
 
-%.v: ../c/%.c
-	$(CLIGHTGEN) $(CFLAGS) -o $@ $<
+csyntax/%.v: ../c/%.c
+	$(CLIGHTGEN) -csyntax $(CFLAGS) -o $@ $<
 
-%.v: ../raytracer/%.c
-	$(CLIGHTGEN) -I../raytracer -fall $(CFLAGS) -o $@ $<
+csyntax/%.v: ../raytracer/%.c
+	$(CLIGHTGEN) -csyntax -I../raytracer -fall $(CFLAGS) -o $@ $<
 
 %.vo: %.v
 	$(COQC) $(COQINCLUDES) -noglob $<
 
-.SECONDARY: $(SRC:.c=.v)
+.SECONDARY: $(GENERATED)
 
 clean:
-	rm -f *.v *.vo* .*.aux
+	for d in clight csyntax; do rm -f $$d/*.v $$d/*.vo $$d/.*.aux; done
diff --git a/test/clightgen/annotations.c b/test/export/annotations.c
index 993fa7d0..993fa7d0 100644
--- a/test/clightgen/annotations.c
+++ b/test/export/annotations.c
diff --git a/test/clightgen/bitfields.c b/test/export/bitfields.c
index 34f6a686..34f6a686 100644
--- a/test/clightgen/bitfields.c
+++ b/test/export/bitfields.c
diff --git a/test/export/clight/.gitkeep b/test/export/clight/.gitkeep
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/test/export/clight/.gitkeep
diff --git a/test/export/csyntax/.gitkeep b/test/export/csyntax/.gitkeep
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/test/export/csyntax/.gitkeep
diff --git a/test/clightgen/empty.c b/test/export/empty.c
index 8f8871a7..8f8871a7 100644
--- a/test/clightgen/empty.c
+++ b/test/export/empty.c
diff --git a/test/clightgen/issue196.c b/test/export/issue196.c
index 1821fd6d..1821fd6d 100644
--- a/test/clightgen/issue196.c
+++ b/test/export/issue196.c
diff --git a/test/clightgen/issue216.c b/test/export/issue216.c
index 796b69b4..796b69b4 100644
--- a/test/clightgen/issue216.c
+++ b/test/export/issue216.c
diff --git a/test/clightgen/issue319.c b/test/export/issue319.c
index be9f3f7e..be9f3f7e 100644
--- a/test/clightgen/issue319.c
+++ b/test/export/issue319.c