index
:
compcert
FPcomp
aarch64
conditional-move
dev/michalis
floatofintu
inl-cse-const
master
no-pervasives
CompCert fork with minor modifications for Vericert.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
backend
Mode
Name
Size
-rw-r--r--
Allocation.v
48630
log
stats
plain
-rw-r--r--
Allocproof.v
90133
log
stats
plain
-rw-r--r--
Asmexpandaux.ml
5234
log
stats
plain
-rw-r--r--
Asmgenproof0.v
27118
log
stats
plain
-rw-r--r--
Bounds.v
12047
log
stats
plain
-rw-r--r--
CMlexer.mli
1106
log
stats
plain
-rw-r--r--
CMlexer.mll
5659
log
stats
plain
-rw-r--r--
CMparser.mly
25706
log
stats
plain
-rw-r--r--
CMtypecheck.ml
10828
log
stats
plain
-rw-r--r--
CMtypecheck.mli
1116
log
stats
plain
-rw-r--r--
CSE.v
22493
log
stats
plain
-rw-r--r--
CSEdomain.v
5626
log
stats
plain
-rw-r--r--
CSEproof.v
44865
log
stats
plain
-rw-r--r--
CleanupLabels.v
2738
log
stats
plain
-rw-r--r--
CleanupLabelsproof.v
11852
log
stats
plain
-rw-r--r--
Cminor.v
43625
log
stats
plain
-rw-r--r--
CminorSel.v
20704
log
stats
plain
-rw-r--r--
Constprop.v
8477
log
stats
plain
-rw-r--r--
Constpropproof.v
24241
log
stats
plain
-rw-r--r--
Conventions.v
3637
log
stats
plain
-rw-r--r--
Deadcode.v
8012
log
stats
plain
-rw-r--r--
Deadcodeproof.v
41802
log
stats
plain
-rw-r--r--
Debugvar.v
12020
log
stats
plain
-rw-r--r--
Debugvarproof.v
18752
log
stats
plain
-rw-r--r--
Fileinfo.ml
2755
log
stats
plain
-rw-r--r--
IRC.ml
30891
log
stats
plain
-rw-r--r--
IRC.mli
1770
log
stats
plain
-rw-r--r--
Inlining.v
17179
log
stats
plain
-rw-r--r--
Inliningaux.ml
974
log
stats
plain
-rw-r--r--
Inliningproof.v
51560
log
stats
plain
-rw-r--r--
Inliningspec.v
27140
log
stats
plain
-rw-r--r--
Kildall.v
55525
log
stats
plain
-rw-r--r--
LTL.v
12672
log
stats
plain
-rw-r--r--
Linear.v
10836
log
stats
plain
-rw-r--r--
Linearize.v
8364
log
stats
plain
-rw-r--r--
Linearizeaux.ml
4020
log
stats
plain
-rw-r--r--
Linearizeproof.v
24398
log
stats
plain
-rw-r--r--
Lineartyping.v
11762
log
stats
plain
-rw-r--r--
Liveness.v
5504
log
stats
plain
-rw-r--r--
Locations.v
17279
log
stats
plain
-rw-r--r--
Mach.v
16314
log
stats
plain
-rw-r--r--
NeedDomain.v
45524
log
stats
plain
-rw-r--r--
PrintAsm.ml
5279
log
stats
plain
-rw-r--r--
PrintAsm.mli
973
log
stats
plain
-rw-r--r--
PrintAsmaux.ml
9363
log
stats
plain
-rw-r--r--
PrintCminor.ml
11647
log
stats
plain
-rw-r--r--
PrintLTL.ml
4448
log
stats
plain
-rw-r--r--
PrintLTLin.ml
3746
log
stats
plain
-rw-r--r--
PrintMach.ml
3595
log
stats
plain
-rw-r--r--
PrintRTL.ml
3914
log
stats
plain
-rw-r--r--
PrintXTL.ml
4943
log
stats
plain
-rw-r--r--
RTL.v
22402
log
stats
plain
-rw-r--r--
RTLgen.v
24652
log
stats
plain
-rw-r--r--
RTLgenaux.ml
3689
log
stats
plain
-rw-r--r--
RTLgenproof.v
53028
log
stats
plain
-rw-r--r--
RTLgenspec.v
47185
log
stats
plain
-rw-r--r--
RTLtyping.v
32672
log
stats
plain
-rw-r--r--
Regalloc.ml
39405
log
stats
plain
-rw-r--r--
Registers.v
3000
log
stats
plain
-rw-r--r--
Renumber.v
3157
log
stats
plain
-rw-r--r--
Renumberproof.v
9364
log
stats
plain
-rw-r--r--
SelectDiv.vp
6376
log
stats
plain
-rw-r--r--
SelectDivproof.v
22162
log
stats
plain
-rw-r--r--
SelectLong.vp
13086
log
stats
plain
-rw-r--r--
SelectLongproof.v
47802
log
stats
plain
-rw-r--r--
Selection.v
15247
log
stats
plain
-rw-r--r--
Selectionproof.v
38424
log
stats
plain
-rw-r--r--
Splitting.ml
5585
log
stats
plain
-rw-r--r--
Stacking.v
9396
log
stats
plain
-rw-r--r--
Stackingproof.v
105541
log
stats
plain
-rw-r--r--
Tailcall.v
4127
log
stats
plain
-rw-r--r--
Tailcallproof.v
22379
log
stats
plain
-rw-r--r--
Tunneling.v
4016
log
stats
plain
-rw-r--r--
Tunnelingproof.v
14513
log
stats
plain
-rw-r--r--
Unusedglob.v
4800
log
stats
plain
-rw-r--r--
Unusedglobproof.v
52299
log
stats
plain
-rw-r--r--
ValueAnalysis.v
69158
log
stats
plain
-rw-r--r--
ValueDomain.v
136835
log
stats
plain
-rw-r--r--
XTL.ml
7053
log
stats
plain
-rw-r--r--
XTL.mli
2966
log
stats
plain