compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Added the _Noreturn keyword.	Bernhard Schommer	2016-03-23	1	-1/+1
\| \| \| \| \| \| \| \|	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
*	Merge remote-tracking branch 'origin/master' into parser_fix	Jacques-Henri Jourdan	2015-11-04	1	-2/+2
\|\
\| *	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-2/+2
\| \|
* \|	Better handling of old-style K&R function declarations:	Jacques-Henri Jourdan	2015-11-01	1	-9/+1
\|/ \| \| \| \| \|	- Added a Cabs.PROTO_OLD constructor to Cabs.decl_type - Refactored the Parser.vy and pre_parser.mly grammars - Rewritten the conversion of old function definitions to new-style
*	Experiment: support a subset of GCC's extended asm statements.	Xavier Leroy	2015-04-17	1	-1/+1
\|
*	Assorted fixes to fix parsing issues and be more GCC-like:	xleroy	2014-05-12	1	-1/+1
\| \| \| \| \| \| \| \| \| \|	- Moved scanning of char constants and string literals entirely to Lexer - Parser: separate STRING_LITERAL from CONSTANT to be closer to ISO C99 grammar - pre_parser: adapted + "asm" takes string_literal, not CONSTANT - Revised errors "inline doesnt belong here" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2492 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Incorrect conversion of K&R functions. Example of problem:	xleroy	2014-05-12	1	-0/+7
\| \| \| \| \| \| \|	void * foo(s, u) ... git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2491 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support for old-style K&R function definitions.	xleroy	2014-05-05	1	-0/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2478 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Integration of Jacques-Henri Jourdan's verified parser.	xleroy	2014-04-29	1	-51/+4
\| \| \| \| \| \| \|	(Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of ↵	xleroy	2010-09-01	1	-1/+1
\| \| \| \| \| \|	reading a small unsigned bitfield git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1496 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Switching to the new C parser/elaborator/simplifier	xleroy	2010-03-03	1	-0/+126
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e