From e7cdfd97ade293bf3ea568b156fa17f282d05ede Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 8 Nov 2019 15:29:29 +0100
Subject: [PATCH] [tests] simplify test
- no 3d party module dependency
- don't have a stack dump as oracle
---
tests/spec/extend_extern.i | 1 -
tests/spec/extend_extern.ml | 15 ++++++++++++---
tests/spec/oracle/extend_extern.res.oracle | 3 +++
3 files changed, 15 insertions(+), 4 deletions(-)
create mode 100644 tests/spec/oracle/extend_extern.res.oracle
diff --git a/tests/spec/extend_extern.i b/tests/spec/extend_extern.i
index 8dffe226177..c3c61836044 100644
--- a/tests/spec/extend_extern.i
+++ b/tests/spec/extend_extern.i
@@ -1,5 +1,4 @@
/* run.config
- MACRO: PTEST_MAKE_MODULE make FRAMAC_USER_OFLAGS="-package why3" FRAMAC_USER_BFLAGS="-package why3"
MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
OPT:
*/
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
index 70f1ad660c2..66629497432 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -3,9 +3,7 @@ open Cil_types
let load_theory = function
| { pred_content = Papp (_, [], [ { term_node = TConst(LStr _name) } ] ) } ->
- let open Why3 in ignore (
- Theory.import_namespace Theory.empty_ns [_name]
- )
+ raise Not_found
| _ -> assert false
let typing ~typing_context ~loc lexprs =
@@ -20,3 +18,14 @@ let typing ~typing_context ~loc lexprs =
let () =
Logic_typing.register_global_extension "why3" false typing
+
+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"
+
+let () = Kernel.TypeCheck.set false
+
+let () = Db.Main.extend main
diff --git a/tests/spec/oracle/extend_extern.res.oracle b/tests/spec/oracle/extend_extern.res.oracle
new file mode 100644
index 00000000000..a5e2e92faf2
--- /dev/null
+++ b/tests/spec/oracle/extend_extern.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Checking handler of exception occurring in extension typing
+[kernel] Parsing tests/spec/extend_extern.i (no preprocessing)
+[kernel] Extension typing failed as expected
--
GitLab