summaryrefslogtreecommitdiff
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v8235logplain
-rw-r--r--Allocproof.v26212logplain
-rw-r--r--Alloctyping.v6105logplain
-rw-r--r--Bounds.v11977logplain
-rw-r--r--CMlexer.mli1106logplain
-rw-r--r--CMlexer.mll4294logplain
-rw-r--r--CMparser.mly17368logplain
-rw-r--r--CMtypecheck.ml10727logplain
-rw-r--r--CMtypecheck.mli1116logplain
-rw-r--r--CSE.v16344logplain
-rw-r--r--CSEproof.v31970logplain
-rw-r--r--Cminor.v40808logplain
-rw-r--r--CminorSel.v13941logplain
-rw-r--r--Coloring.v12181logplain
-rw-r--r--Coloringaux.ml19861logplain
-rw-r--r--Coloringaux.mli969logplain
-rw-r--r--Coloringproof.v30106logplain
-rw-r--r--InterfGraph.v10221logplain
-rw-r--r--Kildall.v38819logplain
-rw-r--r--LTL.v10496logplain
-rw-r--r--LTLin.v9845logplain
-rw-r--r--LTLintyping.v3984logplain
-rw-r--r--LTLtyping.v4826logplain
-rw-r--r--Linear.v13418logplain
-rw-r--r--Linearize.v8175logplain
-rw-r--r--Linearizeaux.ml2943logplain
-rw-r--r--Linearizeproof.v23830logplain
-rw-r--r--Linearizetyping.v3700logplain
-rw-r--r--Lineartyping.v3896logplain
-rw-r--r--Locations.v12934logplain
-rw-r--r--Mach.v4706logplain
-rw-r--r--Machabstr.v12493logplain
-rw-r--r--Machabstr2concr.v32285logplain
-rw-r--r--Machconcr.v11120logplain
-rw-r--r--Machtyping.v9330logplain
-rw-r--r--Parallelmove.v13137logplain
-rw-r--r--RTL.v15377logplain
-rw-r--r--RTLgen.v22334logplain
-rw-r--r--RTLgenaux.ml2676logplain
-rw-r--r--RTLgenproof.v43132logplain
-rw-r--r--RTLgenspec.v43564logplain
-rw-r--r--RTLtyping.v19042logplain
-rw-r--r--RTLtypingaux.ml5024logplain
-rw-r--r--Registers.v2015logplain
-rw-r--r--Reload.v9432logplain
-rw-r--r--Reloadproof.v49192logplain
-rw-r--r--Reloadtyping.v11668logplain
-rw-r--r--Stacking.v8802logplain
-rw-r--r--Stackingproof.v57831logplain
-rw-r--r--Stackingtyping.v8372logplain
-rw-r--r--Tunneling.v5614logplain
-rw-r--r--Tunnelingproof.v12776logplain
-rw-r--r--Tunnelingtyping.v3266logplain