backend - compcert - CompCert fork with minor modifications for Vericert.

Mode	Name	Size
-rwxr-xr-x	Affinity_relation.v	4634	log stats plain
-rw-r--r--	Allocation.v	7769	log stats plain
-rw-r--r--	Allocproof.v	25978	log stats plain
-rw-r--r--	Alloctyping.v	6110	log stats plain
-rw-r--r--	Bounds.v	11935	log stats plain
-rw-r--r--	CMlexer.mli	1106	log stats plain
-rw-r--r--	CMlexer.mll	4272	log stats plain
-rw-r--r--	CMparser.mly	16970	log stats plain
-rw-r--r--	CMtypecheck.ml	10479	log stats plain
-rw-r--r--	CMtypecheck.mli	1116	log stats plain
-rw-r--r--	CSE.v	15867	log stats plain
-rw-r--r--	CSEproof.v	31357	log stats plain
-rw-r--r--	Cminor.v	40457	log stats plain
-rw-r--r--	CminorSel.v	17236	log stats plain
-rw-r--r--	Coloring.v	12109	log stats plain
-rw-r--r--	Coloringaux.ml	21867	log stats plain
-rw-r--r--	Coloringaux.mli	969	log stats plain
-rw-r--r--	Coloringproof.v	28728	log stats plain
-rwxr-xr-x	Conservative_criteria.v	11221	log stats plain
-rw-r--r--	Constprop.v	7837	log stats plain
-rw-r--r--	Constpropproof.v	16281	log stats plain
-rwxr-xr-x	Delete_Preference_Edges_Adjacency.v	1928	log stats plain
-rwxr-xr-x	Delete_Preference_Edges_Degree.v	583	log stats plain
-rwxr-xr-x	Delete_Preference_Edges_Move.v	4629	log stats plain
-rwxr-xr-x	Edges.v	13951	log stats plain
-rwxr-xr-x	EqualSetMap.v	2259	log stats plain
-rwxr-xr-x	Freeze_WL.v	7428	log stats plain
-rwxr-xr-x	Graph_Facts.v	5245	log stats plain
-rw-r--r--	Graph_translation.v	107168	log stats plain
-rwxr-xr-x	IRC.v	3877	log stats plain
-rwxr-xr-x	IRCColoring.v	26606	log stats plain
-rwxr-xr-x	IRC_Graph_Functions.v	17960	log stats plain
-rwxr-xr-x	IRC_graph.v	391	log stats plain
-rwxr-xr-x	IRC_termination.v	15262	log stats plain
-rw-r--r--	InterfGraph.v	9782	log stats plain
-rwxr-xr-x	InterfGraphMapImp.v	281028	log stats plain
-rwxr-xr-x	InterfGraphProperties.v	202	log stats plain
-rwxr-xr-x	InterfGraph_Construction.v	6088	log stats plain
-rwxr-xr-x	Interference_adjacency.v	1897	log stats plain
-rw-r--r--	Kildall.v	41057	log stats plain
-rw-r--r--	LTL.v	10358	log stats plain
-rw-r--r--	LTLin.v	9853	log stats plain
-rw-r--r--	LTLintyping.v	4021	log stats plain
-rw-r--r--	LTLtyping.v	4889	log stats plain
-rw-r--r--	Linear.v	13345	log stats plain
-rw-r--r--	Linearize.v	8148	log stats plain
-rw-r--r--	Linearizeaux.ml	4368	log stats plain
-rw-r--r--	Linearizeproof.v	23486	log stats plain
-rw-r--r--	Linearizetyping.v	3679	log stats plain
-rw-r--r--	Lineartyping.v	4040	log stats plain
-rw-r--r--	Locations.v	12936	log stats plain
-rw-r--r--	Mach.v	4734	log stats plain
-rw-r--r--	Machabstr.v	12489	log stats plain
-rw-r--r--	Machabstr2concr.v	31957	log stats plain
-rw-r--r--	Machconcr.v	11123	log stats plain
-rw-r--r--	Machtyping.v	9503	log stats plain
-rwxr-xr-x	Merge_Adjacency.v	14014	log stats plain
-rwxr-xr-x	Merge_Degree.v	7678	log stats plain
-rwxr-xr-x	Merge_Move.v	28495	log stats plain
-rwxr-xr-x	Merge_WL.v	34268	log stats plain
-rw-r--r--	MyAllocation.v	51834	log stats plain
-rwxr-xr-x	MyRegisters.v	2912	log stats plain
-rwxr-xr-x	Order_arith.v	5992	log stats plain
-rwxr-xr-x	OrderedOption.v	2168	log stats plain
-rw-r--r--	Parallelmove.v	13137	log stats plain
-rw-r--r--	RTL.v	14978	log stats plain
-rw-r--r--	RTLgen.v	22721	log stats plain
-rw-r--r--	RTLgenaux.ml	4099	log stats plain
-rw-r--r--	RTLgenproof.v	43751	log stats plain
-rw-r--r--	RTLgenspec.v	42137	log stats plain
-rw-r--r--	RTLtyping.v	18941	log stats plain
-rw-r--r--	RTLtypingaux.ml	4993	log stats plain
-rw-r--r--	Registers.v	2018	log stats plain
-rwxr-xr-x	Regs.v	2541	log stats plain
-rw-r--r--	Reload.v	9429	log stats plain
-rw-r--r--	Reloadproof.v	48258	log stats plain
-rw-r--r--	Reloadtyping.v	11771	log stats plain
-rwxr-xr-x	Remove_Vertex_Adjacency.v	2426	log stats plain
-rwxr-xr-x	Remove_Vertex_Degree.v	5792	log stats plain
-rwxr-xr-x	Remove_Vertex_Move.v	7092	log stats plain
-rwxr-xr-x	Remove_Vertex_WL.v	18154	log stats plain
-rw-r--r--	Selection.v	7329	log stats plain
-rw-r--r--	Selectionproof.v	15594	log stats plain
-rwxr-xr-x	SetsFacts.v	2191	log stats plain
-rwxr-xr-x	Simplify_WL.v	6804	log stats plain
-rwxr-xr-x	Spill_WL.v	5877	log stats plain
-rw-r--r--	Stacking.v	8827	log stats plain
-rw-r--r--	Stackingproof.v	55408	log stats plain
-rw-r--r--	Stackingtyping.v	8582	log stats plain
-rw-r--r--	Tailcall.v	4093	log stats plain
-rw-r--r--	Tailcallproof.v	26530	log stats plain
-rw-r--r--	Tunneling.v	4927	log stats plain
-rw-r--r--	Tunnelingproof.v	13508	log stats plain
-rw-r--r--	Tunnelingtyping.v	3558	log stats plain
-rwxr-xr-x	Typed_interfgraphs.v	25558	log stats plain
-rwxr-xr-x	WS.v	7827	log stats plain