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	-389/+389
*	ValueDomain: add some documentation comments.	Xavier Leroy	2015-07-19	1	-20/+32
*	Value analysis: keep track of pointer values that leak through small integers...	Xavier Leroy	2015-07-19	1	-153/+171
*	Value analysis: keep track of pointer values that leak through arithmetic ope...	Xavier Leroy	2015-07-19	1	-152/+160
*	ValueDomain.aptr_of_aval: be more conservative with pointers synthesized from...	Xavier Leroy	2015-07-18	1	-5/+13
*	Missing cases in ValueDomain.vnormalize, causing overapproximation.	Xavier Leroy	2015-07-18	1	-2/+2
*	Missing case in ValueDomain.pincl, causing incompleteness.	Xavier Leroy	2015-07-18	1	-0/+9
*	Introduce tolerance for casts of pointer values to/from 64-bit integers.	Xavier Leroy	2015-07-15	1	-3/+12
*	Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...	Xavier Leroy	2015-04-30	1	-3/+3
*	Revised semantics of comparisons between a pointer and 0.	Xavier Leroy	2015-03-15	1	-2/+4
*	- Support "switch" statements over 64-bit integers	xleroy	2014-08-17	1	-4/+177
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-84/+233
*	Refactoring: move symbol_offset into Genv.	xleroy	2014-05-24	1	-7/+4
*	Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...	xleroy	2014-04-09	1	-0/+14
*	Add option -Os to optimize for code size rather than for execution speed.	xleroy	2014-02-19	1	-16/+13
*	- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.	xleroy	2014-01-12	1	-5/+2
*	Updated ARM backend wrt new static analyses and optimizations.	xleroy	2014-01-02	1	-0/+12
*	Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).	xleroy	2013-12-30	1	-6/+4
*	Merge of branch value-analysis.	xleroy	2013-12-20	1	-0/+3692