Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10

10 files changed, 24 insertions, 12 deletions

diff --git a/test/Makefile b/test/Makefile
index 50cf57fb..b0010ea0 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -11,7 +11,7 @@ else
 endif
 
 ifeq ($(CLIGHTGEN),true)
-DIRS+=clightgen
+DIRS+=export
 endif
 
 all:
diff --git a/test/clightgen/Makefile b/test/export/Makefile
index f0e9d961..d1228bf9 100644
--- a/test/clightgen/Makefile
+++ b/test/export/Makefile
@@ -5,12 +5,13 @@ ARCHDIRS=$(ARCH)
 else
 ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
 endif
-RECDIRS := lib common $(ARCHDIRS) cfrontend  exportclight
+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
@@ -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