aboutsummaryrefslogtreecommitdiffstats
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v7946logstatsplain
-rw-r--r--Allocproof.v26778logstatsplain
-rw-r--r--Alloctyping.v6132logstatsplain
-rw-r--r--Bounds.v12866logstatsplain
-rw-r--r--CMlexer.mli1106logstatsplain
-rw-r--r--CMlexer.mll4272logstatsplain
-rw-r--r--CMparser.mly16981logstatsplain
-rw-r--r--CMtypecheck.ml10468logstatsplain
-rw-r--r--CMtypecheck.mli1116logstatsplain
-rw-r--r--CSE.v15776logstatsplain
-rw-r--r--CSEproof.v31057logstatsplain
-rw-r--r--CleanupLabels.v2778logstatsplain
-rw-r--r--CleanupLabelsproof.v10666logstatsplain
-rw-r--r--CleanupLabelstyping.v1967logstatsplain
-rw-r--r--Cminor.v38791logstatsplain
-rw-r--r--CminorSel.v17710logstatsplain
-rw-r--r--Coloring.v12276logstatsplain
-rw-r--r--Coloringaux.ml28128logstatsplain
-rw-r--r--Coloringaux.mli1017logstatsplain
-rw-r--r--Coloringproof.v28898logstatsplain
-rw-r--r--Constprop.v8002logstatsplain
-rw-r--r--Constpropproof.v19638logstatsplain
-rw-r--r--Conventions.v8441logstatsplain
-rw-r--r--InterfGraph.v9824logstatsplain
-rw-r--r--Kildall.v40282logstatsplain
-rw-r--r--LTL.v10739logstatsplain
-rw-r--r--LTLin.v10310logstatsplain
-rw-r--r--LTLintyping.v4348logstatsplain
-rw-r--r--LTLtyping.v5246logstatsplain
-rw-r--r--Linear.v14582logstatsplain
-rw-r--r--Linearize.v8227logstatsplain
-rw-r--r--Linearizeaux.ml4436logstatsplain
-rw-r--r--Linearizeproof.v24357logstatsplain
-rw-r--r--Linearizetyping.v3747logstatsplain
-rw-r--r--Lineartyping.v6592logstatsplain
-rw-r--r--Locations.v14376logstatsplain
-rw-r--r--Mach.v6045logstatsplain
-rw-r--r--Machsem.v11952logstatsplain
-rw-r--r--Machtyping.v3775logstatsplain
-rw-r--r--Parallelmove.v13342logstatsplain
-rw-r--r--PrintCminor.ml8619logstatsplain
-rw-r--r--PrintLTL.ml4077logstatsplain
-rw-r--r--PrintLTLin.ml3844logstatsplain
-rw-r--r--PrintMach.ml4108logstatsplain
-rw-r--r--PrintRTL.ml4810logstatsplain
-rw-r--r--RRE.v6394logstatsplain
-rw-r--r--RREproof.v20940logstatsplain
-rw-r--r--RREtyping.v3553logstatsplain
-rw-r--r--RTL.v16282logstatsplain
-rw-r--r--RTLgen.v23668logstatsplain
-rw-r--r--RTLgenaux.ml4156logstatsplain
-rw-r--r--RTLgenproof.v44226logstatsplain
-rw-r--r--RTLgenspec.v46750logstatsplain
-rw-r--r--RTLtyping.v19497logstatsplain
-rw-r--r--RTLtypingaux.ml5623logstatsplain
-rw-r--r--Registers.v2018logstatsplain
-rw-r--r--Reload.v9694logstatsplain
-rw-r--r--Reloadproof.v52386logstatsplain
-rw-r--r--Reloadtyping.v11980logstatsplain
-rw-r--r--Selection.v8249logstatsplain
-rw-r--r--Selectionproof.v24287logstatsplain
-rw-r--r--Stacking.v8920logstatsplain
-rw-r--r--Stackingproof.v97974logstatsplain
-rw-r--r--Stackingtyping.v7398logstatsplain
-rw-r--r--Tailcall.v4088logstatsplain
-rw-r--r--Tailcallproof.v22557logstatsplain
-rw-r--r--Tunneling.v4998logstatsplain
-rw-r--r--Tunnelingproof.v13769logstatsplain
-rw-r--r--Tunnelingtyping.v3561logstatsplain