debian-compcert - Debian packaging for CompCert

	Commit message (Expand)	Author	Age
*	Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.	xleroy	2011-03-09
*	Float.intoffloat and Float.intuoffloat are now partial functions.	xleroy	2010-10-28
*	Various algorithmic improvements that reduce compile times (thanks Alexandre ...	xleroy	2010-10-27
*	Typo in doc comment	xleroy	2010-09-21
*	Merge of the reuse-temps branch:	xleroy	2010-09-02
*	Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext	xleroy	2010-08-21
*	Nettoyages pour doc	xleroy	2010-08-18
*	Merge of branches/full-expr-4:	xleroy	2010-08-18
*	Forgot to add this file. Part of the refactoring of $ARCH/$SYSTEM/Conventions.v	xleroy	2010-07-07
*	Support for inlined built-ins.	xleroy	2010-06-29
*	Merging the Princeton implementation of the memory model. Separate axioms in...	xleroy	2010-06-28
*	Updated Caml parts to match new representation for global variables.	xleroy	2010-05-26
*	More faithful semantics for volatile reads and writes.	xleroy	2010-05-23
*	- Extended traces so that pointers within globals are supported as event values.	xleroy	2010-05-10
*	Improved coalescing heuristics based on Hailperin's paper.	xleroy	2010-05-08
*	Removed an ADMITTED that was unused, fortunately	xleroy	2010-05-05
*	Pretty-printers for RTL and LTL. Not yet well integrated.	xleroy	2010-05-02
*	Compute spill costs.	xleroy	2010-05-02
*	In compilation of Sassign, avoid systematic move from a fresh temp.	xleroy	2010-05-02
*	Coloring: allow to exclude user-specified registers from allocation.	xleroy	2010-04-10
*	Include targets of preference edges in all_interf_regs. Not needed for corre...	xleroy	2010-03-30
*	More resistant proof	xleroy	2010-03-28
*	Restored the big-step semantics for Cminor	xleroy	2010-03-11
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07
*	Switching to the new C parser/elaborator/simplifier	xleroy	2010-03-03
*	Backtracking on commit 1220	xleroy	2010-01-13
*	ajout branche allocation de registres	blazy	2010-01-08
*	MAJ extraction after changes in Integers	xleroy	2009-12-16
*	Revised lib/Integers.v to make it parametric w.r.t. word size.	xleroy	2009-11-19
*	More realistic treatment of jump tables: show the absence of overflow when ac...	xleroy	2009-11-10
*	Added support for jump tables in back end.	xleroy	2009-11-10
*	Coloringaux: make identifiers unique; special treatment of precolored	xleroy	2009-08-26
*	Forgot to add some files	xleroy	2009-08-18
*	"val_match_approx_increasing" moved from mach-dep part to mach-indep part.	xleroy	2009-08-18
*	Refactoring of Constprop and Constpropproof into a machine-dependent part and...	xleroy	2009-08-17
*	Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...	xleroy	2009-08-17
*	Cil2Csyntax: added goto and labels; added assignment between structs	xleroy	2009-08-16
*	Distinguish two kinds of nonterminating behaviors: silent divergence	xleroy	2009-08-16
*	Update spill costs when coalescing	xleroy	2009-08-16
*	Added 'going wrong' behaviors	xleroy	2009-08-05
*	Transition semantics for Clight and Csharpminor	xleroy	2009-08-03
*	Adapted to work with Coq 8.2-1	xleroy	2009-06-05
*	Added tail call optimization pass	xleroy	2009-03-26
*	New linearization heuristic	xleroy	2009-02-27
*	Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...	xleroy	2009-01-29
*	Elimination of "alloc" instruction in Caml files and test files.	xleroy	2009-01-11
*	- Added alignment constraints to memory loads and stores.	xleroy	2009-01-11
*	Fixed unary minus	xleroy	2009-01-07
*	Cminor, CminorSel: removed useless premises in rules for Sreturn	xleroy	2009-01-04
*	Reorganized the development, modularizing away machine-dependent parts.	xleroy	2008-12-30