compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Resynchronize the LICENSE file and the license headers in individual files (#45)	Xavier Leroy	2018-01-05	1	-0/+3
\| \| \| \| \| \| \| \| \| \| \|	Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent. This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed. Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, /extractionMachdep.v Moved lib/Json to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST which is not in lib/
*	Updated handcrafted.messages for __builtin_offsetof	Bernhard Schommer	2017-02-01	1	-753/+858
\|
*	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.