compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Merge branch 'master' into dwarf	Bernhard Schommer	2015-01-12	1	-21/+33
\|\
\| *	PR#16: give option rules precedence over file pattern rules.	Xavier Leroy	2015-01-03	1	-22/+33
\| *	PR#14: recognize ".so" arguments as files to pass to the linker.	Xavier Leroy	2015-01-02	1	-1/+2
* \|	Renamed the printer module for the Abbreviations and deactivated adding the -...	Bernhard Schommer	2014-12-02	1	-1/+1
\|/
*	Verification of the Unusedglob pass (removal of unreferenced static global de...	Xavier Leroy	2014-11-24	1	-1/+1
*	Add flags to control individual optimization passes + flag -O0 for turning th...	Xavier Leroy	2014-11-16	1	-12/+29
*	Revised parsing of command-line arguments (in preparation for adding more).	Xavier Leroy	2014-11-16	1	-118/+104
*	Removed environment variable for the stdlib_path and added a new variable for...	Bernhard Schommer	2014-10-06	1	-5/+1
*	Moved the timing facility to a seperate file.	Bernhard Schommer	2014-09-29	1	-0/+1
*	Rename "-fthumb" option into "-mthumb" for GCC compatibility.	xleroy	2014-08-19	1	-4/+8
*	Nicer reporting of I/O errors (e.g. "No such file").	xleroy	2014-08-13	1	-23/+26
*	PowerPC port: refactored the expansion of built-in functions and	xleroy	2014-07-28	1	-2/+3
*	ARM port: add support for Thumb2. To be tested.	xleroy	2014-07-27	1	-0/+2
*	Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...	xleroy	2014-04-09	1	-1/+1
*	Merge of branch linear-typing:	xleroy	2014-04-06	1	-0/+2
*	Add option -Os to optimize for code size rather than for execution speed.	xleroy	2014-02-19	1	-0/+4
*	Recognize .i and .p source files as C sources not to be preprocessed.	xleroy	2014-02-05	1	-3/+31
*	- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.	xleroy	2014-01-12	1	-20/+9
*	More tolerance for functions declared without a prototype	xleroy	2013-12-28	1	-3/+5
*	Simpler, more robust emulation of calls to variadic functions:	xleroy	2013-12-28	1	-2/+0
*	Revised parsing of command-line options, more GCC-like.	xleroy	2013-12-21	1	-21/+44
*	Merge of branch value-analysis.	xleroy	2013-12-20	1	-0/+3
*	Rename "-fno-sse" into "-fno-fpu" and honor it on PowerPC as well.	xleroy	2013-11-27	1	-2/+3
*	Compile in debug mode and activate stack backtraces.	xleroy	2013-07-07	1	-0/+1
*	Add option -fno-tailcalls to turn off tailcall elimination (causes problem wi...	xleroy	2013-05-17	1	-0/+2
*	Preliminary support for debugging info (-g).	xleroy	2013-05-17	1	-8/+12
*	driver: removed option -flonglong	xleroy	2013-04-22	1	-4/+2
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-1/+4
*	Updated PowerPC port to new integers.	xleroy	2013-02-12	1	-1/+5
*	Be more like gcc in the way we display or not the usage message.	xleroy	2013-02-12	1	-8/+6
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	1	-3/+4
*	Better treatment of volatile accesses in the reference interpreter.	xleroy	2013-01-08	1	-2/+0
*	Merge of the clightgen branch:	xleroy	2012-12-29	1	-9/+1
*	Support for inline assembly (asm statements).	xleroy	2012-12-18	1	-1/+4
*	Generate output files in current directory; can be overriden with -o option	xleroy	2012-10-08	1	-33/+58
*	Support for indirect symbols under MacOS X (final).	xleroy	2012-07-14	1	-2/+2
*	Added option -falign-functions	xleroy	2012-07-01	1	-0/+2
*	Merge of the newmem branch:	xleroy	2012-05-21	1	-4/+7
*	checklink: first import of Valentin Robert's validator for asm and link	xleroy	2012-03-28	1	-10/+28
*	Option -randvol to expose randomization of volatiles in Interp.ml	xleroy	2012-03-12	1	-0/+2
*	Merge of Andrew Tolmach's HASP-related changes	xleroy	2012-03-09	1	-0/+9
*	PowerPC: remove the fmadd and fmsub operators/Asm instructions	xleroy	2012-03-07	1	-2/+0
*	Added command-line options -Wp,<opt> -Wa,<opt> -Wl,<opt>	xleroy	2012-02-29	1	-2/+16
*	Merge of the "volatile" branch:	xleroy	2012-02-04	1	-12/+5
*	Interp: accommodate "int main(int, char **)".	xleroy	2011-10-19	1	-6/+0
*	Corrected initialization of char arrays by string literals.	xleroy	2011-10-17	1	-1/+3
*	Presimplification SimplVolatile: cleaned up and integrated.	xleroy	2011-08-18	1	-1/+16
*	Added animation of the CompCert C semantics (ccomp -interp)	xleroy	2011-07-28	1	-56/+96
*	cparser: support for attributes over struct and union.	xleroy	2011-05-12	1	-1/+5
*	powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).	xleroy	2011-05-08	1	-8/+41