blob: 69b5f572e853f4b03a8b6fd8cf64e9ca74d7011e (
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
|
FILES=\
Datatypes.ml Logic.ml Wf.ml Peano.ml Specif.ml Compare_dec.ml \
Bool.ml CList.ml Sumbool.ml Setoid.ml BinPos.ml BinNat.ml BinInt.ml \
ZArith_dec.ml Zeven.ml Zmax.ml Zmisc.ml Zbool.ml Zpower.ml Zdiv.ml \
OrderedType.ml FSetInterface.ml FSetFacts.ml FSetList.ml \
CInt.ml FSetAVL.ml \
Coqlib.ml Maps.ml Ordered.ml AST.ml Iteration.ml Integers.ml \
../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Parmov.ml Values.ml \
Mem.ml Globalenvs.ml \
Csyntax.ml Ctyping.ml Csharpminor.ml Cshmgen.ml \
Op.ml Cminor.ml Cmconstr.ml \
Cminorgen.ml \
Registers.ml RTL.ml \
../caml/RTLgenaux.ml RTLgen.ml \
Locations.ml Conventions.ml \
../caml/RTLtypingaux.ml RTLtyping.ml \
Lattice.ml Kildall.ml \
Constprop.ml CSE.ml \
LTL.ml \
InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \
Parallelmove.ml Allocation.ml \
Tunneling.ml Linear.ml Lineartyping.ml Linearize.ml \
Mach.ml Stacking.ml \
PPC.ml PPCgen.ml \
Main.ml \
../caml/Cil2Csyntax.ml \
../caml/CMparser.ml ../caml/CMlexer.ml ../caml/CMtypecheck.ml \
../caml/PrintCsyntax.ml ../caml/PrintPPC.ml \
../caml/Main2.ml
EXTRACTEDFILES:=$(filter-out ../caml/%, $(FILES))
GENFILES:=$(EXTRACTEDFILES) $(EXTRACTEDFILES:.ml=.mli)
CAMLINCL=-I ../caml -I ../cil/obj/x86_LINUX -I ../cil/obj/ppc_DARWIN
OCAMLC=ocamlc -g $(CAMLINCL)
OCAMLOPT=ocamlopt $(CAMLINCL)
OCAMLDEP=ocamldep $(CAMLINCL)
OCAMLLIBS=unix.cma str.cma cil.cma
COQINCL=-I ../lib -I ../common -I ../backend -I ../cfrontend
COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source
executables: ../ccomp ../ccomp.byt
../ccomp.byt: $(FILES:.ml=.cmo)
$(OCAMLC) -o ../ccomp.byt $(OCAMLLIBS) $(FILES:.ml=.cmo)
clean::
rm -f ../ccomp
../ccomp: $(FILES:.ml=.cmx)
$(OCAMLOPT) -o ../ccomp $(OCAMLLIBS:.cma=.cmxa) $(FILES:.ml=.cmx)
clean::
rm -f ../ccomp.opt
extraction:
@rm -f $(GENFILES)
$(COQEXEC) extraction.v
@echo "Fixing file names..."
@mv list.ml CList.ml
@mv list.mli CList.mli
@mv int.ml CInt.ml
@mv int.mli CInt.mli
@for i in $(GENFILES); do \
j=`./uncapitalize $$i`; \
test -f $$i || (test -f $$j && mv $$j $$i); \
done
@echo "Conversion List -> CList and Int -> CInt..."
@./convert $(GENFILES)
@echo "Patching files..."
@for i in *.patch; do patch < $$i; done
../caml/CMparser.ml ../caml/CMparser.mli: ../caml/CMparser.mly
ocamlyacc -v ../caml/CMparser.mly
beforedepend:: ../caml/CMparser.ml ../caml/CMparser.mli
clean::
rm -f ../caml/CMparser.ml ../caml/CMparser.mli ../caml/CMparser.output
../caml/CMlexer.ml: ../caml/CMlexer.mll
ocamllex ../caml/CMlexer.mll
beforedepend:: ../caml/CMlexer.ml
clean::
rm -f ../caml/CMlexer.ml
.SUFFIXES: .ml .mli .cmo .cmi .cmx
.mli.cmi:
$(OCAMLC) -c $*.mli
.ml.cmo:
$(OCAMLC) -c $*.ml
.ml.cmx:
$(OCAMLOPT) -c $*.ml
clean::
rm -f $(GENFILES)
rm -f *.cm? *.o
cd ../caml && rm -f *.cm? *.o
depend: beforedepend
$(OCAMLDEP) ../caml/*.mli ../caml/*.ml *.mli *.ml > .depend
include .depend
|
