summaryrefslogtreecommitdiff
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v7650logplain
-rw-r--r--Allocproof.v25671logplain
-rw-r--r--Alloctyping.v6085logplain
-rw-r--r--Bounds.v11905logplain
-rw-r--r--CMlexer.mli1106logplain
-rw-r--r--CMlexer.mll4272logplain
-rw-r--r--CMparser.mly16970logplain
-rw-r--r--CMtypecheck.ml10479logplain
-rw-r--r--CMtypecheck.mli1116logplain
-rw-r--r--CSE.v15820logplain
-rw-r--r--CSEproof.v31148logplain
-rw-r--r--Cminor.v40457logplain
-rw-r--r--CminorSel.v17236logplain
-rw-r--r--Coloring.v11924logplain
-rw-r--r--Coloringaux.ml19928logplain
-rw-r--r--Coloringaux.mli969logplain
-rw-r--r--Coloringproof.v28489logplain
-rw-r--r--Constprop.v7876logplain
-rw-r--r--Constpropproof.v15517logplain
-rw-r--r--InterfGraph.v9670logplain
-rw-r--r--Kildall.v41057logplain
-rw-r--r--LTL.v10021logplain
-rw-r--r--LTLin.v9526logplain
-rw-r--r--LTLintyping.v3813logplain
-rw-r--r--LTLtyping.v4624logplain
-rw-r--r--Linear.v13013logplain
-rw-r--r--Linearize.v8088logplain
-rw-r--r--Linearizeaux.ml4273logplain
-rw-r--r--Linearizeproof.v23048logplain
-rw-r--r--Linearizetyping.v3632logplain
-rw-r--r--Lineartyping.v3859logplain
-rw-r--r--Locations.v12936logplain
-rw-r--r--Mach.v4684logplain
-rw-r--r--Machabstr.v12202logplain
-rw-r--r--Machabstr2concr.v31857logplain
-rw-r--r--Machconcr.v10785logplain
-rw-r--r--Machtyping.v9297logplain
-rw-r--r--Parallelmove.v13137logplain
-rw-r--r--RTL.v14967logplain
-rw-r--r--RTLgen.v22091logplain
-rw-r--r--RTLgenaux.ml2676logplain
-rw-r--r--RTLgenproof.v42337logplain
-rw-r--r--RTLgenspec.v40538logplain
-rw-r--r--RTLtyping.v18370logplain
-rw-r--r--RTLtypingaux.ml4943logplain
-rw-r--r--Registers.v2018logplain
-rw-r--r--Reload.v9311logplain
-rw-r--r--Reloadproof.v47802logplain
-rw-r--r--Reloadtyping.v11658logplain
-rw-r--r--Stacking.v8771logplain
-rw-r--r--Stackingproof.v55159logplain
-rw-r--r--Stackingtyping.v8513logplain
-rw-r--r--Tailcall.v4093logplain
-rw-r--r--Tailcallproof.v26290logplain
-rw-r--r--Tunneling.v4853logplain
-rw-r--r--Tunnelingproof.v13196logplain
-rw-r--r--Tunnelingtyping.v3409logplain