index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
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--
Allnontrap.v
1536
log
stats
plain
-rw-r--r--
Allnontrapproof.v
7656
log
stats
plain
-rw-r--r--
Allocation.v
52816
log
stats
plain
-rw-r--r--
Allocationproof.v
101719
log
stats
plain
-rw-r--r--
Asmaux.v
1024
log
stats
plain
-rw-r--r--
Asmexpandaux.ml
6475
log
stats
plain
-rw-r--r--
Asmexpandaux.mli
1883
log
stats
plain
-rw-r--r--
Asmgenproof0.v
31206
log
stats
plain
-rw-r--r--
Bounds.v
15974
log
stats
plain
-rw-r--r--
CSE.v
22774
log
stats
plain
-rw-r--r--
CSE2.v
12388
log
stats
plain
-rw-r--r--
CSE2proof.v
49340
log
stats
plain
-rw-r--r--
CSE3.v
5252
log
stats
plain
-rw-r--r--
CSE3analysis.v
17406
log
stats
plain
-rw-r--r--
CSE3analysisaux.ml
11236
log
stats
plain
-rw-r--r--
CSE3analysisproof.v
42572
log
stats
plain
-rw-r--r--
CSE3proof.v
48468
log
stats
plain
-rw-r--r--
CSEdomain.v
6080
log
stats
plain
-rw-r--r--
CSEproof.v
51500
log
stats
plain
-rw-r--r--
CleanupLabels.v
2713
log
stats
plain
-rw-r--r--
CleanupLabelsproof.v
11977
log
stats
plain
-rw-r--r--
Cminor.v
46227
log
stats
plain
-rw-r--r--
CminorSel.v
20986
log
stats
plain
-rw-r--r--
Cminortyping.v
27922
log
stats
plain
-rw-r--r--
Constprop.v
9348
log
stats
plain
-rw-r--r--
Constpropproof.v
27144
log
stats
plain
-rw-r--r--
Conventions.v
8109
log
stats
plain
-rw-r--r--
Deadcode.v
8003
log
stats
plain
-rw-r--r--
Deadcodeproof.v
45696
log
stats
plain
-rw-r--r--
Debugvar.v
11897
log
stats
plain
-rw-r--r--
Debugvarproof.v
18804
log
stats
plain
-rw-r--r--
Duplicate.v
9275
log
stats
plain
-rw-r--r--
Duplicateaux.ml
42783
log
stats
plain
-rw-r--r--
Duplicatepasses.v
1798
log
stats
plain
-rw-r--r--
Duplicateproof.v
20296
log
stats
plain
-rw-r--r--
Fileinfo.ml
2755
log
stats
plain
-rw-r--r--
FirstNop.v
1357
log
stats
plain
-rw-r--r--
FirstNopproof.v
9482
log
stats
plain
-rw-r--r--
ForwardMoves.v
9238
log
stats
plain
-rw-r--r--
ForwardMovesproof.v
22655
log
stats
plain
-rw-r--r--
IRC.ml
30805
log
stats
plain
-rw-r--r--
IRC.mli
1710
log
stats
plain
-rw-r--r--
Inject.v
4953
log
stats
plain
-rw-r--r--
Injectproof.v
70613
log
stats
plain
-rw-r--r--
Inlining.v
17471
log
stats
plain
-rw-r--r--
Inliningaux.ml
3438
log
stats
plain
-rw-r--r--
Inliningproof.v
54196
log
stats
plain
-rw-r--r--
Inliningspec.v
27464
log
stats
plain
-rw-r--r--
Json.ml
3325
log
stats
plain
-rw-r--r--
JsonAST.ml
6808
log
stats
plain
-rw-r--r--
JsonAST.mli
1007
log
stats
plain
-rw-r--r--
Kildall.v
55460
log
stats
plain
-rw-r--r--
KillUselessMoves.v
1604
log
stats
plain
-rw-r--r--
KillUselessMovesproof.v
11077
log
stats
plain
-rw-r--r--
LICM.v
1057
log
stats
plain
-rw-r--r--
LICMaux.ml
11795
log
stats
plain
-rw-r--r--
LICMproof.v
1543
log
stats
plain
-rw-r--r--
LTL.v
13938
log
stats
plain
-rw-r--r--
LTLTunneling.v
6466
log
stats
plain
-rw-r--r--
LTLTunnelingaux.ml
3638
log
stats
plain
-rw-r--r--
LTLTunnelingproof.v
24781
log
stats
plain
-rw-r--r--
Linear.v
11567
log
stats
plain
-rw-r--r--
Linearize.v
8223
log
stats
plain
-rw-r--r--
Linearizeaux.ml
6525
log
stats
plain
-rw-r--r--
Linearizeproof.v
24463
log
stats
plain
-rw-r--r--
Lineartyping.v
14734
log
stats
plain
-rw-r--r--
Liveness.v
5511
log
stats
plain
-rw-r--r--
Locations.v
18105
log
stats
plain
-rw-r--r--
Mach.v
19954
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
47065
log
stats
plain
-rw-r--r--
OpHelpers.v
3177
log
stats
plain
-rw-r--r--
OpHelpersproof.v
5718
log
stats
plain
-rw-r--r--
PrintAsm.ml
7532
log
stats
plain
-rw-r--r--
PrintAsm.mli
943
log
stats
plain
-rw-r--r--
PrintAsmaux.ml
14302
log
stats
plain
-rw-r--r--
PrintCminor.ml
11742
log
stats
plain
-rw-r--r--
PrintLTL.ml
4653
log
stats
plain
-rw-r--r--
PrintMach.ml
3582
log
stats
plain
-rw-r--r--
PrintRTL.ml
4036
log
stats
plain
-rw-r--r--
PrintXTL.ml
5019
log
stats
plain
-rw-r--r--
Profiling.v
3281
log
stats
plain
-rw-r--r--
ProfilingExploit.v
1777
log
stats
plain
-rw-r--r--
ProfilingExploitproof.v
7775
log
stats
plain
-rw-r--r--
Profilingaux.ml
3005
log
stats
plain
-rw-r--r--
Profilingproof.v
23760
log
stats
plain
-rw-r--r--
RTL.v
23152
log
stats
plain
-rw-r--r--
RTLTunneling.v
4719
log
stats
plain
-rw-r--r--
RTLTunnelingaux.ml
3593
log
stats
plain
-rw-r--r--
RTLTunnelingproof.v
23880
log
stats
plain
-rw-r--r--
RTLcommonaux.ml
3344
log
stats
plain
-rw-r--r--
RTLgen.v
24658
log
stats
plain
-rw-r--r--
RTLgenaux.ml
3674
log
stats
plain
-rw-r--r--
RTLgenproof.v
53904
log
stats
plain
-rw-r--r--
RTLgenspec.v
47403
log
stats
plain
-rw-r--r--
RTLtyping.v
33217
log
stats
plain
-rw-r--r--
Regalloc.ml
42424
log
stats
plain
-rw-r--r--
Registers.v
3035
log
stats
plain
-rw-r--r--
Renumber.v
3177
log
stats
plain
-rw-r--r--
Renumberproof.v
10055
log
stats
plain
-rw-r--r--
SelectDiv.vp
11128
log
stats
plain
-rw-r--r--
SelectDivproof.v
39363
log
stats
plain
-rw-r--r--
Selection.v
20929
log
stats
plain
-rw-r--r--
Selectionaux.ml
4758
log
stats
plain
-rw-r--r--
Selectionproof.v
57606
log
stats
plain
-rw-r--r--
SplitLong.vp
10940
log
stats
plain
-rw-r--r--
SplitLongproof.v
43954
log
stats
plain
-rw-r--r--
Splitting.ml
5579
log
stats
plain
-rw-r--r--
Stacking.v
7482
log
stats
plain
-rw-r--r--
Stackingproof.v
82728
log
stats
plain
-rw-r--r--
Tailcall.v
3966
log
stats
plain
-rw-r--r--
Tailcallproof.v
23453
log
stats
plain
-rw-r--r--
Tunnelinglibs.ml
9420
log
stats
plain
-rw-r--r--
Unusedglob.v
5066
log
stats
plain
-rw-r--r--
Unusedglobproof.v
55157
log
stats
plain
-rw-r--r--
ValueAnalysis.v
73877
log
stats
plain
-rw-r--r--
ValueDomain.v
170939
log
stats
plain
-rw-r--r--
XTL.ml
7319
log
stats
plain
-rw-r--r--
XTL.mli
3038
log
stats
plain