aboutsummaryrefslogtreecommitdiffstats
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v4498logstatsplain
-rw-r--r--Allocproof.v26687logstatsplain
-rw-r--r--Alloctyping.v6157logstatsplain
-rw-r--r--Asmgenproof0.v25486logstatsplain
-rw-r--r--Bounds.v12845logstatsplain
-rw-r--r--CMlexer.mli1106logstatsplain
-rw-r--r--CMlexer.mll4567logstatsplain
-rw-r--r--CMparser.mly21325logstatsplain
-rw-r--r--CMtypecheck.ml10555logstatsplain
-rw-r--r--CMtypecheck.mli1116logstatsplain
-rw-r--r--CSE.v20005logstatsplain
-rw-r--r--CSEproof.v41268logstatsplain
-rw-r--r--CleanupLabels.v2759logstatsplain
-rw-r--r--CleanupLabelsproof.v11063logstatsplain
-rw-r--r--CleanupLabelstyping.v2016logstatsplain
-rw-r--r--Cminor.v38885logstatsplain
-rw-r--r--CminorSel.v16540logstatsplain
-rw-r--r--Coloring.v12276logstatsplain
-rw-r--r--Coloringaux.ml28871logstatsplain
-rw-r--r--Coloringaux.mli1017logstatsplain
-rw-r--r--Coloringproof.v28898logstatsplain
-rw-r--r--Constprop.v15254logstatsplain
-rw-r--r--Constpropproof.v34669logstatsplain
-rw-r--r--Conventions.v8441logstatsplain
-rw-r--r--Inlining.v17356logstatsplain
-rw-r--r--Inliningaux.ml974logstatsplain
-rw-r--r--Inliningproof.v48146logstatsplain
-rw-r--r--Inliningspec.v26535logstatsplain
-rw-r--r--InterfGraph.v9809logstatsplain
-rw-r--r--Kildall.v40418logstatsplain
-rw-r--r--LTL.v10739logstatsplain
-rw-r--r--LTLin.v10261logstatsplain
-rw-r--r--LTLintyping.v4287logstatsplain
-rw-r--r--LTLtyping.v5206logstatsplain
-rw-r--r--Linear.v14561logstatsplain
-rw-r--r--Linearize.v8152logstatsplain
-rw-r--r--Linearizeaux.ml4115logstatsplain
-rw-r--r--Linearizeproof.v24744logstatsplain
-rw-r--r--Linearizetyping.v3814logstatsplain
-rw-r--r--Lineartyping.v6575logstatsplain
-rw-r--r--Liveness.v5463logstatsplain
-rw-r--r--Locations.v14426logstatsplain
-rw-r--r--Mach.v16828logstatsplain
-rw-r--r--Machtyping.v3639logstatsplain
-rw-r--r--Parallelmove.v13319logstatsplain
-rw-r--r--PrintAnnot.ml2738logstatsplain
-rw-r--r--PrintCminor.ml9712logstatsplain
-rw-r--r--PrintLTL.ml4077logstatsplain
-rw-r--r--PrintLTLin.ml3746logstatsplain
-rw-r--r--PrintMach.ml4010logstatsplain
-rw-r--r--PrintRTL.ml4455logstatsplain
-rw-r--r--RRE.v6643logstatsplain
-rw-r--r--RREproof.v22182logstatsplain
-rw-r--r--RREtyping.v3609logstatsplain
-rw-r--r--RTL.v17379logstatsplain
-rw-r--r--RTLgen.v23493logstatsplain
-rw-r--r--RTLgenaux.ml6243logstatsplain
-rw-r--r--RTLgenproof.v43493logstatsplain
-rw-r--r--RTLgenspec.v46629logstatsplain
-rw-r--r--RTLtyping.v19452logstatsplain
-rw-r--r--RTLtypingaux.ml5623logstatsplain
-rw-r--r--Registers.v1996logstatsplain
-rw-r--r--Reload.v9623logstatsplain
-rw-r--r--Reloadproof.v52577logstatsplain
-rw-r--r--Reloadtyping.v11979logstatsplain
-rw-r--r--Renumber.v3155logstatsplain
-rw-r--r--Renumberproof.v9089logstatsplain
-rw-r--r--Selection.v7429logstatsplain
-rw-r--r--Selectionproof.v21819logstatsplain
-rw-r--r--Stacking.v8879logstatsplain
-rw-r--r--Stackingproof.v98506logstatsplain
-rw-r--r--Tailcall.v4061logstatsplain
-rw-r--r--Tailcallproof.v22557logstatsplain
-rw-r--r--Tunneling.v4420logstatsplain
-rw-r--r--Tunnelingproof.v13769logstatsplain
-rw-r--r--Tunnelingtyping.v3417logstatsplain
-rw-r--r--Unusedglob.ml3027logstatsplain