diff options
| author | François Pottier <francois.pottier@inria.fr> | 2015-10-23 13:34:43 +0200 |
|---|---|---|
| committer | François Pottier <francois.pottier@inria.fr> | 2015-10-23 13:40:40 +0200 |
| commit | f8be3f5f2937b053b9cb75ada7937a6c1b20f019 (patch) | |
| tree | 23b4cc1187762f0b956a4109b11fd0736da67e85 /Makefile.extr | |
| parent | 8d1a15f7f5c8fbea194a67c49c5aa10d6371b267 (diff) | |
| download | compcert-f8be3f5f2937b053b9cb75ada7937a6c1b20f019.tar.gz compcert-f8be3f5f2937b053b9cb75ada7937a6c1b20f019.zip | |
Install the new system for reporting syntax errors.
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.
Diffstat (limited to 'Makefile.extr')
| -rw-r--r-- | Makefile.extr | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/Makefile.extr b/Makefile.extr index 6a03f1e1..fce0d933 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -17,10 +17,15 @@ include Makefile.config -# Menhir configuration and rules. +# Menhir configuration. include Makefile.menhir +# The pre-parser's error message database is compiled as follows. + +cparser/pre_parser_messages.ml: + $(MAKE) -C cparser correct + # Directories containing plain Caml code (no preprocessing) DIRS=extraction \ @@ -87,7 +92,7 @@ LIBS_BYTE=$(patsubst %.cmxa,%.cma,$(patsubst %.cmx,%.cmo,$(LIBS))) CHECKLINK_LIBS=str.cmxa EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte -GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml) +GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml) cparser/pre_parser_messages.ml # Beginning of part that assumes .depend.extr already exists |