compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Update for 1.8.1 releasev1.8.1	xleroy	2011-03-14	2	-5/+31
*	Incompatibility 8.3 / 8.3pl1	xleroy	2011-03-14	1	-1/+1
*	Comment char for Diab	xleroy	2011-03-13	1	-1/+1
*	Slightly nicer semantics for initialization	xleroy	2011-03-13	1	-28/+29
*	More global initialization work done and proved in Coq.	xleroy	2011-03-13	4	-80/+410
*	Initializers for global variables: compile-time evaluation of expressions don...	xleroy	2011-03-12	11	-159/+891
*	Undesirable optimization of 'print'	xleroy	2011-03-10	1	-0/+2
*	Bitfields: MSB-to-LSB in addition to LSB-to-MSB	xleroy	2011-03-10	3	-11/+39
*	Revised signed/unsigned char handling.	xleroy	2011-03-10	4	-18/+8
*	Improved test harness	xleroy	2011-03-10	3	-0/+14
*	Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.	xleroy	2011-03-09	18	-85/+70
*	Treat "char" as unsigned OR signed depending on the configuration.	xleroy	2011-03-09	8	-10/+58
*	Use movapd instead of movsd for xmm reg-reg move: it avoids partial register ...	xleroy	2010-11-28	1	-1/+1
*	In StructAssign: be careful not to duplicate accesses to a volatile variable.	xleroy	2010-11-10	3	-9/+24
*	float->int conversions, continued: weaker axiomatization.	xleroy	2010-10-29	5	-29/+9
*	Float.intoffloat and Float.intuoffloat are now partial functions.	xleroy	2010-10-28	21	-62/+139
*	Various algorithmic improvements that reduce compile times (thanks Alexandre ...	xleroy	2010-10-27	19	-141/+965
*	License for Floataux.ml	xleroy	2010-10-27	2	-1/+4
*	Inconsistent treatment of "lone" zero-width bit fields	xleroy	2010-09-24	5	-24/+53
*	Bizarre use of struct valuev1.8	xleroy	2010-09-21	2	-2/+2
*	Update for release 1.8	xleroy	2010-09-21	3	-18/+42
*	Typo in doc comment	xleroy	2010-09-21	1	-2/+2
*	Memory.v: added drop_perm operation	xleroy	2010-09-21	3	-46/+427
*	No crash if nonexistent input file.	xleroy	2010-09-14	2	-2/+3
*	Comments	xleroy	2010-09-10	1	-8/+10
*	Improvements for int8 and int16 stores	xleroy	2010-09-10	4	-11/+53
*	Updates for IA32-Cygwin.	xleroy	2010-09-08	5	-33/+63
*	Updated	xleroy	2010-09-04	2	-12/+43
*	++ on volatile not supported.	xleroy	2010-09-04	1	-2/+2
*	Update: adding __builtin_annotation	xleroy	2010-09-04	1	-1/+36
*	Simplified stdlib wrapper; use it only under MacOS X	xleroy	2010-09-04	7	-278/+76
*	Support for __builtin_fmax and __builtin_fmin	xleroy	2010-09-04	2	-1/+22
*	Better emulation of long long as a struct.	xleroy	2010-09-04	2	-16/+51
*	Merge of the reuse-temps branch:	xleroy	2010-09-02	89	-2579/+12842
*	Semantics of annotations	xleroy	2010-09-02	1	-5/+69
*	Adding __builtin_annotation	xleroy	2010-09-01	8	-12/+219
*	Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of readi...	xleroy	2010-09-01	10	-15/+119
*	Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext	xleroy	2010-08-21	7	-1121/+1148
*	Nettoyages pour doc	xleroy	2010-08-18	4	-21/+15
*	Removed useless constraints on return type at Sreturn instructions	xleroy	2010-08-18	8	-36/+28
*	Copyright banner	xleroy	2010-08-18	1	-0/+12
*	Renamed C2Clight into C2C	xleroy	2010-08-18	4	-7/+7
*	Merge of branches/full-expr-4:	xleroy	2010-08-18	56	-6180/+13619
*	Wrong cast in constant_expr	xleroy	2010-08-04	1	-3/+3
*	Fix extraction problem	xleroy	2010-07-14	2	-4/+4
*	Preliminary support for gcc-style __attribute__ over types	xleroy	2010-07-08	6	-135/+168
*	Bug in cparser/AddCasts.ml.	xleroy	2010-07-08	4	-4/+22
*	Render unto Caesar... (Mention contribution by Dockins and Steward.)	xleroy	2010-07-08	1	-0/+2
*	Forgot to add this file. Part of the refactoring of $ARCH/$SYSTEM/Conventions.v	xleroy	2010-07-07	1	-0/+251
*	Support for inlined built-ins.	xleroy	2010-06-29	77	-1302/+1228