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--
AisAnnot.ml
7007
log
stats
plain
-rw-r--r--
AisAnnot.mli
2360
log
stats
plain
-rw-r--r--
Allocation.v
52534
log
stats
plain
-rw-r--r--
Allocproof.v
99231
log
stats
plain
-rw-r--r--
Asmexpandaux.ml
6418
log
stats
plain
-rw-r--r--
Asmexpandaux.mli
1883
log
stats
plain
-rw-r--r--
Asmgenproof0.v
31208
log
stats
plain
-rw-r--r--
Bounds.v
15967
log
stats
plain
-rw-r--r--
CSE.v
22669
log
stats
plain
-rw-r--r--
CSEdomain.v
5626
log
stats
plain
-rw-r--r--
CSEproof.v
45591
log
stats
plain
-rw-r--r--
CleanupLabels.v
2713
log
stats
plain
-rw-r--r--
CleanupLabelsproof.v
11447
log
stats
plain
-rw-r--r--
Cminor.v
46028
log
stats
plain
-rw-r--r--
CminorSel.v
20949
log
stats
plain
-rw-r--r--
Cminortyping.v
27849
log
stats
plain
-rw-r--r--
Constprop.v
9332
log
stats
plain
-rw-r--r--
Constpropproof.v
24600
log
stats
plain
-rw-r--r--
Conventions.v
8113
log
stats
plain
-rw-r--r--
Deadcode.v
7989
log
stats
plain
-rw-r--r--
Deadcodeproof.v
42917
log
stats
plain
-rw-r--r--
Debugvar.v
11892
log
stats
plain
-rw-r--r--
Debugvarproof.v
18316
log
stats
plain
-rw-r--r--
Fileinfo.ml
2755
log
stats
plain
-rw-r--r--
IRC.ml
30933
log
stats
plain
-rw-r--r--
IRC.mli
1744
log
stats
plain
-rw-r--r--
Inlining.v
17397
log
stats
plain
-rw-r--r--
Inliningaux.ml
3295
log
stats
plain
-rw-r--r--
Inliningproof.v
52144
log
stats
plain
-rw-r--r--
Inliningspec.v
27473
log
stats
plain
-rw-r--r--
Json.ml
3325
log
stats
plain
-rw-r--r--
JsonAST.ml
6420
log
stats
plain
-rw-r--r--
JsonAST.mli
1007
log
stats
plain
-rw-r--r--
Kildall.v
55460
log
stats
plain
-rw-r--r--
LTL.v
13138
log
stats
plain
-rw-r--r--
Linear.v
10748
log
stats
plain
-rw-r--r--
Linearize.v
8211
log
stats
plain
-rw-r--r--
Linearizeaux.ml
3969
log
stats
plain
-rw-r--r--
Linearizeproof.v
24033
log
stats
plain
-rw-r--r--
Lineartyping.v
14331
log
stats
plain
-rw-r--r--
Liveness.v
5504
log
stats
plain
-rw-r--r--
Locations.v
18127
log
stats
plain
-rw-r--r--
Mach.v
19265
log
stats
plain
-rw-r--r--
Machregsnames.ml
1192
log
stats
plain
-rw-r--r--
Machregsnames.mli
970
log
stats
plain
-rw-r--r--
NeedDomain.v
47130
log
stats
plain
-rw-r--r--
PrintAsm.ml
7481
log
stats
plain
-rw-r--r--
PrintAsm.mli
943
log
stats
plain
-rw-r--r--
PrintAsmaux.ml
10495
log
stats
plain
-rw-r--r--
PrintCminor.ml
11599
log
stats
plain
-rw-r--r--
PrintLTL.ml
4460
log
stats
plain
-rw-r--r--
PrintMach.ml
3540
log
stats
plain
-rw-r--r--
PrintRTL.ml
3876
log
stats
plain
-rw-r--r--
PrintXTL.ml
4976
log
stats
plain
-rw-r--r--
RTL.v
22366
log
stats
plain
-rw-r--r--
RTLgen.v
24635
log
stats
plain
-rw-r--r--
RTLgenaux.ml
3664
log
stats
plain
-rw-r--r--
RTLgenproof.v
53883
log
stats
plain
-rw-r--r--
RTLgenspec.v
47208
log
stats
plain
-rw-r--r--
RTLtyping.v
32745
log
stats
plain
-rw-r--r--
Regalloc.ml
42304
log
stats
plain
-rw-r--r--
Registers.v
3035
log
stats
plain
-rw-r--r--
Renumber.v
3157
log
stats
plain
-rw-r--r--
Renumberproof.v
9192
log
stats
plain
-rw-r--r--
SelectDiv.vp
11076
log
stats
plain
-rw-r--r--
SelectDivproof.v
39440
log
stats
plain
-rw-r--r--
Selection.v
19540
log
stats
plain
-rw-r--r--
Selectionaux.ml
4683
log
stats
plain
-rw-r--r--
Selectionproof.v
57361
log
stats
plain
-rw-r--r--
SplitLong.vp
12596
log
stats
plain
-rw-r--r--
SplitLongproof.v
45050
log
stats
plain
-rw-r--r--
Splitting.ml
5561
log
stats
plain
-rw-r--r--
Stacking.v
7472
log
stats
plain
-rw-r--r--
Stackingproof.v
80629
log
stats
plain
-rw-r--r--
Tailcall.v
3966
log
stats
plain
-rw-r--r--
Tailcallproof.v
22161
log
stats
plain
-rw-r--r--
Tunneling.v
4076
log
stats
plain
-rw-r--r--
Tunnelingproof.v
21045
log
stats
plain
-rw-r--r--
Unusedglob.v
5065
log
stats
plain
-rw-r--r--
Unusedglobproof.v
53434
log
stats
plain
-rw-r--r--
ValueAnalysis.v
73287
log
stats
plain
-rw-r--r--
ValueDomain.v
158071
log
stats
plain
-rw-r--r--
XTL.ml
7277
log
stats
plain
-rw-r--r--
XTL.mli
3008
log
stats
plain