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	-124/+124
*	Refactoring of builtins and annotations in the back-end.	Xavier Leroy	2015-08-21	1	-3/+3
*	Extend annotations so that they can keep track of global variables and local ...	Xavier Leroy	2015-03-27	1	-0/+16
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-8/+94
*	Refactoring: move symbol_offset into Genv.	xleroy	2014-05-24	1	-13/+7
*	ia32/Select*: complete the modifications to shifts.	xleroy	2014-04-11	1	-8/+16
*	Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...	xleroy	2014-04-09	1	-12/+0
*	Support Onot operator / notl instruction. More constant propagation during s...	xleroy	2014-04-06	1	-10/+27
*	Merge of branch value-analysis.	xleroy	2013-12-20	1	-17/+1
*	Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms	xleroy	2013-09-14	1	-1/+8
*	Optimize integer divisions by positive constants, turning them into	xleroy	2013-07-29	1	-12/+29
*	Expand 64-bit integer comparisons into 32-bit integer comparisons.	xleroy	2013-04-29	1	-5/+4
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-14/+22
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	1	-18/+18
*	Remove some useless "Require".	xleroy	2012-12-30	1	-3/+0
*	Merge of branch seq-and-or. See Changelog for details.	xleroy	2012-10-06	1	-73/+91
*	Remove Val.is_true and Val.is_false, no longer used.	xleroy	2012-08-06	1	-8/+2
*	Support for MacOS X's indirect symbols. (first try)	xleroy	2012-07-13	1	-22/+31
*	CSE: add recognition of some combined operators, conditions, and addressing m...	xleroy	2012-05-26	1	-7/+3
*	Take advantage of Cmaskzero and Cmasknotzero.	xleroy	2012-02-24	1	-0/+23
*	Merge of the "volatile" branch:	xleroy	2012-02-04	1	-0/+25
*	Merge of the nonstrict-ops branch:	xleroy	2012-01-14	1	-676/+460
*	Merge of branch "unsigned-offsets":	xleroy	2011-04-09	1	-35/+39
*	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	-9/+17
*	Merge of the reuse-temps branch:	xleroy	2010-09-02	1	-0/+935