From f8be3f5f2937b053b9cb75ada7937a6c1b20f019 Mon Sep 17 00:00:00 2001
From: François Pottier <francois.pottier@inria.fr>
Date: Fri, 23 Oct 2015 13:34:43 +0200
Subject: 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.
---
 cparser/ErrorReports.mli | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 cparser/ErrorReports.mli

(limited to 'cparser/ErrorReports.mli')

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
+
-- 
cgit