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--CSE.v16602logplain
-rw-r--r--CSEproof.v31970logplain
-rw-r--r--Cminor.v40808logplain
-rw-r--r--CminorSel.v13941logplain
-rw-r--r--Coloring.v12181logplain
-rw-r--r--Coloringproof.v30106logplain
-rw-r--r--Constprop.v39939logplain
-rw-r--r--Constpropproof.v33533logplain
-rw-r--r--Conventions.v25579logplain
-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.v13366logplain
-rw-r--r--Linearize.v8175logplain
-rw-r--r--Linearizeproof.v23813logplain
-rw-r--r--Linearizetyping.v3700logplain
-rw-r--r--Lineartyping.v3896logplain
-rw-r--r--Locations.v16583logplain
-rw-r--r--Mach.v4706logplain
-rw-r--r--Machabstr.v12435logplain
-rw-r--r--Machabstr2concr.v32285logplain
-rw-r--r--Machconcr.v11062logplain
-rw-r--r--Machtyping.v9330logplain
-rw-r--r--Op.v35538logplain
-rw-r--r--PPC.v36157logplain
-rw-r--r--PPCgen.v19856logplain
-rw-r--r--PPCgenproof.v52553logplain
-rw-r--r--PPCgenproof1.v61784logplain
-rw-r--r--PPCgenretaddr.v6965logplain
-rw-r--r--Parallelmove.v13137logplain
-rw-r--r--RTL.v15377logplain
-rw-r--r--RTLgen.v22334logplain
-rw-r--r--RTLgenproof.v43132logplain
-rw-r--r--RTLgenspec.v43564logplain
-rw-r--r--RTLtyping.v19042logplain
-rw-r--r--Registers.v2015logplain
-rw-r--r--Reload.v9432logplain
-rw-r--r--Reloadproof.v49210logplain
-rw-r--r--Reloadtyping.v11668logplain
-rw-r--r--Selection.v37017logplain
-rw-r--r--Selectionproof.v45472logplain
-rw-r--r--Stacking.v10830logplain
-rw-r--r--Stackingproof.v60455logplain
-rw-r--r--Stackingtyping.v8344logplain
-rw-r--r--Tunneling.v5614logplain
-rw-r--r--Tunnelingproof.v12776logplain
-rw-r--r--Tunnelingtyping.v3266logplain