compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Added iso646 header for alternate spellings.	Bernhard Schommer	2016-04-06	1	-0/+49
\| \| \| \| \| \| \|	The iso646 header defines some macros that expand to common operators. Both clang and gcc ship with them and they are required by the standard. Bug 18645.
*	Added the _Noreturn keyword.	Bernhard Schommer	2016-03-23	2	-0/+80
\| \| \| \| \| \| \| \|	CompCert now recognizes the C11 _Noreturn function specifier and emits a simple warning for functions declared _Noreturn containing a return statement. Also the stdnoreturn header and additionally the stdalign header are added. Bug 18541
*	Include fix for wint_t gcc problem.	Bernhard Schommer	2016-01-21	1	-12/+16
\| \| \| \| \| \|	Gcc defines wint_t in the stddef header (even if it is not stanadard) and additionally defines it if stddef is reincluded. The fix now defines it before stddef is checked for reinclusion.
*	More gcc/newlib compatibility code.	Bernhard Schommer	2015-12-11	1	-2/+13
\| \| \| \| \| \| \| \| \| \|	Some newlib headers use the __extension__ keyword which suppresses warnings for gcc extensions in strict mode. CompCert now ignores this keyword for the gnu backends. Also it seems that stddef of the gcc defines wint_t even though it should not. However some libs rely on this. So wint_t is now defined in CompCert's stddef header. Bug 17613.
*	Also test if the __VA_LIST macro is defined to avoid problems with the ↵	Bernhard Schommer	2015-07-09	1	-2/+8
\| \| \| \|	typedefs in stdio, etc. for the diab compiler.
*	Removed brackets around ty in macro of offestof.	Bernhard Schommer	2015-07-07	1	-1/+1
\|
*	Diab defines w_char to be unsigned short.	Bernhard Schommer	2015-07-07	1	-1/+1
\|
*	Better define the __GNUC__ macro which avoids the inclusion of va_list ↵	Bernhard Schommer	2015-07-07	1	-0/+4
\| \| \| \|	header and set the __VA_LIST macro if it is not defined.
*	Make also the wchar definition diab compatible.	Bernhard Schommer	2015-06-26	1	-0/+15
\|
*	Added diab specific macros for stddef to avoid redefinition of size_t.	Bernhard Schommer	2015-06-26	1	-0/+9
\|
*	Typo in #ifndef guard.	Xavier Leroy	2015-05-09	1	-1/+1
\|
*	Improve compatibility with MacOS X.	Xavier Leroy	2015-04-26	1	-0/+3
\|
*	Provide and use compiler-dependent standard headers.	Xavier Leroy	2015-04-25	5	-0/+298
	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).