compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge remote branch 'upstream/master' into clean	François Pottier	2015-10-23	1	-2/+0
\|\ \| \| \| \| \| \| \| \|	Conflicts: Makefile.extr
\| *	We can ignore the generated automation. Bug 17392	Bernhard Schommer	2015-10-12	1	-0/+1
\| \|
\| *	Removal of cchecklink, superseded by AbsInt's Valex tool.	Xavier Leroy	2015-10-12	1	-2/+0
\| \|
* \|	Install the new system for reporting syntax errors.	François Pottier	2015-10-23	1	-0/+7
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
* \|	A .gitignore entry.	François Pottier	2015-10-23	1	-0/+1
\| \|
* \|	Pass --no-stdlib and -v to menhir when compiling pre_parser.mly.	François Pottier	2015-10-07	1	-0/+1
\|/ \| \| \| \| \| \|	Passing --no-stdlib ensures that there is no dependency on Menhir's standard library. Passing -v, which is equivalent to --explain --dump, requests the generation of pre_parser.automaton, a description of the automaton.
*	Added Build, Tag, etc in version string and driver/Version.ml should be ignored	Bernhard Schommer	2015-07-01	1	-1/+1
\|
*	Added a small ocamlfile that calls ocamlfind recursivly over a given directory.	Bernhard Schommer	2015-02-24	1	-0/+1
\|
*	cparser/Parser.v is generated.	Xavier Leroy	2014-12-30	1	-0/+1
\|
*	Replace ocamlbuild by a second-stage makefile to compile the OCaml code and ↵	Xavier Leroy	2014-11-22	1	-2/+9
\| \| \| \| \| \|	produce the executables. configure: add check for GNU make.
*	Change the way the tools like the linker, assembler, etc. are specified by ↵	Bernhard Schommer	2014-09-30	1	-1/+1
\| \| \| \|	including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
*	Add .gitignore files.	Xavier Leroy	2014-09-21	1	-0/+40