blob: 58d494c09fb43c99b72846d27aadc1ce2b6d14f2 (
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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
#######################################################################
# #
# The Compcert verified compiler #
# #
# Xavier Leroy, INRIA Paris-Rocquencourt #
# #
# Copyright Institut National de Recherche en Informatique et en #
# Automatique. All rights reserved. This file is distributed #
# under the terms of the INRIA Non-Commercial License Agreement. #
# #
#######################################################################
include Makefile.config
COQC=coqc $(INCLUDES)
COQDEP=coqdep $(INCLUDES)
COQDOC=coqdoc
INCLUDES=-I lib -I common -I backend -I cfrontend
# Files in lib/
LIB=Coqlib.v Maps.v Lattice.v Ordered.v \
Iteration.v Integers.v Floats.v Parmov.v
# Files in common/
COMMON=Errors.v AST.v Events.v Globalenvs.v Mem.v Values.v \
Smallstep.v Switch.v Main.v Complements.v
# Files in backend/
BACKEND=\
Cminor.v Op.v CminorSel.v \
Selection.v Selectionproof.v \
Registers.v RTL.v \
RTLgen.v RTLgenspec.v RTLgenproof.v \
RTLtyping.v \
Kildall.v \
Constprop.v Constpropproof.v \
CSE.v CSEproof.v \
Locations.v Conventions.v LTL.v LTLtyping.v \
InterfGraph.v Coloring.v Coloringproof.v \
Allocation.v Allocproof.v Alloctyping.v \
Tunneling.v Tunnelingproof.v Tunnelingtyping.v \
LTLin.v LTLintyping.v \
Linearize.v Linearizeproof.v Linearizetyping.v \
Linear.v Lineartyping.v \
Parallelmove.v Reload.v Reloadproof.v Reloadtyping.v \
Mach.v Machabstr.v Machtyping.v \
Bounds.v Stacking.v Stackingproof.v Stackingtyping.v \
Machconcr.v Machabstr2concr.v \
PPC.v PPCgen.v PPCgenretaddr.v PPCgenproof1.v PPCgenproof.v
# Files in cfrontend/
CFRONTEND=Csyntax.v Csem.v Ctyping.v Cshmgen.v \
Cshmgenproof1.v Cshmgenproof2.v Cshmgenproof3.v \
Csharpminor.v Cminorgen.v Cminorgenproof.v
# All source files
FILES=$(LIB:%=lib/%) $(COMMON:%=common/%) $(BACKEND:%=backend/%) $(CFRONTEND:%=cfrontend/%)
FLATFILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND)
proof: $(FILES:.v=.vo)
all:
$(MAKE) proof
$(MAKE) -C cil
$(MAKE) -C extraction extraction
$(MAKE) -C extraction depend
$(MAKE) -C extraction
$(MAKE) -C runtime
documentation: doc/removeproofs
@ln -f $(FILES) doc/
@mkdir -p doc/html
cd doc; $(COQDOC) --html -d html \
$(FLATFILES:%.v=--glob-from %.glob) $(FLATFILES)
@cd doc; rm -f $(FLATFILES)
cp doc/coqdoc.css doc/html/coqdoc.css
doc/removeproofs doc/html/*.html
doc/removeproofs: doc/removeproofs.ml
ocamlopt -o doc/removeproofs doc/removeproofs.ml
doc/removeproofs.ml: doc/removeproofs.mll
ocamllex doc/removeproofs.mll
latexdoc:
cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES)
.SUFFIXES: .v .vo
.v.vo:
@rm -f doc/glob/$(*F).glob
@echo "COQC $*.v"
@$(COQC) -dump-glob doc/$(*F).glob $*.v
depend:
$(COQDEP) $(FILES) > .depend
install:
$(MAKE) -C extraction install
$(MAKE) -C runtime install
clean:
rm -f */*.vo *~ */*~
rm -rf doc/html doc/*.glob
rm -f doc/removeproofs.ml doc/removeproofs
$(MAKE) -C extraction clean
$(MAKE) -C runtime clean
$(MAKE) -C test/cminor clean
$(MAKE) -C test/c clean
distclean:
$(MAKE) clean
rm -rf cil
rm -f Makefile.config
include .depend
|
