summaryrefslogtreecommitdiff
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v45149logplain
-rw-r--r--Allocproof.v82682logplain
-rw-r--r--Asmgenproof0.v26548logplain
-rw-r--r--Bounds.v12001logplain
-rw-r--r--CMlexer.mli1106logplain
-rw-r--r--CMlexer.mll5633logplain
-rw-r--r--CMparser.mly25536logplain
-rw-r--r--CMtypecheck.ml10155logplain
-rw-r--r--CMtypecheck.mli1116logplain
-rw-r--r--CSE.v22341logplain
-rw-r--r--CSEdomain.v5628logplain
-rw-r--r--CSEproof.v44633logplain
-rw-r--r--CleanupLabels.v2742logplain
-rw-r--r--CleanupLabelsproof.v11755logplain
-rw-r--r--Cminor.v41808logplain
-rw-r--r--CminorSel.v18345logplain
-rw-r--r--Constprop.v7965logplain
-rw-r--r--Constpropproof.v24629logplain
-rw-r--r--Conventions.v3646logplain
-rw-r--r--Deadcode.v7190logplain
-rw-r--r--Deadcodeproof.v36170logplain
-rw-r--r--IRC.ml30200logplain
-rw-r--r--IRC.mli1770logplain
-rw-r--r--Inlining.v16651logplain
-rw-r--r--Inliningaux.ml974logplain
-rw-r--r--Inliningproof.v48603logplain
-rw-r--r--Inliningspec.v27111logplain
-rw-r--r--Kildall.v55692logplain
-rw-r--r--LTL.v12868logplain
-rw-r--r--Linear.v11034logplain
-rw-r--r--Linearize.v8446logplain
-rw-r--r--Linearizeaux.ml4022logplain
-rw-r--r--Linearizeproof.v24396logplain
-rw-r--r--Lineartyping.v29411logplain
-rw-r--r--Liveness.v5448logplain
-rw-r--r--Locations.v16425logplain
-rw-r--r--Mach.v16985logplain
-rw-r--r--NeedDomain.v47718logplain
-rw-r--r--PrintAnnot.ml3071logplain
-rw-r--r--PrintCminor.ml10982logplain
-rw-r--r--PrintLTL.ml4484logplain
-rw-r--r--PrintLTLin.ml3746logplain
-rw-r--r--PrintMach.ml3931logplain
-rw-r--r--PrintRTL.ml3859logplain
-rw-r--r--PrintXTL.ml4871logplain
-rw-r--r--RTL.v22240logplain
-rw-r--r--RTLgen.v23373logplain
-rw-r--r--RTLgenaux.ml6530logplain
-rw-r--r--RTLgenproof.v49084logplain
-rw-r--r--RTLgenspec.v46582logplain
-rw-r--r--RTLtyping.v28111logplain
-rw-r--r--Regalloc.ml34191logplain
-rw-r--r--Registers.v1996logplain
-rw-r--r--Renumber.v3159logplain
-rw-r--r--Renumberproof.v9109logplain
-rw-r--r--SelectDiv.vp5986logplain
-rw-r--r--SelectDivproof.v21646logplain
-rw-r--r--SelectLong.vp14552logplain
-rw-r--r--SelectLongproof.v45476logplain
-rw-r--r--Selection.v8912logplain
-rw-r--r--Selectionproof.v24351logplain
-rw-r--r--Splitting.ml5515logplain
-rw-r--r--Stacking.v8900logplain
-rw-r--r--Stackingproof.v103302logplain
-rw-r--r--Tailcall.v4180logplain
-rw-r--r--Tailcallproof.v22735logplain
-rw-r--r--Tunneling.v4017logplain
-rw-r--r--Tunnelingproof.v14465logplain
-rw-r--r--Unusedglob.ml3027logplain
-rw-r--r--ValueAnalysis.v65280logplain
-rw-r--r--ValueDomain.v121387logplain
-rw-r--r--XTL.ml6521logplain
-rw-r--r--XTL.mli2947logplain