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 /cparser/ErrorReports.mli | |
parent | 8d1a15f7f5c8fbea194a67c49c5aa10d6371b267 (diff) | |
download | compcert-kvx-f8be3f5f2937b053b9cb75ada7937a6c1b20f019.tar.gz compcert-kvx-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 'cparser/ErrorReports.mli')
-rw-r--r-- | cparser/ErrorReports.mli | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/cparser/ErrorReports.mli b/cparser/ErrorReports.mli new file mode 100644 index 00000000..e4296e69 --- /dev/null +++ b/cparser/ErrorReports.mli @@ -0,0 +1,28 @@ +(* This module is in charge of reporting a syntax error after the pre_parser + has failed. *) + +open Pre_parser.MenhirInterpreter + +(* The parser keeps track of the last two tokens in a two-place buffer. *) + +type 'a buffer = +| Zero +| One of 'a +| Two of 'a * (* most recent: *) 'a + +(* [push buffer x] pushes [x] into [buffer], causing the buffer to slide. *) + +val update: 'a buffer -> 'a -> 'a buffer + +(* [report text buffer checkpoint] constructs an error message. The C source + code must be stored in the string [text]. The start and end positions of the + last two tokens that were read must be stored in [buffer]. The parser state + (i.e., the automaton's state and stack) must be recorded in the checkpoint + [checkpoint]. *) + +val report: + string -> + (Lexing.position * Lexing.position) buffer -> + _ checkpoint -> + string + |