blob: fdfbc3fbd0a6520b849f7b256b79268c0eb908a1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
include ../../Makefile.config
ifeq ($(wildcard ../../$(ARCH)_$(BITSIZE)),)
ARCHDIRS=$(ARCH)
else
ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
endif
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
# 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
CFLAGS=-DSYSTEM_$(SYSTEM)
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
|
