compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-1/+1
*	Use Coq strings instead of idents to name external and builtin functions.	Xavier Leroy	2015-10-11	1	-15/+8
*	Refactoring of builtins and annotations in the back-end.	Xavier Leroy	2015-08-21	1	-1/+12
*	Extended inline asm: revised treatment of clobbered registers.	Xavier Leroy	2015-05-09	1	-1/+29
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-14/+16
*	Support Onot operator / notl instruction. More constant propagation during s...	xleroy	2014-04-06	1	-0/+1
*	In Regalloc, dead code elimination, don't eliminate move operations	xleroy	2014-02-23	1	-0/+3
*	- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.	xleroy	2014-01-12	1	-1/+1
*	Optimize integer divisions by positive constants, turning them into	xleroy	2013-07-29	1	-0/+6
*	Merge of the float32 branch:	xleroy	2013-05-19	1	-1/+8
*	Revert suppression of __builtin_{read,write}_reversed for x86 and ARM,	xleroy	2013-04-29	1	-2/+9
*	Add __builtin_bswap16 and __builtin_bswap32 to all ports.	xleroy	2013-04-20	1	-5/+5
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-27/+165
*	Glasnost: making transparent a number of definitions that were opaque	xleroy	2013-03-10	1	-1/+2
*	Merge of the reuse-temps branch:	xleroy	2010-09-02	1	-0/+76