aboutsummaryrefslogtreecommitdiffstats
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v7650logstatsplain
-rw-r--r--Allocproof.v25671logstatsplain
-rw-r--r--Alloctyping.v6085logstatsplain
-rw-r--r--Bounds.v11905logstatsplain
-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.v15820logstatsplain
-rw-r--r--CSEproof.v31148logstatsplain
-rw-r--r--Cminor.v40457logstatsplain
-rw-r--r--CminorSel.v13583logstatsplain
-rw-r--r--Coloring.v11924logstatsplain
-rw-r--r--Coloringaux.ml19928logstatsplain
-rw-r--r--Coloringaux.mli969logstatsplain
-rw-r--r--Coloringproof.v28489logstatsplain
-rw-r--r--InterfGraph.v9670logstatsplain
-rw-r--r--Kildall.v41057logstatsplain
-rw-r--r--LTL.v10021logstatsplain
-rw-r--r--LTLin.v9526logstatsplain
-rw-r--r--LTLintyping.v3813logstatsplain
-rw-r--r--LTLtyping.v4624logstatsplain
-rw-r--r--Linear.v13013logstatsplain
-rw-r--r--Linearize.v8088logstatsplain
-rw-r--r--Linearizeaux.ml4273logstatsplain
-rw-r--r--Linearizeproof.v23048logstatsplain
-rw-r--r--Linearizetyping.v3632logstatsplain
-rw-r--r--Lineartyping.v3859logstatsplain
-rw-r--r--Locations.v12936logstatsplain
-rw-r--r--Mach.v4684logstatsplain
-rw-r--r--Machabstr.v12202logstatsplain
-rw-r--r--Machabstr2concr.v31857logstatsplain
-rw-r--r--Machconcr.v10785logstatsplain
-rw-r--r--Machtyping.v9297logstatsplain
-rw-r--r--Parallelmove.v13137logstatsplain
-rw-r--r--RTL.v14967logstatsplain
-rw-r--r--RTLgen.v22091logstatsplain
-rw-r--r--RTLgenaux.ml2676logstatsplain
-rw-r--r--RTLgenproof.v42337logstatsplain
-rw-r--r--RTLgenspec.v40538logstatsplain
-rw-r--r--RTLtyping.v18370logstatsplain
-rw-r--r--RTLtypingaux.ml4943logstatsplain
-rw-r--r--Registers.v2018logstatsplain
-rw-r--r--Reload.v9311logstatsplain
-rw-r--r--Reloadproof.v47802logstatsplain
-rw-r--r--Reloadtyping.v11658logstatsplain
-rw-r--r--Stacking.v8771logstatsplain
-rw-r--r--Stackingproof.v55159logstatsplain
-rw-r--r--Stackingtyping.v8513logstatsplain
-rw-r--r--Tailcall.v4093logstatsplain
-rw-r--r--Tailcallproof.v26290logstatsplain
-rw-r--r--Tunneling.v4853logstatsplain
-rw-r--r--Tunnelingproof.v13196logstatsplain
-rw-r--r--Tunnelingtyping.v3409logstatsplain