[tests] simplify test

- no 3d party module dependency
- don't have a stack dump as oracle

tests/spec/extend_extern.i

 /* run.config
-   MACRO: PTEST_MAKE_MODULE make FRAMAC_USER_OFLAGS="-package why3" FRAMAC_USER_BFLAGS="-package why3"
    MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT:
  */

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

tests/spec/oracle/extend_extern.res.oracle

+[kernel] Checking handler of exception occurring in extension typing
+[kernel] Parsing tests/spec/extend_extern.i (no preprocessing)
+[kernel] Extension typing failed as expected