diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/Makefile | 2 | ||||
-rw-r--r-- | test/export/Makefile (renamed from test/clightgen/Makefile) | 32 | ||||
-rw-r--r-- | test/export/annotations.c (renamed from test/clightgen/annotations.c) | 0 | ||||
-rw-r--r-- | test/export/bitfields.c (renamed from test/clightgen/bitfields.c) | 0 | ||||
-rw-r--r-- | test/export/clight/.gitkeep | 0 | ||||
-rw-r--r-- | test/export/csyntax/.gitkeep | 0 | ||||
-rw-r--r-- | test/export/empty.c (renamed from test/clightgen/empty.c) | 0 | ||||
-rw-r--r-- | test/export/issue196.c (renamed from test/clightgen/issue196.c) | 0 | ||||
-rw-r--r-- | test/export/issue216.c (renamed from test/clightgen/issue216.c) | 0 | ||||
-rw-r--r-- | test/export/issue319.c (renamed from test/clightgen/issue319.c) | 0 |
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 |