aboutsummaryrefslogtreecommitdiffstats
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v52560logstatsplain
-rw-r--r--Allocproof.v99605logstatsplain
-rw-r--r--Asmexpandaux.ml5475logstatsplain
-rw-r--r--Asmexpandaux.mli1873logstatsplain
-rw-r--r--Asmgenproof0.v27921logstatsplain
-rw-r--r--Bounds.v15923logstatsplain
-rw-r--r--CSE.v22376logstatsplain
-rw-r--r--CSEdomain.v5626logstatsplain
-rw-r--r--CSEproof.v45433logstatsplain
-rw-r--r--CleanupLabels.v2713logstatsplain
-rw-r--r--CleanupLabelsproof.v11447logstatsplain
-rw-r--r--Cminor.v43627logstatsplain
-rw-r--r--CminorSel.v20949logstatsplain
-rw-r--r--Constprop.v8039logstatsplain
-rw-r--r--Constpropproof.v23552logstatsplain
-rw-r--r--Conventions.v4260logstatsplain
-rw-r--r--Deadcode.v7875logstatsplain
-rw-r--r--Deadcodeproof.v42675logstatsplain
-rw-r--r--Debugvar.v11890logstatsplain
-rw-r--r--Debugvarproof.v18334logstatsplain
-rw-r--r--Fileinfo.ml2755logstatsplain
-rw-r--r--IRC.ml30945logstatsplain
-rw-r--r--IRC.mli1873logstatsplain
-rw-r--r--Inlining.v17162logstatsplain
-rw-r--r--Inliningaux.ml987logstatsplain
-rw-r--r--Inliningproof.v52044logstatsplain
-rw-r--r--Inliningspec.v27433logstatsplain
-rw-r--r--Kildall.v55463logstatsplain
-rw-r--r--LTL.v12517logstatsplain
-rw-r--r--Linear.v10723logstatsplain
-rw-r--r--Linearize.v8211logstatsplain
-rw-r--r--Linearizeaux.ml3980logstatsplain
-rw-r--r--Linearizeproof.v24033logstatsplain
-rw-r--r--Lineartyping.v11966logstatsplain
-rw-r--r--Liveness.v5504logstatsplain
-rw-r--r--Locations.v18142logstatsplain
-rw-r--r--Mach.v19126logstatsplain
-rw-r--r--NeedDomain.v45880logstatsplain
-rw-r--r--PrintAsm.ml5264logstatsplain
-rw-r--r--PrintAsm.mli943logstatsplain
-rw-r--r--PrintAsmaux.ml9606logstatsplain
-rw-r--r--PrintCminor.ml11640logstatsplain
-rw-r--r--PrintLTL.ml4469logstatsplain
-rw-r--r--PrintLTLin.ml3746logstatsplain
-rw-r--r--PrintMach.ml3543logstatsplain
-rw-r--r--PrintRTL.ml3887logstatsplain
-rw-r--r--PrintXTL.ml4985logstatsplain
-rw-r--r--RTL.v22283logstatsplain
-rw-r--r--RTLgen.v24631logstatsplain
-rw-r--r--RTLgenaux.ml3664logstatsplain
-rw-r--r--RTLgenproof.v53910logstatsplain
-rw-r--r--RTLgenspec.v47185logstatsplain
-rw-r--r--RTLtyping.v32633logstatsplain
-rw-r--r--Regalloc.ml42305logstatsplain
-rw-r--r--Registers.v3035logstatsplain
-rw-r--r--Renumber.v3157logstatsplain
-rw-r--r--Renumberproof.v9192logstatsplain
-rw-r--r--SelectDiv.vp11076logstatsplain
-rw-r--r--SelectDivproof.v39397logstatsplain
-rw-r--r--Selection.v15033logstatsplain
-rw-r--r--Selectionproof.v42515logstatsplain
-rw-r--r--SplitLong.vp12645logstatsplain
-rw-r--r--SplitLongproof.v46235logstatsplain
-rw-r--r--Splitting.ml5561logstatsplain
-rw-r--r--Stacking.v7472logstatsplain
-rw-r--r--Stackingproof.v80980logstatsplain
-rw-r--r--Tailcall.v3966logstatsplain
-rw-r--r--Tailcallproof.v22208logstatsplain
-rw-r--r--Tunneling.v4076logstatsplain
-rw-r--r--Tunnelingproof.v20674logstatsplain
-rw-r--r--Unusedglob.v5064logstatsplain
-rw-r--r--Unusedglobproof.v53382logstatsplain
-rw-r--r--ValueAnalysis.v71544logstatsplain
-rw-r--r--ValueDomain.v154377logstatsplain
-rw-r--r--XTL.ml7277logstatsplain
-rw-r--r--XTL.mli3008logstatsplain