From febcb9bc2554a96c2edd529bd45d1a21f8aa1564 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 28 Jul 2023 19:59:39 +0200
Subject: [PATCH] Update script to catch errors instead of fatals
---
tests/spec/extend_extern.ml | 2 +-
tests/spec/oracle/extend_extern.res.oracle | 4 ++++
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
index e5c2f208daa..2061e23ca86 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -25,7 +25,7 @@ let main () =
"Checking handler of exception occurring in extension typing";
Ast.compute (); assert false
with
- | Log.AbortFatal _ -> Kernel.feedback "Extension typing failed as expected"
+ | Log.AbortError _ -> 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"
diff --git a/tests/spec/oracle/extend_extern.res.oracle b/tests/spec/oracle/extend_extern.res.oracle
index c9a7358f456..d4ceba5f880 100644
--- a/tests/spec/oracle/extend_extern.res.oracle
+++ b/tests/spec/oracle/extend_extern.res.oracle
@@ -1,4 +1,8 @@
[kernel] Checking handler of exception occurring in extension typing
[kernel] Parsing extend_extern.i (no preprocessing)
[kernel] Failure: Typechecking ACSL extension why3 raised exception Not_found
+[kernel:annot-error] extend_extern.i:6: Warning:
+ Logic typing error. Ignoring global annotation
+[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] User Error: stopping on file "extend_extern.i" that has errors.
[kernel] Extension typing failed as expected
--
GitLab