compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Interpreter produces more detailed trace, including name of semantic rules used.	Xavier Leroy	2015-02-08	1	-135/+164
*	Represent struct and union types by name instead of by structure.	Xavier Leroy	2014-12-22	1	-38/+42
*	Introduce symbol environments (type Senv.t) as a restricted view on global en...	Xavier Leroy	2014-11-26	1	-12/+12
*	Add Genv.public_symbol operation.	Xavier Leroy	2014-11-24	1	-7/+15
*	Revised translation of '&&' and '\|\|' to Clight.	Xavier Leroy	2014-10-13	1	-10/+10
*	- Support "switch" statements over 64-bit integers	xleroy	2014-08-17	1	-5/+3
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-14/+5
*	Continued: change typeconv t into incrdecr_type t for Epostincr.	xleroy	2014-04-16	1	-1/+1
*	Remove useless checks on type_of_global in dynamic semantics	xleroy	2014-02-20	1	-7/+3
*	Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).	xleroy	2013-12-30	1	-5/+10
*	Simpler, more robust emulation of calls to variadic functions:	xleroy	2013-12-28	1	-11/+11
*	Merge of branch value-analysis.	xleroy	2013-12-20	1	-1/+1
*	Revised semantics of external functions, continued:	xleroy	2013-11-18	1	-35/+36
*	Revised modeling of external functions and built-in functions: just axiomatize	xleroy	2013-11-17	1	-17/+18
*	Revised treatment of _Alignas, for better compatibility with GCC and Clang, a...	xleroy	2013-11-06	1	-2/+1
*	Merge of the "alignas" branch.	xleroy	2013-10-05	1	-4/+5
*	Merge of the float32 branch:	xleroy	2013-05-19	1	-1/+6
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-0/+4
*	Glasnost: making transparent a number of definitions that were opaque	xleroy	2013-03-10	1	-4/+3
*	Constant propagation within __builtin_annot.	xleroy	2013-02-24	1	-4/+5
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	1	-89/+92
*	Merge of the clightgen branch:	xleroy	2012-12-29	1	-2/+1
*	Support for inline assembly (asm statements).	xleroy	2012-12-18	1	-0/+7
*	Make Clight independent of CompCert C.	xleroy	2012-10-08	1	-0/+2
*	Merge of branch seq-and-or. See Changelog for details.	xleroy	2012-10-06	1	-1/+114
*	- Revised non-overflow constraints on memory injections so that	xleroy	2012-07-23	1	-3/+4
*	Revert unintentional commit #1955	xleroy	2012-07-06	1	-7/+0
*	Ajout trunk CompCert	blazy	2012-07-04	1	-0/+7
*	- Support for _Alignof(ty) operator from ISO C 2011	xleroy	2012-02-26	1	-0/+6
*	Merge of the "volatile" branch:	xleroy	2012-02-04	1	-969/+1188
*	Added volatile_read_global and volatile_store_global builtins.	xleroy	2012-01-15	1	-19/+71
*	Cleaned up old commented-out parts	xleroy	2011-08-19	1	-14/+0
*	Interp.ml: initialize PRNG	xleroy	2011-07-29	1	-2/+14
*	Added animation of the CompCert C semantics (ccomp -interp)	xleroy	2011-07-28	1	-0/+1814