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	-67/+0
\| \| \| \|	definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-0/+4
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Future-proofing: keep signature information in IA32 and PowerPC Asm, just ↵	xleroy	2013-12-26	1	-3/+3
\| \| \| \| \| \|	like we already do in ARM Asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	powerpc/: new unary operation "addsymbol"	xleroy	2013-11-17	1	-0/+2
\| \| \| \| \| \| \| \|	Support far-data addressing in sections. (Currently ignored in checklink.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the newmem branch:	xleroy	2012-05-21	1	-0/+61
	- 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