compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Improved instruction selection for "notint".	xleroy	2012-02-24	1	-8/+19
*	Merge of the "volatile" branch:	xleroy	2012-02-04	1	-0/+25
*	powerpc/SelectOp: optimize the pattern ((x >>s N) & N1) & N2 common in a cert...	xleroy	2012-01-21	1	-0/+15
*	Merge of the nonstrict-ops branch:	xleroy	2012-01-14	1	-702/+490
*	Recognition of rlwimi instruction (useful for bitfield assignment)	xleroy	2011-06-21	1	-0/+12
*	Merge of branch "unsigned-offsets":	xleroy	2011-04-09	1	-38/+42
*	float->int conversions, continued: weaker axiomatization.	xleroy	2010-10-29	1	-2/+2
*	Float.intoffloat and Float.intuoffloat are now partial functions.	xleroy	2010-10-28	1	-11/+20
*	Merge of the reuse-temps branch:	xleroy	2010-09-02	1	-53/+53
*	Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext	xleroy	2010-08-21	1	-3/+3
*	Optimisation: addrsymbol + (expr + cst) and addrstack + (expr + cst).	xleroy	2010-05-02	1	-0/+12
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07	1	-21/+14
*	Wrong rlwinm generated for 'x mod 1'	xleroy	2010-03-02	1	-58/+57
*	Revised lib/Integers.v to make it parametric w.r.t. word size.	xleroy	2009-11-19	1	-12/+8
*	Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...	xleroy	2009-08-17	1	-0/+957