aboutsummaryrefslogtreecommitdiffstats
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v48677logstatsplain
-rw-r--r--Allocproof.v90516logstatsplain
-rw-r--r--Asmexpandaux.ml2024logstatsplain
-rw-r--r--Asmgenproof0.v27182logstatsplain
-rw-r--r--Bounds.v12065logstatsplain
-rw-r--r--CMlexer.mli1106logstatsplain
-rw-r--r--CMlexer.mll5662logstatsplain
-rw-r--r--CMparser.mly25656logstatsplain
-rw-r--r--CMtypecheck.ml10829logstatsplain
-rw-r--r--CMtypecheck.mli1116logstatsplain
-rw-r--r--CSE.v22502logstatsplain
-rw-r--r--CSEdomain.v5628logstatsplain
-rw-r--r--CSEproof.v45007logstatsplain
-rw-r--r--CleanupLabels.v2742logstatsplain
-rw-r--r--CleanupLabelsproof.v11887logstatsplain
-rw-r--r--Cminor.v43686logstatsplain
-rw-r--r--CminorSel.v20723logstatsplain
-rw-r--r--Constprop.v8475logstatsplain
-rw-r--r--Constpropproof.v24111logstatsplain
-rw-r--r--Conventions.v3646logstatsplain
-rw-r--r--Deadcode.v8014logstatsplain
-rw-r--r--Deadcodeproof.v41995logstatsplain
-rw-r--r--Debugvar.v12025logstatsplain
-rw-r--r--Debugvarproof.v18816logstatsplain
-rw-r--r--IRC.ml30902logstatsplain
-rw-r--r--IRC.mli1770logstatsplain
-rw-r--r--Inlining.v17200logstatsplain
-rw-r--r--Inliningaux.ml974logstatsplain
-rw-r--r--Inliningproof.v51775logstatsplain
-rw-r--r--Inliningspec.v27229logstatsplain
-rw-r--r--Kildall.v55692logstatsplain
-rw-r--r--LTL.v12676logstatsplain
-rw-r--r--Linear.v10836logstatsplain
-rw-r--r--Linearize.v8369logstatsplain
-rw-r--r--Linearizeaux.ml4022logstatsplain
-rw-r--r--Linearizeproof.v24467logstatsplain
-rw-r--r--Lineartyping.v11797logstatsplain
-rw-r--r--Liveness.v5514logstatsplain
-rw-r--r--Locations.v17341logstatsplain
-rw-r--r--Mach.v16321logstatsplain
-rw-r--r--NeedDomain.v45718logstatsplain
-rw-r--r--PrintAsm.ml5299logstatsplain
-rw-r--r--PrintAsm.mli973logstatsplain
-rw-r--r--PrintAsmaux.ml11196logstatsplain
-rw-r--r--PrintCminor.ml11653logstatsplain
-rw-r--r--PrintLTL.ml4448logstatsplain
-rw-r--r--PrintLTLin.ml3746logstatsplain
-rw-r--r--PrintMach.ml3595logstatsplain
-rw-r--r--PrintRTL.ml3915logstatsplain
-rw-r--r--PrintXTL.ml4962logstatsplain
-rw-r--r--RTL.v22427logstatsplain
-rw-r--r--RTLgen.v24658logstatsplain
-rw-r--r--RTLgenaux.ml3691logstatsplain
-rw-r--r--RTLgenproof.v53147logstatsplain
-rw-r--r--RTLgenspec.v47287logstatsplain
-rw-r--r--RTLtyping.v32755logstatsplain
-rw-r--r--Regalloc.ml39466logstatsplain
-rw-r--r--Registers.v3001logstatsplain
-rw-r--r--Renumber.v3159logstatsplain
-rw-r--r--Renumberproof.v9400logstatsplain
-rw-r--r--SelectDiv.vp6376logstatsplain
-rw-r--r--SelectDivproof.v22260logstatsplain
-rw-r--r--SelectLong.vp14082logstatsplain
-rw-r--r--SelectLongproof.v46945logstatsplain
-rw-r--r--Selection.v12565logstatsplain
-rw-r--r--Selectionproof.v36184logstatsplain
-rw-r--r--Splitting.ml5588logstatsplain
-rw-r--r--Stacking.v9401logstatsplain
-rw-r--r--Stackingproof.v105870logstatsplain
-rw-r--r--Tailcall.v4129logstatsplain
-rw-r--r--Tailcallproof.v22444logstatsplain
-rw-r--r--Tunneling.v4017logstatsplain
-rw-r--r--Tunnelingproof.v14547logstatsplain
-rw-r--r--Unusedglob.v4800logstatsplain
-rw-r--r--Unusedglobproof.v52507logstatsplain
-rw-r--r--ValueAnalysis.v69477logstatsplain
-rw-r--r--ValueDomain.v137230logstatsplain
-rw-r--r--XTL.ml7054logstatsplain
-rw-r--r--XTL.mli2966logstatsplain