compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	For uniformity with other messages, added an "Ill-formed expression.".	François Pottier	2015-11-24	1	-0/+1
\|
*	Update of the auto-generated comments.	François Pottier	2015-11-24	1	-610/+611
\|
*	A simplification in the grammar, leading to fewer states in the automaton	François Pottier	2015-11-24	1	-13/+1
\| \| \| \|	and merging two error states into one. There should be no observable change.
*	Fix a typo in a syntax error message.	François Pottier	2015-11-23	1	-1/+1
\|
*	Typo, coherence in error messages	Jacques-Henri Jourdan	2015-11-07	1	-4/+4
\|
*	Integrate a few comments of F. Pottier into the pre_parser and ↵	Jacques-Henri Jourdan	2015-11-07	1	-131/+99
\| \| \| \|	handcrafted.messages
*	Merge remote-tracking branch 'origin/master' into parser_fix	Jacques-Henri Jourdan	2015-11-04	1	-1876/+1406
\|
*	Fixed some comments.	François Pottier	2015-10-28	1	-16/+16
\|
*	Fixed one error message and removed two comments.	François Pottier	2015-10-26	1	-5/+1
\|
*	Added copyright banners to the new files.	François Pottier	2015-10-23	1	-0/+12
\|
*	Install the new system for reporting syntax errors.	François Pottier	2015-10-23	1	-0/+5162
	This requires the development version of Menhir, to be released soon. In summary: handcrafted.messages is new. It contains a mapping of erroneous sentences to error messages, together with a lot of comments. Makefile.extr is new. It contains a rule to generate cparser/pre_parser_messages.ml based on this mapping. cparser/ErrorReports.{ml,mli} are new. They construct syntax error messages, based on the compiled mapping. cparser/Lexer.mll is modified. The last two tokens that have been read are stored in a buffer. ErrorReports is called to construct a syntax error message. cparser/GNUmakefile is new. It offers several commands for working on the pre-parser. cparser/deLexer.ml is new. It is a script (it is not linked into CompCert). It translates the symbolic name of a token to an example of this token in concrete C syntax. It is used by [make -C cparser concrete] to produce the .c files in tests/generated/. cparser/tests/generated/Makefile is new. It runs ccomp, clang and gcc on each of the generated C files, so as to allow a comparison of the error messages.