blob: d1228bf9c185b7808f2673e233313d25462ef0b1 (
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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
include ../../Makefile.config
ifeq ($(wildcard ../../$(ARCH)_$(BITSIZE)),)
ARCHDIRS=$(ARCH)
else
ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
endif
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
# 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
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
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: $(GENERATED:.v=.vo)
test:
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 $@ $<
csyntax/%.v: ../c/%.c
$(CLIGHTGEN) -csyntax $(CFLAGS) -o $@ $<
csyntax/%.v: ../raytracer/%.c
$(CLIGHTGEN) -csyntax -I../raytracer -fall $(CFLAGS) -o $@ $<
%.vo: %.v
$(COQC) $(COQINCLUDES) -noglob $<
.SECONDARY: $(GENERATED)
clean:
for d in clight csyntax; do rm -f $$d/*.v $$d/*.vo $$d/.*.aux; done
|
