diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml index e5c2f208daa0da69b050079e2917b19e417fc40d..2061e23ca869ac84660f0ba2704e5bca279fe7a2 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 c9a7358f4566c0270e4791daa63e7ad53f418c22..d4ceba5f88073c917826a5eb07b90656b8b795a3 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