compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
...
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-1/+2
*	Update Coq documentationv2.3	xleroy	2014-05-05	1	-1/+1
*	Integration of Jacques-Henri Jourdan's verified parser.	xleroy	2014-04-29	1	-3/+18
*	ia32/Select*: complete the modifications to shifts.	xleroy	2014-04-11	1	-7/+8
*	Merge of branch linear-typing:	xleroy	2014-04-06	1	-1/+1
*	Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):	xleroy	2014-03-28	1	-1/+1
*	Move wt_instr_inv where it belongs.	xleroy	2014-03-27	1	-1/+1
*	Add option -Os to optimize for code size rather than for execution speed.	xleroy	2014-02-19	1	-1/+1
*	Introduce and use the platform-specific Archi module giving:	xleroy	2014-01-03	1	-1/+1
*	Merge of branch value-analysis.	xleroy	2013-12-20	1	-2/+4
*	powerpc/: new unary operation "addsymbol"	xleroy	2013-11-17	1	-1/+1
*	Merge of Flocq version 2.2.0.	xleroy	2013-08-02	1	-10/+12
*	Optimize integer divisions by positive constants, turning them into	xleroy	2013-07-29	1	-2/+2
*	Updating LICENSE and license headers, continued.	xleroy	2013-06-17	1	-0/+3
*	Fix compilation of runtime system.	xleroy	2013-05-29	1	-0/+4
*	Merge of the float32 branch:	xleroy	2013-05-19	1	-1/+1
*	Preliminary support for debugging info (-g).	xleroy	2013-05-17	1	-0/+1
*	Clean up 'make clean'	xleroy	2013-05-01	1	-2/+1
*	Use "-as" to put CompCert modules in a compcert.xxx namespace.	xleroy	2013-05-01	1	-7/+16
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-11/+8
*	Updated issues with coqchk. See PR#3026 on the Coq bug tracker.	xleroy	2013-04-14	1	-6/+9
*	Assorted changes to reduce stack and heap requirements when compiling very bi...	xleroy	2013-03-16	1	-1/+1
*	Revised Stacking and Asmgen passes and Mach semantics:	xleroy	2013-03-01	1	-4/+3
*	More correct exportclight/ dependencies	xleroy	2013-01-08	1	-2/+2
*	Put clighgen files in exportclight/	xleroy	2013-01-05	1	-7/+10
*	RTLgenaux: heuristic to orient if-then-else statements based on sizes.	xleroy	2012-12-31	1	-2/+4
*	Make "all" the defaut target.	xleroy	2012-12-29	1	-18/+21
*	Merge of the clightgen branch:	xleroy	2012-12-29	1	-2/+11
*	Clight: split off the big step semantics in ClightBigstep.	xleroy	2012-10-14	1	-1/+1
*	Make Clight independent of CompCert C.	xleroy	2012-10-08	1	-1/+1
*	Support for indirect symbols under MacOS X (final).	xleroy	2012-07-14	1	-1/+1
*	Revert unintentional commit #1955	xleroy	2012-07-06	1	-6/+6
*	Ajout trunk CompCert	blazy	2012-07-04	1	-6/+6
*	Use Flocq for floats	xleroy	2012-06-28	1	-2/+14
*	CSE: add recognition of some combined operators, conditions, and addressing m...	xleroy	2012-05-26	1	-1/+1
*	Merge of the newmem branch:	xleroy	2012-05-21	1	-3/+6
*	Configuration, build and install for cchecklink. Clean-ups in myocamlbuild.ml.	xleroy	2012-04-04	1	-1/+7
*	checklink: first import of Valentin Robert's validator for asm and link	xleroy	2012-03-28	1	-4/+18
*	make clean must erase tools/ndfun	xleroy	2012-03-13	1	-0/+1
*	Cosmetic cleanups.	xleroy	2012-01-15	1	-2/+0
*	Merge of the nonstrict-ops branch:	xleroy	2012-01-14	1	-4/+12
*	Changelog, doc: updated for release 1.9v1.9	xleroy	2011-08-22	1	-0/+7
*	New backend pass "RRE": optimize (somewhat) redundant reloads introduced by t...	xleroy	2011-08-16	1	-0/+1
*	ARM codegen ported to new ABI + VFD floats	xleroy	2011-07-30	1	-8/+8
*	Updated Makefile and dependencies. Typo in powerpc/PrintAsm.ml.	xleroy	2011-07-28	1	-2/+1
*	Added animation of the CompCert C semantics (ccomp -interp)	xleroy	2011-07-28	1	-2/+2
*	Merge of branch new-semantics: revised and strengthened top-level statements ...	xleroy	2011-07-15	1	-1/+2
*	Added pass CleanupLabels to remove unreferenced labels in a proved way.	xleroy	2011-05-08	1	-0/+1
*	Renamed Machconcr into Machsem.	xleroy	2011-04-09	1	-1/+1
*	Merge of branch "unsigned-offsets":	xleroy	2011-04-09	1	-2/+2