aboutsummaryrefslogtreecommitdiffstats
path: root/backend
ModeNameSize
-rw-r--r--Allocation.v8235logstatsplain
-rw-r--r--Allocproof.v26212logstatsplain
-rw-r--r--Alloctyping.v6105logstatsplain
-rw-r--r--Bounds.v11977logstatsplain
-rw-r--r--CMlexer.mli1106logstatsplain
-rw-r--r--CMlexer.mll4294logstatsplain
-rw-r--r--CMparser.mly17368logstatsplain
-rw-r--r--CMtypecheck.ml10727logstatsplain
-rw-r--r--CMtypecheck.mli1116logstatsplain
-rw-r--r--CSE.v16344logstatsplain
-rw-r--r--CSEproof.v31970logstatsplain
-rw-r--r--Cminor.v40808logstatsplain
-rw-r--r--CminorSel.v13941logstatsplain
-rw-r--r--Coloring.v12181logstatsplain
-rw-r--r--Coloringaux.ml19861logstatsplain
-rw-r--r--Coloringaux.mli969logstatsplain
-rw-r--r--Coloringproof.v30106logstatsplain
-rw-r--r--InterfGraph.v10221logstatsplain
-rw-r--r--Kildall.v38819logstatsplain
-rw-r--r--LTL.v10496logstatsplain
-rw-r--r--LTLin.v9845logstatsplain
-rw-r--r--LTLintyping.v3984logstatsplain
-rw-r--r--LTLtyping.v4826logstatsplain
-rw-r--r--Linear.v13418logstatsplain
-rw-r--r--Linearize.v8175logstatsplain
-rw-r--r--Linearizeaux.ml2943logstatsplain
-rw-r--r--Linearizeproof.v23830logstatsplain
-rw-r--r--Linearizetyping.v3700logstatsplain
-rw-r--r--Lineartyping.v3896logstatsplain
-rw-r--r--Locations.v12934logstatsplain
-rw-r--r--Mach.v4706logstatsplain
-rw-r--r--Machabstr.v12493logstatsplain
-rw-r--r--Machabstr2concr.v32285logstatsplain
-rw-r--r--Machconcr.v11120logstatsplain
-rw-r--r--Machtyping.v9330logstatsplain
-rw-r--r--Parallelmove.v13137logstatsplain
-rw-r--r--RTL.v15377logstatsplain
-rw-r--r--RTLgen.v22334logstatsplain
-rw-r--r--RTLgenaux.ml2676logstatsplain
-rw-r--r--RTLgenproof.v43132logstatsplain
-rw-r--r--RTLgenspec.v43564logstatsplain
-rw-r--r--RTLtyping.v19042logstatsplain
-rw-r--r--RTLtypingaux.ml5024logstatsplain
-rw-r--r--Registers.v2015logstatsplain
-rw-r--r--Reload.v9432logstatsplain
-rw-r--r--Reloadproof.v49192logstatsplain
-rw-r--r--Reloadtyping.v11668logstatsplain
-rw-r--r--Stacking.v8802logstatsplain
-rw-r--r--Stackingproof.v57831logstatsplain
-rw-r--r--Stackingtyping.v8372logstatsplain
-rw-r--r--Tunneling.v5614logstatsplain
-rw-r--r--Tunnelingproof.v12776logstatsplain
-rw-r--r--Tunnelingtyping.v3266logstatsplain