debian-compcert - Debian packaging for CompCert

	Commit message (Expand)	Author	Age
...
*	Missing case: initialization of a global variable of type _Bool.	xleroy	2013-05-08
*	Revised semantics and compilation of 2-argument C operators to better match	xleroy	2013-05-06
*	Expand 64-bit integer comparisons into 32-bit integer comparisons.	xleroy	2013-04-29
*	driver: removed option -flonglong	xleroy	2013-04-22
*	Labeled statements inside switch were incorrectly processed.	xleroy	2013-04-22
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20
*	Error when calling un-prototyped function.	xleroy	2013-03-25
*	Watch out for behaviors exponential in the nesting of struct/union types.	xleroy	2013-03-23
*	Fixed parsing of hex float literals 0xNNNpMMM.	xleroy	2013-03-11
*	Glasnost: making transparent a number of definitions that were opaque	xleroy	2013-03-10
*	Constant propagation within __builtin_annot.	xleroy	2013-02-24
*	Pointers one past	xleroy	2013-02-15
*	lib/Integers.v: revised and extended, faster implementation based on	xleroy	2013-02-10
*	Errors for excessively large global variables or stack frames.	xleroy	2013-02-02
*	Camlcoq.ml: bug in conversion Z to string	xleroy	2013-01-29
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29
*	Avoid generating some obviously useless casts.	xleroy	2013-01-08
*	Put clighgen files in exportclight/	xleroy	2013-01-05
*	Print Swhile loops. Fix indentation.	xleroy	2013-01-05
*	Remove some useless "Require".	xleroy	2012-12-30
*	Merge of the clightgen branch:	xleroy	2012-12-29
*	Support for inline assembly (asm statements).	xleroy	2012-12-18
*	Globalenvs: allocate one-byte block with permissions Nonempty for each	xleroy	2012-11-12
*	Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)	xleroy	2012-11-03
*	Clight: split off the big step semantics in ClightBigstep.	xleroy	2012-10-14
*	Make Clight independent of CompCert C.	xleroy	2012-10-08
*	Merge of branch seq-and-or. See Changelog for details.	xleroy	2012-10-06
*	Remove Val.is_true and Val.is_false, no longer used.	xleroy	2012-08-06
*	Forgot to collect types of expressions	xleroy	2012-07-28
*	- Revised non-overflow constraints on memory injections so that	xleroy	2012-07-23
*	Strip quotes from section names during #pragma parsing.	xleroy	2012-07-11
*	Accept long double literals if -flongdouble is given.	xleroy	2012-07-10
*	Revert unintentional commit #1955	xleroy	2012-07-06
*	Ajout trunk CompCert	blazy	2012-07-04
*	More aggressive 'uncasting' before storing small integers	xleroy	2012-06-30
*	Use Flocq for floats	xleroy	2012-06-28
*	Make min_int / -1 and min_int % -1 semantically undefined	xleroy	2012-06-09
*	CSE: add recognition of some combined operators, conditions, and addressing m...	xleroy	2012-05-26
*	Merge of the newmem branch:	xleroy	2012-05-21
*	checklink: first import of Valentin Robert's validator for asm and link	xleroy	2012-03-28
*	Merge of Andrew Tolmach's HASP-related changes	xleroy	2012-03-09
*	Cprint: export Cprint.attributes	xleroy	2012-03-07
*	PowerPC: remove the fmadd and fmsub operators/Asm instructions	xleroy	2012-03-07
*	Remove 'near-code' access mode, makes no sense in CompCert	xleroy	2012-03-06
*	Problems with multiple declarations of publically-visible identifiers	xleroy	2012-02-29
*	Better printing of pointer values and of locations.	xleroy	2012-02-29
*	Make CPragmas common to all ports.	xleroy	2012-02-27
*	- Support for _Alignof(ty) operator from ISO C 2011	xleroy	2012-02-26
*	Translate CompCert C's "a ? b : c" to the equivalent simple Clight expr if	xleroy	2012-02-25
*	Simplified and cleaned up the passing of information from C2C to PrintAsm, as...	xleroy	2012-02-22