From 1ac80ff1d74c17066be01e0029996bf19a0bbc44 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 15 Nov 2019 09:54:37 +0100
Subject: [PATCH] [logic] fix error handling in extensions
Don't treat as fatal internal error of the extension exceptions that are
raised as part of the standard error mechanism provided by the typing context.
---
src/kernel_services/ast_queries/logic_typing.ml | 9 +++++++--
1 file changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 5920671ad02..9a4e7782568 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -544,11 +544,16 @@ module Extensions = struct
with Not_found ->
Kernel.fatal ~source:(fst loc) "unsupported clause of name '%s'" name
in
+ let normal_error = ref false in
+ let has_error () = normal_error := true in
+ let wrapper =
+ typing_context.on_error (typer ~typing_context ~loc) has_error
+ in
try
- status, typer ~typing_context ~loc p
+ status, wrapper p
with
| (Log.AbortError _ | Log.AbortFatal _) as exn -> raise exn
- | exn ->
+ | exn when not !normal_error ->
Kernel.fatal "Typechecking ACSL extension %s raised exception %s"
name (Printexc.to_string exn)
end
--
GitLab