aboutsummaryrefslogtreecommitdiffstats
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v7946logstatsplain
-rw-r--r--Allocproof.v27197logstatsplain
-rw-r--r--Alloctyping.v6132logstatsplain
-rw-r--r--Bounds.v12025logstatsplain
-rw-r--r--CMlexer.mli1106logstatsplain
-rw-r--r--CMlexer.mll4272logstatsplain
-rw-r--r--CMparser.mly17042logstatsplain
-rw-r--r--CMtypecheck.ml10479logstatsplain
-rw-r--r--CMtypecheck.mli1116logstatsplain
-rw-r--r--CSE.v15791logstatsplain
-rw-r--r--CSEproof.v31596logstatsplain
-rw-r--r--CastOptim.v9111logstatsplain
-rw-r--r--CastOptimproof.v20032logstatsplain
-rw-r--r--Cminor.v41205logstatsplain
-rw-r--r--CminorSel.v17750logstatsplain
-rw-r--r--Coloring.v12009logstatsplain
-rw-r--r--Coloringaux.ml28024logstatsplain
-rw-r--r--Coloringaux.mli1017logstatsplain
-rw-r--r--Coloringproof.v28535logstatsplain
-rw-r--r--Constprop.v7906logstatsplain
-rw-r--r--Constpropproof.v16691logstatsplain
-rw-r--r--Conventions.v7902logstatsplain
-rw-r--r--InterfGraph.v9904logstatsplain
-rw-r--r--Kildall.v41057logstatsplain
-rw-r--r--LTL.v11024logstatsplain
-rw-r--r--LTLin.v10346logstatsplain
-rw-r--r--LTLintyping.v4321logstatsplain
-rw-r--r--LTLtyping.v5219logstatsplain
-rw-r--r--Linear.v14126logstatsplain
-rw-r--r--Linearize.v8227logstatsplain
-rw-r--r--Linearizeaux.ml4436logstatsplain
-rw-r--r--Linearizeproof.v24511logstatsplain
-rw-r--r--Linearizetyping.v3747logstatsplain
-rw-r--r--Lineartyping.v4301logstatsplain
-rw-r--r--Locations.v14264logstatsplain
-rw-r--r--Mach.v5216logstatsplain
-rw-r--r--Machabstr.v12909logstatsplain
-rw-r--r--Machabstr2concr.v39949logstatsplain
-rw-r--r--Machconcr.v11569logstatsplain
-rw-r--r--Machtyping.v10642logstatsplain
-rw-r--r--Parallelmove.v13137logstatsplain
-rw-r--r--PrintCminor.ml8639logstatsplain
-rw-r--r--PrintLTL.ml3973logstatsplain
-rw-r--r--PrintLTLin.ml4148logstatsplain
-rw-r--r--PrintRTL.ml5055logstatsplain
-rw-r--r--RTL.v15749logstatsplain
-rw-r--r--RTLgen.v23655logstatsplain
-rw-r--r--RTLgenaux.ml4174logstatsplain
-rw-r--r--RTLgenproof.v44411logstatsplain
-rw-r--r--RTLgenspec.v46691logstatsplain
-rw-r--r--RTLtyping.v19463logstatsplain
-rw-r--r--RTLtypingaux.ml5621logstatsplain
-rw-r--r--Registers.v2018logstatsplain
-rw-r--r--Reload.v9618logstatsplain
-rw-r--r--Reloadproof.v50278logstatsplain
-rw-r--r--Reloadtyping.v12003logstatsplain
-rw-r--r--Selection.v8250logstatsplain
-rw-r--r--Selectionproof.v18349logstatsplain
-rw-r--r--Stacking.v8782logstatsplain
-rw-r--r--Stackingproof.v58837logstatsplain
-rw-r--r--Stackingtyping.v8655logstatsplain
-rw-r--r--Tailcall.v4088logstatsplain
-rw-r--r--Tailcallproof.v22929logstatsplain
-rw-r--r--Tunneling.v4998logstatsplain
-rw-r--r--Tunnelingproof.v13986logstatsplain
-rw-r--r--Tunnelingtyping.v3561logstatsplain