diff options
Diffstat (limited to 'test/clightgen/Makefile')
| -rw-r--r-- | test/clightgen/Makefile | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/test/clightgen/Makefile b/test/clightgen/Makefile index 0607e2fa..f0e9d961 100644 --- a/test/clightgen/Makefile +++ b/test/clightgen/Makefile @@ -5,8 +5,12 @@ ARCHDIRS=$(ARCH) else ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) endif -RECDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight -COQINCLUDES=$(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d)) +RECDIRS := lib common $(ARCHDIRS) cfrontend exportclight +COQINCLUDES := $(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d)) +ifeq ($(LIBRARY_FLOCQ),local) +COQINCLUDES += -R ../../flocq Flocq +endif + CLIGHTGEN=../../clightgen COQC=coqc @@ -22,6 +26,14 @@ 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 +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: $(SRC:.c=.vo) test: @@ -41,4 +53,4 @@ test: .SECONDARY: $(SRC:.c=.v) clean: - rm -f *.v *.vo .*.aux + rm -f *.v *.vo* .*.aux |