compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	- Revised non-overflow constraints on memory injections so that	xleroy	2012-07-23	1	-3/+2
*	Make CPragmas common to all ports.	xleroy	2012-02-27	1	-108/+0
*	IA32 port: more faithful treatment of pseudoregister ST0.	xleroy	2011-08-08	1	-2/+7
*	Merge of branch "unsigned-offsets":	xleroy	2011-04-09	1	-13/+72
*	Merge of the reuse-temps branch:	xleroy	2010-09-02	1	-1/+4
*	Adding __builtin_annotation	xleroy	2010-09-01	1	-8/+8
*	Support for inlined built-ins.	xleroy	2010-06-29	1	-208/+4
*	Cleaned up handling of linker sections.	xleroy	2010-05-08	1	-143/+11
*	Coloring: allow to exclude user-specified registers from allocation.	xleroy	2010-04-10	1	-3/+28
*	Handling of volatile accesses through builtin functions.	xleroy	2010-03-08	1	-35/+34
*	Revised handling of #pragma section and small data areas	xleroy	2010-01-27	1	-43/+125
*	PowerPC/EABI port: preliminary support for #pragma section and	xleroy	2009-11-03	1	-0/+134
*	Use callee-save regs starting with R31/F31 and going down, like Diab does	xleroy	2009-11-02	1	-14/+14
*	Adapted to work with Coq 8.2-1v1.4.1	xleroy	2009-06-05	1	-1/+1
*	Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...	xleroy	2009-02-26	1	-6/+6
*	- Added alignment constraints to memory loads and stores.	xleroy	2009-01-11	1	-4/+0
*	Continuation of PowerPC/EABI port	xleroy	2008-12-31	1	-6/+10
*	Reorganized the development, modularizing away machine-dependent parts.	xleroy	2008-12-30	2	-0/+877