aboutsummaryrefslogtreecommitdiffstats
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v7769logstatsplain
-rw-r--r--Allocproof.v25812logstatsplain
-rw-r--r--Alloctyping.v6110logstatsplain
-rw-r--r--Bounds.v11935logstatsplain
-rw-r--r--CMlexer.mli1106logstatsplain
-rw-r--r--CMlexer.mll4272logstatsplain
-rw-r--r--CMparser.mly16970logstatsplain
-rw-r--r--CMtypecheck.ml10479logstatsplain
-rw-r--r--CMtypecheck.mli1116logstatsplain
-rw-r--r--CSE.v15874logstatsplain
-rw-r--r--CSEproof.v31083logstatsplain
-rw-r--r--Cminor.v40858logstatsplain
-rw-r--r--CminorSel.v17430logstatsplain
-rw-r--r--Coloring.v11924logstatsplain
-rw-r--r--Coloringaux.ml21867logstatsplain
-rw-r--r--Coloringaux.mli969logstatsplain
-rw-r--r--Coloringproof.v28489logstatsplain
-rw-r--r--Constprop.v7837logstatsplain
-rw-r--r--Constpropproof.v16002logstatsplain
-rw-r--r--InterfGraph.v9670logstatsplain
-rw-r--r--Kildall.v41057logstatsplain
-rw-r--r--LTL.v10464logstatsplain
-rw-r--r--LTLin.v9967logstatsplain
-rw-r--r--LTLintyping.v4045logstatsplain
-rw-r--r--LTLtyping.v4913logstatsplain
-rw-r--r--Linear.v13463logstatsplain
-rw-r--r--Linearize.v8148logstatsplain
-rw-r--r--Linearizeaux.ml4368logstatsplain
-rw-r--r--Linearizeproof.v23643logstatsplain
-rw-r--r--Linearizetyping.v3679logstatsplain
-rw-r--r--Lineartyping.v4064logstatsplain
-rw-r--r--Locations.v12936logstatsplain
-rw-r--r--Mach.v4742logstatsplain
-rw-r--r--Machabstr.v12593logstatsplain
-rw-r--r--Machabstr2concr.v38710logstatsplain
-rw-r--r--Machconcr.v11262logstatsplain
-rw-r--r--Machtyping.v9370logstatsplain
-rw-r--r--Parallelmove.v13137logstatsplain
-rw-r--r--RTL.v15165logstatsplain
-rw-r--r--RTLgen.v22721logstatsplain
-rw-r--r--RTLgenaux.ml4174logstatsplain
-rw-r--r--RTLgenproof.v44103logstatsplain
-rw-r--r--RTLgenspec.v42140logstatsplain
-rw-r--r--RTLtyping.v18770logstatsplain
-rw-r--r--RTLtypingaux.ml5006logstatsplain
-rw-r--r--Registers.v2018logstatsplain
-rw-r--r--Reload.v9429logstatsplain
-rw-r--r--Reloadproof.v48155logstatsplain
-rw-r--r--Reloadtyping.v11771logstatsplain
-rw-r--r--Selection.v7332logstatsplain
-rw-r--r--Selectionproof.v15629logstatsplain
-rw-r--r--Stacking.v8827logstatsplain
-rw-r--r--Stackingproof.v55885logstatsplain
-rw-r--r--Stackingtyping.v8582logstatsplain
-rw-r--r--Tailcall.v4093logstatsplain
-rw-r--r--Tailcallproof.v22221logstatsplain
-rw-r--r--Tunneling.v4927logstatsplain
-rw-r--r--Tunnelingproof.v13405logstatsplain
-rw-r--r--Tunnelingtyping.v3561logstatsplain