compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Removed the version from the compcert.ini file and add it again in a ↵	Bernhard Schommer	2015-07-01	1	-2/+0
\| \| \| \|	separate file.
*	Provide and use compiler-dependent standard headers.	Xavier Leroy	2015-04-25	1	-0/+2
\| \| \| \| \| \| \| \| \| \| \| \|	This branch provides implementations of the following standard headers: <float.h> <stdarg.h> <stdbool.h> <stddef.h> <varargs.h> These are the headers that are provided by GCC and Clang, as opposed to being provided by Glibc and similar C standard libraries. Configuration flag "-no-standard-headers" deactivates the installation and use of these headers. Lightly tested so far (IA32 Linux).
*	Merge branch 'master' into dwarf	Bernhard Schommer	2015-03-31	1	-0/+2
\| \| \| \| \| \|	Conflicts: Makefile driver/Driver.ml
*	Improvements in the StructReturn transformation (ABI conformance for passing ↵	Xavier Leroy	2015-03-20	1	-0/+55
	composites). - Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD. - Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions. - More comprehensive interoperability test in regression/interop1.c.