summaryrefslogtreecommitdiff
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v7843logplain
-rw-r--r--Allocproof.v26751logplain
-rw-r--r--Alloctyping.v6132logplain
-rw-r--r--Bounds.v12845logplain
-rw-r--r--CMlexer.mli1106logplain
-rw-r--r--CMlexer.mll4567logplain
-rw-r--r--CMparser.mly21281logplain
-rw-r--r--CMtypecheck.ml10555logplain
-rw-r--r--CMtypecheck.mli1116logplain
-rw-r--r--CSE.v19999logplain
-rw-r--r--CSEproof.v41268logplain
-rw-r--r--CleanupLabels.v2757logplain
-rw-r--r--CleanupLabelsproof.v10622logplain
-rw-r--r--CleanupLabelstyping.v1944logplain
-rw-r--r--Cminor.v38885logplain
-rw-r--r--CminorSel.v16540logplain
-rw-r--r--Coloring.v12276logplain
-rw-r--r--Coloringaux.ml28677logplain
-rw-r--r--Coloringaux.mli1017logplain
-rw-r--r--Coloringproof.v28898logplain
-rw-r--r--Constprop.v13487logplain
-rw-r--r--Constpropproof.v31625logplain
-rw-r--r--Conventions.v8441logplain
-rw-r--r--Inlining.v17356logplain
-rw-r--r--Inliningaux.ml974logplain
-rw-r--r--Inliningproof.v48151logplain
-rw-r--r--Inliningspec.v26536logplain
-rw-r--r--InterfGraph.v9803logplain
-rw-r--r--Kildall.v40282logplain
-rw-r--r--LTL.v10739logplain
-rw-r--r--LTLin.v10261logplain
-rw-r--r--LTLintyping.v4287logplain
-rw-r--r--LTLtyping.v5206logplain
-rw-r--r--Linear.v14561logplain
-rw-r--r--Linearize.v8177logplain
-rw-r--r--Linearizeaux.ml4115logplain
-rw-r--r--Linearizeproof.v24323logplain
-rw-r--r--Linearizetyping.v3747logplain
-rw-r--r--Lineartyping.v6575logplain
-rw-r--r--Locations.v14355logplain
-rw-r--r--Mach.v5977logplain
-rw-r--r--Machsem.v11931logplain
-rw-r--r--Machtyping.v3639logplain
-rw-r--r--Parallelmove.v13319logplain
-rw-r--r--PrintCminor.ml9710logplain
-rw-r--r--PrintLTL.ml4077logplain
-rw-r--r--PrintLTLin.ml3746logplain
-rw-r--r--PrintMach.ml4010logplain
-rw-r--r--PrintRTL.ml4451logplain
-rw-r--r--RRE.v6323logplain
-rw-r--r--RREproof.v20909logplain
-rw-r--r--RREtyping.v3551logplain
-rw-r--r--RTL.v17379logplain
-rw-r--r--RTLgen.v23493logplain
-rw-r--r--RTLgenaux.ml6243logplain
-rw-r--r--RTLgenproof.v43493logplain
-rw-r--r--RTLgenspec.v46629logplain
-rw-r--r--RTLtyping.v19452logplain
-rw-r--r--RTLtypingaux.ml5623logplain
-rw-r--r--Registers.v1996logplain
-rw-r--r--Reload.v9623logplain
-rw-r--r--Reloadproof.v52338logplain
-rw-r--r--Reloadtyping.v11960logplain
-rw-r--r--Renumber.v3155logplain
-rw-r--r--Renumberproof.v9089logplain
-rw-r--r--Selection.v7429logplain
-rw-r--r--Selectionproof.v21819logplain
-rw-r--r--Stacking.v8879logplain
-rw-r--r--Stackingproof.v98568logplain
-rw-r--r--Stackingtyping.v7377logplain
-rw-r--r--Tailcall.v4061logplain
-rw-r--r--Tailcallproof.v22557logplain
-rw-r--r--Tunneling.v4420logplain
-rw-r--r--Tunnelingproof.v13769logplain
-rw-r--r--Tunnelingtyping.v3417logplain
-rw-r--r--Unusedglob.ml3027logplain