From 9a473c43ff1b758adccae2d95aa5d62c64adf00e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 15 Nov 2019 08:48:44 +0100
Subject: [PATCH] [logic] more precise error message when typing extension
raises an exn
---
src/kernel_services/ast_queries/logic_typing.ml | 8 +++++++-
tests/spec/extend_extern.ml | 9 +++++++--
tests/spec/oracle/extend_extern.res.oracle | 1 +
3 files changed, 15 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index f855e465650..5920671ad02 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -544,7 +544,13 @@ module Extensions = struct
with Not_found ->
Kernel.fatal ~source:(fst loc) "unsupported clause of name '%s'" name
in
- status, typer ~typing_context ~loc p
+ try
+ status, typer ~typing_context ~loc p
+ with
+ | (Log.AbortError _ | Log.AbortFatal _) as exn -> raise exn
+ | exn ->
+ Kernel.fatal "Typechecking ACSL extension %s raised exception %s"
+ name (Printexc.to_string exn)
end
let register_behavior_extension name f =
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
index 66629497432..c60a714b9bf 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -23,9 +23,14 @@ let main () =
try
Kernel.feedback
"Checking handler of exception occurring in extension typing";
- Ast.compute (); Kernel.fatal "Extension typing should have failed"
- with Not_found -> Kernel.feedback "Extension typing failed as expected"
+ Ast.compute (); assert false
+ with
+ | Log.AbortFatal _ -> Kernel.feedback "Extension typing failed as expected"
+ | Not_found -> Kernel.fatal "kernel did not capture our exception"
+ | Assert_failure _ -> Kernel.fatal "kernel silently captured our exception"
let () = Kernel.TypeCheck.set false
+let () = Kernel.Debug.set 1
+
let () = Db.Main.extend main
diff --git a/tests/spec/oracle/extend_extern.res.oracle b/tests/spec/oracle/extend_extern.res.oracle
index a5e2e92faf2..3b7533295bb 100644
--- a/tests/spec/oracle/extend_extern.res.oracle
+++ b/tests/spec/oracle/extend_extern.res.oracle
@@ -1,3 +1,4 @@
[kernel] Checking handler of exception occurring in extension typing
[kernel] Parsing tests/spec/extend_extern.i (no preprocessing)
+[kernel] Failure: Typechecking ACSL extension why3 raised exception Not_found
[kernel] Extension typing failed as expected
--
GitLab