aboutsummaryrefslogtreecommitdiffstats
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v48397logstatsplain
-rw-r--r--Allocproof.v89664logstatsplain
-rw-r--r--Asmexpandaux.ml5457logstatsplain
-rw-r--r--Asmexpandaux.mli1873logstatsplain
-rw-r--r--Asmgenproof0.v27118logstatsplain
-rw-r--r--Bounds.v12047logstatsplain
-rw-r--r--CMlexer.mli1106logstatsplain
-rw-r--r--CMlexer.mll5757logstatsplain
-rw-r--r--CMparser.mly26350logstatsplain
-rw-r--r--CMtypecheck.ml10513logstatsplain
-rw-r--r--CMtypecheck.mli1116logstatsplain
-rw-r--r--CSE.v22358logstatsplain
-rw-r--r--CSEdomain.v5626logstatsplain
-rw-r--r--CSEproof.v44990logstatsplain
-rw-r--r--CleanupLabels.v2713logstatsplain
-rw-r--r--CleanupLabelsproof.v11448logstatsplain
-rw-r--r--Cminor.v43625logstatsplain
-rw-r--r--CminorSel.v20704logstatsplain
-rw-r--r--Constprop.v8326logstatsplain
-rw-r--r--Constpropproof.v24032logstatsplain
-rw-r--r--Conventions.v3637logstatsplain
-rw-r--r--Deadcode.v7785logstatsplain
-rw-r--r--Deadcodeproof.v41540logstatsplain
-rw-r--r--Debugvar.v11876logstatsplain
-rw-r--r--Debugvarproof.v18335logstatsplain
-rw-r--r--Fileinfo.ml2755logstatsplain
-rw-r--r--IRC.ml30565logstatsplain
-rw-r--r--IRC.mli1761logstatsplain
-rw-r--r--Inlining.v17091logstatsplain
-rw-r--r--Inliningaux.ml960logstatsplain
-rw-r--r--Inliningproof.v51775logstatsplain
-rw-r--r--Inliningspec.v27424logstatsplain
-rw-r--r--Kildall.v55525logstatsplain
-rw-r--r--LTL.v12672logstatsplain
-rw-r--r--Linear.v10836logstatsplain
-rw-r--r--Linearize.v8211logstatsplain
-rw-r--r--Linearizeaux.ml3980logstatsplain
-rw-r--r--Linearizeproof.v24034logstatsplain
-rw-r--r--Lineartyping.v11762logstatsplain
-rw-r--r--Liveness.v5504logstatsplain
-rw-r--r--Locations.v17279logstatsplain
-rw-r--r--Mach.v16314logstatsplain
-rw-r--r--NeedDomain.v45524logstatsplain
-rw-r--r--PrintAsm.ml5268logstatsplain
-rw-r--r--PrintAsm.mli943logstatsplain
-rw-r--r--PrintAsmaux.ml9348logstatsplain
-rw-r--r--PrintCminor.ml11640logstatsplain
-rw-r--r--PrintLTL.ml4435logstatsplain
-rw-r--r--PrintLTLin.ml3746logstatsplain
-rw-r--r--PrintMach.ml3543logstatsplain
-rw-r--r--PrintRTL.ml3887logstatsplain
-rw-r--r--PrintXTL.ml4921logstatsplain
-rw-r--r--RTL.v22402logstatsplain
-rw-r--r--RTLgen.v24652logstatsplain
-rw-r--r--RTLgenaux.ml3664logstatsplain
-rw-r--r--RTLgenproof.v52667logstatsplain
-rw-r--r--RTLgenspec.v47185logstatsplain
-rw-r--r--RTLtyping.v32672logstatsplain
-rw-r--r--Regalloc.ml39545logstatsplain
-rw-r--r--Registers.v3000logstatsplain
-rw-r--r--Renumber.v3157logstatsplain
-rw-r--r--Renumberproof.v9192logstatsplain
-rw-r--r--SelectDiv.vp6376logstatsplain
-rw-r--r--SelectDivproof.v22162logstatsplain
-rw-r--r--SelectLong.vp13086logstatsplain
-rw-r--r--SelectLongproof.v47902logstatsplain
-rw-r--r--Selection.v14940logstatsplain
-rw-r--r--Selectionproof.v43279logstatsplain
-rw-r--r--Splitting.ml5561logstatsplain
-rw-r--r--Stacking.v9268logstatsplain
-rw-r--r--Stackingproof.v105101logstatsplain
-rw-r--r--Tailcall.v3966logstatsplain
-rw-r--r--Tailcallproof.v22171logstatsplain
-rw-r--r--Tunneling.v3984logstatsplain
-rw-r--r--Tunnelingproof.v14250logstatsplain
-rw-r--r--Unusedglob.v5064logstatsplain
-rw-r--r--Unusedglobproof.v52621logstatsplain
-rw-r--r--ValueAnalysis.v71237logstatsplain
-rw-r--r--ValueDomain.v136740logstatsplain
-rw-r--r--XTL.ml7053logstatsplain
-rw-r--r--XTL.mli2966logstatsplain