summaryrefslogtreecommitdiff
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v7946logplain
-rw-r--r--Allocproof.v26778logplain
-rw-r--r--Alloctyping.v6132logplain
-rw-r--r--Bounds.v12866logplain
-rw-r--r--CMlexer.mli1106logplain
-rw-r--r--CMlexer.mll4693logplain
-rw-r--r--CMparser.mly19021logplain
-rw-r--r--CMtypecheck.ml11020logplain
-rw-r--r--CMtypecheck.mli1116logplain
-rw-r--r--CSE.v20369logplain
-rw-r--r--CSEproof.v41270logplain
-rw-r--r--CleanupLabels.v2778logplain
-rw-r--r--CleanupLabelsproof.v10666logplain
-rw-r--r--CleanupLabelstyping.v1967logplain
-rw-r--r--Cminor.v39775logplain
-rw-r--r--CminorSel.v18049logplain
-rw-r--r--Coloring.v12276logplain
-rw-r--r--Coloringaux.ml28581logplain
-rw-r--r--Coloringaux.mli1017logplain
-rw-r--r--Coloringproof.v28898logplain
-rw-r--r--Constprop.v12232logplain
-rw-r--r--Constpropproof.v32515logplain
-rw-r--r--Conventions.v8441logplain
-rw-r--r--Inlining.v17520logplain
-rw-r--r--Inliningaux.ml974logplain
-rw-r--r--Inliningproof.v47859logplain
-rw-r--r--Inliningspec.v27249logplain
-rw-r--r--InterfGraph.v9824logplain
-rw-r--r--Kildall.v40282logplain
-rw-r--r--LTL.v10739logplain
-rw-r--r--LTLin.v10310logplain
-rw-r--r--LTLintyping.v4348logplain
-rw-r--r--LTLtyping.v5246logplain
-rw-r--r--Linear.v14582logplain
-rw-r--r--Linearize.v8227logplain
-rw-r--r--Linearizeaux.ml4436logplain
-rw-r--r--Linearizeproof.v24323logplain
-rw-r--r--Linearizetyping.v3747logplain
-rw-r--r--Lineartyping.v6592logplain
-rw-r--r--Locations.v14376logplain
-rw-r--r--Mach.v6045logplain
-rw-r--r--Machsem.v11952logplain
-rw-r--r--Machtyping.v3775logplain
-rw-r--r--Parallelmove.v13342logplain
-rw-r--r--PrintCminor.ml10258logplain
-rw-r--r--PrintLTL.ml4077logplain
-rw-r--r--PrintLTLin.ml3784logplain
-rw-r--r--PrintMach.ml4048logplain
-rw-r--r--PrintRTL.ml4516logplain
-rw-r--r--RRE.v6394logplain
-rw-r--r--RREproof.v20940logplain
-rw-r--r--RREtyping.v3553logplain
-rw-r--r--RTL.v16295logplain
-rw-r--r--RTLgen.v24056logplain
-rw-r--r--RTLgenaux.ml4156logplain
-rw-r--r--RTLgenproof.v45263logplain
-rw-r--r--RTLgenspec.v47730logplain
-rw-r--r--RTLtyping.v19497logplain
-rw-r--r--RTLtypingaux.ml5623logplain
-rw-r--r--Registers.v2018logplain
-rw-r--r--Reload.v9694logplain
-rw-r--r--Reloadproof.v52386logplain
-rw-r--r--Reloadtyping.v11980logplain
-rw-r--r--Renumber.v3175logplain
-rw-r--r--Renumberproof.v9151logplain
-rw-r--r--Selection.v8834logplain
-rw-r--r--Selectionproof.v25615logplain
-rw-r--r--Stacking.v8920logplain
-rw-r--r--Stackingproof.v98463logplain
-rw-r--r--Stackingtyping.v7398logplain
-rw-r--r--Tailcall.v4088logplain
-rw-r--r--Tailcallproof.v22557logplain
-rw-r--r--Tunneling.v4998logplain
-rw-r--r--Tunnelingproof.v13769logplain
-rw-r--r--Tunnelingtyping.v3561logplain
-rw-r--r--Unusedglob.ml3176logplain