compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Verification of the Unusedglob pass (removal of unreferenced static global ↵	Xavier Leroy	2014-11-24	1	-32/+0
\| \| \| \|	definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
*	CSE: add recognition of some combined operators, conditions, and addressing ↵	xleroy	2012-05-26	1	-1/+1
\| \| \| \| \| \| \| \| \| \|	modes (cf. CombineOp.v) Memory model: cleaning up Memdata Inlining and new Constprop: updated for ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1902 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the newmem branch:	xleroy	2012-05-21	1	-0/+32
	- Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e