From b59fd68938a2769d981402d0ff408f9f991b3bb8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?=
<tuong@users.noreply.github.com>
Date: Sat, 23 May 2020 14:16:43 +0100
Subject: [PATCH] report C99 parsing errors
---
src_ext/l4v/src/tools/c-parser/Feedback.ML | 6 ++++++
src_ext/l4v/src/tools/c-parser/StrictCParser.ML | 14 ++++++++++----
src_ext/l4v/src/tools/c-parser/isar_install.ML | 2 +-
3 files changed, 17 insertions(+), 5 deletions(-)
diff --git a/src_ext/l4v/src/tools/c-parser/Feedback.ML b/src_ext/l4v/src/tools/c-parser/Feedback.ML
index 553e37b68..23cf17818 100644
--- a/src_ext/l4v/src/tools/c-parser/Feedback.ML
+++ b/src_ext/l4v/src/tools/c-parser/Feedback.ML
@@ -13,6 +13,9 @@ signature FEEDBACK =
sig
exception WantToExit of string
+
+ val msg_c99 : string
+
val numErrors : int Unsynchronized.ref
val errorThreshold : int option Unsynchronized.ref
val errorStr : Region.t * string -> unit
@@ -35,6 +38,9 @@ structure Feedback :> FEEDBACK =
struct
open Unsynchronized
exception WantToExit of string
+
+val msg_c99 = "C99 parser"
+
val isSome = Option.isSome
val numErrors = ref 0
diff --git a/src_ext/l4v/src/tools/c-parser/StrictCParser.ML b/src_ext/l4v/src/tools/c-parser/StrictCParser.ML
index b8dafec53..dd9c81f49 100644
--- a/src_ext/l4v/src/tools/c-parser/StrictCParser.ML
+++ b/src_ext/l4v/src/tools/c-parser/StrictCParser.ML
@@ -63,7 +63,7 @@ fun parse maybe_c11 docpp0 error_lookahead (includes : string list) (input : inp
| (_, Source src) =>
f (drain [Input.source_content src |> #1]) (C_Env.encode_positions [Input.pos_of src])
- fun parse_without_c11 thy =
+ fun parse_without_c11 exit_err thy =
docpp
(open_close (fn istream => fn fname =>
let
@@ -71,8 +71,14 @@ fun parse maybe_c11 docpp0 error_lookahead (includes : string list) (input : inp
val lexarg = StrictCLex.UserDeclarations.new_state fname
val lexer = StrictCParser.makeLexer istream lexarg
val pos = #source lexarg
+ fun err e =
+ tap (fn _ =>
+ (writeln (Markup.markup (Markup.bad ()) (Feedback.msg_c99 ^ ": " ^ "returning a default empty parsed value"));
+ exit_err (Feedback.msg_c99 ^ ": " ^ @{make_string} e ^ Position.here \<^here>)))
+ ([], !Feedback.numErrors)
in (invoke error_lookahead pos lexer
- handle StrictCParser.ParseError => ([], !Feedback.numErrors))
+ handle e as StrictCParser.ParseError => err e
+ | e as Feedback.WantToExit _ => err e)
|>> pair fname
end))
|>> (fn (fname, v) => Synchronized.change_result last_parsed (K (v, (fname, v))))
@@ -119,7 +125,7 @@ fun parse maybe_c11 docpp0 error_lookahead (includes : string list) (input : inp
case maybe_c11 of
SOME true =>
let val ((res2, err2), thy) = parse_with_c11 thy
- val ((res1, err1), thy) = parse_without_c11 thy
+ val ((res1, err1), thy) = parse_without_c11 warning thy
val rm = StmtDecl.rm_region_ext_decl_list
val r1 = rm res1
val r2 = rm res2
@@ -134,7 +140,7 @@ fun parse maybe_c11 docpp0 error_lookahead (includes : string list) (input : inp
r1 r2 (0, true))
then ((res1, err1 + err2), thy)
else error "Parsed values are not similar." end
- | SOME false => parse_without_c11 thy
+ | SOME false => parse_without_c11 error thy
| _ => parse_with_c11 thy
end
diff --git a/src_ext/l4v/src/tools/c-parser/isar_install.ML b/src_ext/l4v/src/tools/c-parser/isar_install.ML
index 8200f1bd9..3c4be8ced 100644
--- a/src_ext/l4v/src/tools/c-parser/isar_install.ML
+++ b/src_ext/l4v/src/tools/c-parser/isar_install.ML
@@ -55,7 +55,7 @@ fun setup_feedback extra_output_filename = let
NONE => (fn _ => fn f => f)
| SOME _ => (fn pfx => fn f => fn s => (trace_extra (pfx ^ s); f s))
in
- Feedback.errorf := add_extra "ERROR: " (writeln o Markup.markup (Markup.bad ()));
+ Feedback.errorf := add_extra "ERROR: " (writeln o Markup.markup (Markup.bad ()) o (fn s => Feedback.msg_c99 ^ ": " ^ s));
Feedback.warnf := add_extra "" warning;
Feedback.informf := add_extra "" (Output.tracing o Feedback.timestamp)
end
--
GitLab