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.mll4693logstatsplain
-rw-r--r--CMparser.mly19021logstatsplain
-rw-r--r--CMtypecheck.ml11020logstatsplain
-rw-r--r--CMtypecheck.mli1116logstatsplain
-rw-r--r--CSE.v17189logstatsplain
-rw-r--r--CSEproof.v36348logstatsplain
-rw-r--r--CleanupLabels.v2778logstatsplain
-rw-r--r--CleanupLabelsproof.v10666logstatsplain
-rw-r--r--CleanupLabelstyping.v1967logstatsplain
-rw-r--r--Cminor.v39775logstatsplain
-rw-r--r--CminorSel.v17710logstatsplain
-rw-r--r--Coloring.v12276logstatsplain
-rw-r--r--Coloringaux.ml28581logstatsplain
-rw-r--r--Coloringaux.mli1017logstatsplain
-rw-r--r--Coloringproof.v28898logstatsplain
-rw-r--r--Constprop.v8150logstatsplain
-rw-r--r--Constpropproof.v19977logstatsplain
-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.ml10258logstatsplain
-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.v16295logstatsplain
-rw-r--r--RTLgen.v23669logstatsplain
-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.v8456logstatsplain
-rw-r--r--Selectionproof.v24722logstatsplain
-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