compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge of branch value-analysis.	xleroy	2013-12-20	1	-6/+17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Recombine x = cmp(...); if (x == 1) ...	xleroy	2012-07-01	1	-4/+24
\| \| \| \| \| \| \|	and x = cmp(...); if (x != 1) ... git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Removed Oandimm, etc, cases, because of 2-address constraints...	xleroy	2012-05-29	1	-15/+0
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1904 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	CSE: add recognition of some combined operators, conditions, and addressing ↵	xleroy	2012-05-26	1	-0/+101
	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