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	-79/+79
*	Value analysis: keep track of pointer values that leak through small integers...	Xavier Leroy	2015-07-19	1	-20/+20
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-19/+37
*	Refactoring: move symbol_offset into Genv.	xleroy	2014-05-24	1	-19/+12
*	Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...	xleroy	2014-04-09	1	-15/+67
*	Support Onot operator / notl instruction. More constant propagation during s...	xleroy	2014-04-06	1	-0/+2
*	Add option -Os to optimize for code size rather than for execution speed.	xleroy	2014-02-19	1	-0/+1
*	Merge of branch value-analysis.	xleroy	2013-12-20	1	-254/+263
*	Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms	xleroy	2013-09-14	1	-0/+36
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-1/+6
*	Constant propagation within __builtin_annot.	xleroy	2013-02-24	1	-18/+0
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	1	-9/+9
*	Remove some useless "Require".	xleroy	2012-12-30	1	-1/+0
*	Make min_int / -1 and min_int % -1 semantically undefined	xleroy	2012-06-09	1	-2/+4
*	Merge of the newmem branch:	xleroy	2012-05-21	1	-1/+2
*	Added volatile_read_global and volatile_store_global builtins.	xleroy	2012-01-15	1	-0/+19
*	Merge of the nonstrict-ops branch:	xleroy	2012-01-14	1	-315/+239
*	Merge of branch "unsigned-offsets":	xleroy	2011-04-09	1	-27/+28
*	Float.intoffloat and Float.intuoffloat are now partial functions.	xleroy	2010-10-28	1	-0/+2
*	Merge of the reuse-temps branch:	xleroy	2010-09-02	1	-0/+497