debian-compcert - Debian packaging for CompCert

	Commit message (Expand)	Author	Age
*	Optimize integer divisions by positive constants, turning them into	xleroy	2013-07-29
*	Bad printing of alignment on 'comm' symbols.	xleroy	2013-07-07
*	Missing case for EF_inline_asm.	xleroy	2013-06-20
*	powerpc: tentative support for Diab debug info	xleroy	2013-05-20
*	Add option -fno-tailcalls to turn off tailcall elimination (causes problem wi...	xleroy	2013-05-17
*	Update PowerPC port	xleroy	2013-05-17
*	Preliminary support for debugging info (-g).	xleroy	2013-05-17
*	Fixes in PowerPC port	xleroy	2013-04-21
*	Add __builtin_bswap16 and __builtin_bswap32 to all ports.	xleroy	2013-04-20
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20
*	Diab asm syntax issue	xleroy	2013-03-20
*	For Pfreeframe, generate an "addi" over GPR1 when possible, to work around a ...	xleroy	2013-03-18
*	Revised Stacking and Asmgen passes and Mach semantics:	xleroy	2013-03-01
*	Updated ARM and PowerPC ports with new handling of __builtin_annot.	xleroy	2013-02-24
*	Constant propagation within __builtin_annot.	xleroy	2013-02-24
*	Updated PowerPC port to new integers.	xleroy	2013-02-12
*	Errors for excessively large global variables or stack frames.	xleroy	2013-02-02
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29
*	Support for inline assembly (asm statements).	xleroy	2012-12-18
*	Add __builtin_fcti (double -> int conversion w/ round to nearest)	xleroy	2012-11-24
*	Globalenvs: allocate one-byte block with permissions Nonempty for each	xleroy	2012-11-12
*	- Revised non-overflow constraints on memory injections so that	xleroy	2012-07-23
*	Remove the PowerPC/MacOS X port, as MacOS no longer supports PowerPC.	xleroy	2012-07-14
*	Strip quotes from section names during #pragma parsing.	xleroy	2012-07-11
*	Added option -falign-functions	xleroy	2012-07-01
*	Use Flocq for floats	xleroy	2012-06-28
*	PowerPC: remove the fmadd and fmsub operators/Asm instructions	xleroy	2012-03-07
*	Improved instruction selection for "notint".	xleroy	2012-02-24
*	Simplified and cleaned up the passing of information from C2C to PrintAsm, as...	xleroy	2012-02-22
*	Work around limited excursion of conditional branches	xleroy	2012-02-13
*	Merge of the "volatile" branch:	xleroy	2012-02-04
*	Another typo in print_builtin_vstore_common	xleroy	2012-01-21
*	Typo in print_builtin_vstore_common	xleroy	2012-01-21
*	Cosmetic cleanups.	xleroy	2012-01-15
*	Added volatile_read_global and volatile_store_global builtins.	xleroy	2012-01-15
*	Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml chars	xleroy	2011-10-18
*	Revised emulation of packed structs	xleroy	2011-10-16
*	More builtins for ARM and PowerPC	xleroy	2011-08-05
*	Updated Makefile and dependencies. Typo in powerpc/PrintAsm.ml.	xleroy	2011-07-28
*	Added animation of the CompCert C semantics (ccomp -interp)	xleroy	2011-07-28
*	Back from Oregon commit.	xleroy	2011-07-05
*	Recognition of rlwimi instruction (useful for bitfield assignment)	xleroy	2011-06-21
*	Revised handling of annotation statements, and more generally built-in functi...	xleroy	2011-06-13
*	Nicer printing of annotations.	xleroy	2011-05-23
*	cparser/StructAssign: always use __builtin_memcpy + alignment indication	xleroy	2011-05-11
*	powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).	xleroy	2011-05-08
*	Fixed some typos	xleroy	2011-04-16
*	Preliminary support for 'aligned' and 'section' attributes, gcc-style. New-s...	xleroy	2011-04-16
*	Merge of branch "unsigned-offsets":	xleroy	2011-04-09
*	Comment char for Diab	xleroy	2011-03-13