diff --git a/.Makefile.lint b/.Makefile.lint
index 6feefd8e7db75131a329db0cf888e456e877942b..0d06aec2a52cabd62013b44313fc1ec5de6f4143 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -6,8 +6,6 @@ ML_LINT_KO+=src/kernel_internals/parsing/lexerhack.ml
 ML_LINT_KO+=src/kernel_internals/parsing/logic_preprocess.mli
 ML_LINT_KO+=src/kernel_internals/runtime/boot.ml
 ML_LINT_KO+=src/kernel_internals/runtime/machdeps.ml
-ML_LINT_KO+=src/kernel_internals/runtime/messages.ml
-ML_LINT_KO+=src/kernel_internals/runtime/messages.mli
 ML_LINT_KO+=src/kernel_internals/runtime/special_hooks.ml
 ML_LINT_KO+=src/kernel_internals/typing/allocates.ml
 ML_LINT_KO+=src/kernel_internals/typing/frontc.mli
diff --git a/Changelog b/Changelog
index 1fc3c4520e359bda43eb2add1037d0e2e7e2abc7..d5124640269c6be51f50f492718d84d487814ac3 100644
--- a/Changelog
+++ b/Changelog
@@ -24,6 +24,7 @@ Open Source Release <next-release>
               transition, and use such variables in subsequent guards.
 -   Kernel    [2020-10-09] Add option -print-config-json, to output Frama-C
               configuration data in JSON format.
+-   Logic     [2020-10-XX] '\from' now accepts '&v' expressions
 -   Metrics   [2020-10-01] Distinguish between undefined but specified functions
               and functions with neither definition nor specification.
 -*  Eva       [2020-09-28] Improved string builtins on wide strings: crash fixed,
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 3b7ec0011a82cccbe8d9d79a2839679608d3ef69..300b449ff1e5e07979e205ce37a16e2552ee48b3 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1462,6 +1462,8 @@ src/plugins/variadic/va_build.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/variadic/va_types.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/wp/.gitignore: .ignore
 src/plugins/wp/.ocp-indent: .ignore
+src/plugins/wp/AssignsCompleteness.ml: CEA_WP
+src/plugins/wp/AssignsCompleteness.mli: CEA_WP
 src/plugins/wp/Auto.ml: CEA_WP
 src/plugins/wp/Auto.mli: CEA_WP
 src/plugins/wp/Cache.ml: CEA_WP
@@ -1820,6 +1822,8 @@ src/plugins/wp/wpRTE.ml: CEA_WP
 src/plugins/wp/wpRTE.mli: CEA_WP
 src/plugins/wp/wpStrategy.ml: CEA_WP
 src/plugins/wp/wpStrategy.mli: CEA_WP
+src/plugins/wp/wpTarget.ml: CEA_WP
+src/plugins/wp/wpTarget.mli: CEA_WP
 src/plugins/wp/wp_error.ml: CEA_WP
 src/plugins/wp/wp_error.mli: CEA_WP
 src/plugins/wp/wp_parameters.ml: CEA_WP
diff --git a/src/kernel_internals/runtime/messages.ml b/src/kernel_internals/runtime/messages.ml
index 30ad09ac69fb87b4d9ca6288d1e21358efde9ae8..2f4cffa49367a7dd56c1652b158f4c3100c96fef 100644
--- a/src/kernel_internals/runtime/messages.ml
+++ b/src/kernel_internals/runtime/messages.ml
@@ -23,51 +23,53 @@
 module DatatypeMessages =
   Datatype.Make_with_collections
     (struct
-       include Datatype.Serializable_undefined
-       open Log
-       type t = event
-       let name = "message"
-       let reprs =
-         [ { evt_kind = Failure;
-             evt_plugin = "";
-             evt_category = None;
-             evt_source = None;
-             evt_message = "" } ]
-       let mem_project = Datatype.never_any_project
-       let hash (e: event)= Hashtbl.hash e
-       let compare (e1: event) e2 = Extlib.compare_basic e1 e2
-       let equal = Datatype.from_compare
-     end)
+      include Datatype.Serializable_undefined
+      open Log
+      type t = event
+      let name = "message"
+      let reprs =
+        [ { evt_kind = Failure;
+            evt_plugin = "";
+            evt_category = None;
+            evt_source = None;
+            evt_message = "" } ]
+      let mem_project = Datatype.never_any_project
+      let hash (e: event)= Hashtbl.hash e
+      let compare (e1: event) e2 = Extlib.compare_basic e1 e2
+      let equal = Datatype.from_compare
+    end)
 
 module Messages =
   State_builder.List_ref
     (DatatypeMessages)
     (struct
-       let name = "Messages.message_table"
-       let dependencies = [ Ast.self ]
-     end)
+      let name = "Messages.message_table"
+      let dependencies = [ Ast.self ]
+    end)
 let () = Ast.add_monotonic_state Messages.self
 
+let hooks = ref []
 let add_message m =
-  Messages.set (m :: Messages.get ());;
+  begin
+    Messages.set (m :: Messages.get ()) ;
+    List.iter (fun fn -> fn()) !hooks ;
+  end
 
 let nb_errors () =
-  let n = ref 0 in
-  Messages.iter (fun e ->
-      match e.Log.evt_kind with
-      | Log.Error -> incr n
-      | _ -> ());
-  !n
+  Messages.fold_left
+    (fun n e ->
+       match e.Log.evt_kind with
+       | Log.Error -> succ n
+       | _ -> n) 0
 
 let nb_warnings () =
-  let n = ref 0 in
-  Messages.iter (fun e ->
-      match e.Log.evt_kind with
-      | Log.Warning -> incr n
-      | _ -> ());
-  !n
+  Messages.fold_left
+    (fun n e ->
+       match e.Log.evt_kind with
+       | Log.Warning -> succ n
+       | _ -> n) 0
 
-let nb_messages() = nb_errors() + nb_warnings();;
+let nb_messages() = List.length (Messages.get ())
 
 let self = Messages.self
 
@@ -75,10 +77,9 @@ let iter f = List.iter f (List.rev (Messages.get ()))
 let dump_messages () = iter Log.echo
 
 let () =
-  Log.add_listener ~kind:[ Log.Error; Log.Warning ] add_message;
-;;
+  Log.add_listener ~kind:[ Log.Error; Log.Warning ] add_message
 
-module OnceTable = 
+module OnceTable =
   State_builder.Hashtbl
     (DatatypeMessages.Hashtbl)
     (Datatype.Unit)
@@ -86,12 +87,12 @@ module OnceTable =
       let size = 37
       let dependencies = [ Ast.self ]
       let name = "Messages.OnceTable"
-     end)
+    end)
 
 let check_not_yet evt =
   if OnceTable.mem evt then false
   else begin
-    OnceTable.add evt (); 
+    OnceTable.add evt ();
     true
   end
 
@@ -99,6 +100,7 @@ let () = Log.check_not_yet := check_not_yet
 
 let reset_once_flag () = OnceTable.clear ()
 
+let add_global_hook fn = hooks := !hooks @ [fn]
 
 (*
 Local Variables:
diff --git a/src/kernel_internals/runtime/messages.mli b/src/kernel_internals/runtime/messages.mli
index c78dec23b50e5a21ff0f5dbb5c919d5b264d1bf6..11f26cc5bf12d49304fa30a01e87d592f44d3c21 100644
--- a/src/kernel_internals/runtime/messages.mli
+++ b/src/kernel_internals/runtime/messages.mli
@@ -24,19 +24,19 @@
     Currently, only warning and error messages are stored. *)
 
 val iter: (Log.event -> unit) -> unit
-  (** Iter over all stored messages. The messages are passed in emission order.
-      @modify Nitrogen-20111001  Messages are now passed in emission order. *)
+(** Iter over all stored messages. The messages are passed in emission order.
+    @modify Nitrogen-20111001  Messages are now passed in emission order. *)
 
 val dump_messages: unit -> unit
-  (** Dump stored messages to standard channels *)
+(** Dump stored messages to standard channels *)
 
 val self: State.t
-  (** Internal state of stored messages *)
+(** Internal state of stored messages *)
 
 val reset_once_flag : unit -> unit
-  (** Reset the [once] flag of pretty-printers. Messages already printed
-      will be printed again.
-      @since Boron-20100401 *)
+(** Reset the [once] flag of pretty-printers. Messages already printed
+    will be printed again.
+    @since Boron-20100401 *)
 
 val nb_errors: unit -> int
 val nb_warnings: unit -> int
@@ -44,6 +44,9 @@ val nb_messages: unit -> int
 (** Number of stored warning messages, error messages, or all
     messages.*)
 
+val add_global_hook: (unit -> unit) -> unit
+(** Register a global hook (not projectified) on message addition. *)
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 86129401b2122b383b0ef430311205fb8317452d..477044c55237b2a176287a24d50381468bf41ab8 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -2308,14 +2308,18 @@ struct
       accept_array: bool;
       accept_models: bool;
       accept_func_ptr: bool;
+      accept_addrs: bool;
     }
 
   let lval_addressable_mode =
     { accept_empty = false; accept_formal = true; accept_array = true;
-      accept_models = false; accept_func_ptr = true; }
+      accept_models = false; accept_func_ptr = true; accept_addrs = false;}
   let lval_assignable_mode =
     { accept_empty = true; accept_formal = true; accept_array = false;
-      accept_models = true; accept_func_ptr = false; }
+      accept_models = true; accept_func_ptr = false; accept_addrs = false;}
+  let lval_assigns_dependency_mode =
+    { accept_empty = true; accept_formal = true; accept_array = false;
+      accept_models = true; accept_func_ptr = false; accept_addrs = true;}
 
   let is_fct_ptr lv = Cil.isLogicFunctionType (Cil.typeOfTermLval lv)
 
@@ -2341,7 +2345,15 @@ struct
         (match snd (Logic_utils.remove_term_offset loff) with
          | TModel _ -> m.accept_models
          | _ -> true)
-      | TAddrOf lv -> is_fct_ptr lv && m.accept_func_ptr
+      | TAddrOf lv when is_fct_ptr lv -> m.accept_func_ptr
+      | TAddrOf lv | TStartOf lv ->
+        m.accept_addrs &&
+        (* note that we assume that 'lv' is adressable. *)
+        begin match lv with
+          | TVar { lv_origin = Some _ }, _ | TMem _, _ -> true
+          | TVar { lv_origin = None }, _ -> false
+          | _ -> false
+        end
       | Tif (_,t1,t2) -> aux t1 && aux t2
 
       | Tunion l | Tinter l -> List.for_all aux l
@@ -2351,7 +2363,7 @@ struct
 
       | Trange _ | TConst _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
       | TAlignOfE _ | TUnOp (_,_) | TBinOp (_,_,_) | TCastE (_,_)
-      | TStartOf _ | Tlambda (_,_) | TDataCons (_,_) | Tbase_addr (_,_)
+      | Tlambda (_,_) | TDataCons (_,_) | Tbase_addr (_,_)
       | Toffset (_,_) | Tblock_length (_,_) | Tnull | Tapp _
       | TUpdate (_,_,_) | Ttypeof _ | Ttype _ ->
         false
@@ -3109,6 +3121,27 @@ struct
     in
     lift_set check_lval t
 
+  and term_from f t =
+    let check_from t =
+      match t.term_node with
+      | TAddrOf lv when is_fun_ptr t.term_type ->
+        f lv
+          { t with
+            term_type = type_of_pointed t.term_type;
+            term_node = TLval lv }
+      | TLval lv
+      | TLogic_coerce(_,{term_node = TLval lv })
+      | Tat({term_node = TLval lv},_) -> f lv t
+      | TStartOf lv
+      | Tat ({term_node = TStartOf lv}, _)
+      | TAddrOf lv
+      | Tat ({term_node = TAddrOf lv}, _) ->
+        f lv t
+      | _ -> C.error t.term_loc "not a dependency value: %a"
+               Cil_printer.pp_term t
+    in
+    lift_set check_from t
+
   and type_logic_app env loc f labels ttl =
     (* support for overloading *)
     let infos =
@@ -3448,6 +3481,14 @@ struct
     | PLcomprehension _ | PLset _ | PLunion _ | PLinter _ | PLempty ->
       ctxt.error loc "expecting a predicate and not tsets"
 
+  let term_as_dependency ctxt env t =
+    let module [@warning "-60"] C = struct end in
+    let t = ctxt.type_term ctxt env t in
+    if not (check_lval_kind lval_assigns_dependency_mode t) then
+      ctxt.error t.term_loc "not a valid dependency: %a"
+        Cil_printer.pp_term t ;
+    lift_set (term_from (fun _ t -> t)) t
+
   let type_from ctxt ~accept_formal env (l,d) =
     let module [@warning "-60"] C = struct end in
     (* Yannick: [assigns *\at(\result,Post)] should be allowed *)
@@ -3459,7 +3500,7 @@ struct
       FromAny -> (tl,Cil_types.FromAny)
     | From f ->
       let tf =
-        List.map (term_lval_assignable ctxt ~accept_formal:true env) f
+        List.map (term_as_dependency ctxt env) f
       in
       let tf =
         List.map
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 87952f24f7043431e9b988db6ef9adf56d9e74e3..03048c9f2ac6615d73ab14862524f039a2609021 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1708,14 +1708,24 @@ class main_window () : main_window_extension_points =
         in
         Warning_manager.make ~packing ~callback
       in
+      let outdated_warnings = ref false in
       let display_warnings () =
-        Messages.reset_once_flag ();
+        outdated_warnings := false ;
         Warning_manager.clear warning_manager;
         Messages.iter (fun event -> Warning_manager.append warning_manager event);
         let text = Format.sprintf "Messages (%d)" (Messages.nb_messages ()) in
         let label = GtkMisc.Label.cast warnings_tab_label#as_widget in
         GtkMisc.Label.set_text label text
       in
+      register_reset_extension (fun _ -> display_warnings ());
+      Messages.add_global_hook (fun () ->
+          if not !outdated_warnings then
+            begin
+              outdated_warnings := true ;
+              Wutil.later display_warnings
+            end
+        );
+      Messages.reset_once_flag ();
       display_warnings ();
 
       (* Management of navigation history *)
@@ -1728,7 +1738,6 @@ class main_window () : main_window_extension_points =
             self#scroll l
         );
 
-      register_reset_extension (fun _ -> display_warnings ());
       self#default_screen ();
       menu_manager#refresh ();
       Project.register_after_set_current_hook
diff --git a/src/plugins/wp/AssignsCompleteness.ml b/src/plugins/wp/AssignsCompleteness.ml
new file mode 100644
index 0000000000000000000000000000000000000000..25db9a6e85e9a6a4157343361a9aaeca4d4a7ffe
--- /dev/null
+++ b/src/plugins/wp/AssignsCompleteness.ml
@@ -0,0 +1,166 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+module Completeness = struct
+  module KfParam = struct
+    include Cil_datatype.Kf
+    let label = None
+  end
+
+  module Data =
+    Datatype.Pair
+      (Datatype.Bool)
+      (Datatype.Function(KfParam)(Datatype.Unit))
+
+  include State_builder.Hashtbl
+      (Cil_datatype.Kf.Hashtbl)
+      (Data)
+      (struct
+        let name = "RefUsage.AssignsCompleteness.Callbacks"
+        let size = 17
+        let dependencies = [ Ast.self ]
+      end)
+end
+
+exception Incomplete_assigns of (string list * string)
+
+let wkey_pedantic = Wp_parameters.register_warn_category "pedantic-assigns"
+
+type ('a, 'b) result = Ok of 'a | Error of 'b
+
+let collect_assigns kf =
+  let opt_try f p = function None -> f p | Some x -> Some x in
+  let fold_assigns bhv =
+    let folder _ a acc = match a, acc with
+      | WritesAny, _ -> None
+      | _, None      -> Some a
+      | _, Some acc  -> Some (Logic_utils.concat_assigns acc a)
+    in
+    Annotations.fold_assigns folder kf bhv None
+  in
+  let find_default () =
+    match fold_assigns Cil.default_behavior_name with
+    | None -> None
+    | Some x -> Some [x]
+  in
+  let incompletes = ref [] in
+  let find_complete () =
+    let fold_behaviors names =
+      let folder l name = match (fold_assigns name) with
+        | None -> raise (Incomplete_assigns(names, name))
+        | Some a -> a :: l
+      in
+      try Some (List.fold_left folder [] names)
+      with Incomplete_assigns(bhv_l,b) ->
+        incompletes := (bhv_l, b) :: !incompletes ;
+        None
+    in
+    Annotations.fold_complete (fun _ -> opt_try fold_behaviors) kf None
+  in
+  (* First:
+     - try to find default behavior assigns, if we cannot get it
+     - try to find a "complete behaviors" set where each behavior has assigns
+       As assigns and froms are over-approximations, the result (if it exists)
+       must cover all assigned memory locations and all data dependencies.
+  *)
+  match opt_try find_complete () (opt_try find_default () None) with
+  | None -> Error !incompletes
+  | Some r -> Ok r
+
+let pretty_behaviors_errors fmt l =
+  let pp_complete =
+    Pretty_utils.pp_list ~pre:"{" ~suf:"}" ~sep:", " Format.pp_print_string
+  in
+  let pp_bhv_error fmt (bhv_l, name) =
+    Format.fprintf fmt
+      "- in complete behaviors: %a@\n  No assigns for (at least) '%s'@\n"
+      pp_complete bhv_l name
+  in
+  match l with
+  | [] -> Format.fprintf fmt ""
+  | l -> Format.fprintf fmt "%a" (Pretty_utils.pp_list pp_bhv_error) l
+
+let check_assigns kf assigns =
+  let complete = (true, fun _ -> ()) in
+  let incomplete (_status, current) warning =
+    let new_warning kf =
+      current kf ;
+      warning kf ;
+    in
+    (false, new_warning)
+  in
+  let vassigns acc a =
+    let res_t = Kernel_function.get_return_type kf in
+    let assigns_result ({ it_content=t }, _) = Logic_utils.is_result t in
+    let froms = match a with WritesAny -> [] | Writes l -> l in
+    let acc =
+      if Cil.isPointerType res_t && not (List.exists assigns_result froms) then
+        incomplete acc
+          begin fun kf ->
+            Wp_parameters.warning ~wkey:wkey_pedantic
+              ~once:true ~source:(fst (Kernel_function.get_location kf))
+              "No 'assigns \\result \\from ...' specification for function '%a'\
+               returning pointer type.@ Callers assumptions might be imprecise."
+              Kernel_function.pretty kf ;
+          end
+      else acc
+    in
+    let vfrom acc = function
+      | t, FromAny when Logic_typing.is_pointer_type t.it_content.term_type ->
+          incomplete acc
+            begin fun _kf ->
+              Wp_parameters.warning ~wkey:wkey_pedantic
+                ~once:true ~source:(fst t.it_content.term_loc)
+                "No \\from specification for assigned pointer '%a'.@ \
+                 Callers assumptions might be imprecise."
+                Cil_printer.pp_identified_term t
+            end
+      | _ -> acc
+    in List.fold_left vfrom acc froms
+  in
+  match assigns with
+  | Error l ->
+      false,
+      begin fun kf ->
+        Wp_parameters.warning ~wkey:wkey_pedantic
+          ~once:true ~source:(fst (Kernel_function.get_location kf))
+          "No 'assigns' specification for function '%a'.@\n%a\
+           Callers assumptions might be imprecise."
+          Kernel_function.pretty kf
+          pretty_behaviors_errors l
+      end
+  | Ok l ->
+      List.fold_left vassigns complete l
+
+let memo_compute kf =
+  Completeness.memo (fun kf -> check_assigns kf (collect_assigns kf)) kf
+
+let compute kf =
+  ignore (memo_compute kf)
+
+let is_complete kf =
+  fst(memo_compute kf)
+
+let warn kf =
+  snd(memo_compute kf) kf
diff --git a/src/plugins/wp/AssignsCompleteness.mli b/src/plugins/wp/AssignsCompleteness.mli
new file mode 100644
index 0000000000000000000000000000000000000000..8fa55bec1d546c61fddd6cdd9e6a7bc65c2ee968
--- /dev/null
+++ b/src/plugins/wp/AssignsCompleteness.mli
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** This module is used to check the assigns specification of a given function
+    so that if it is not precise enough to enable precise memory models
+    hypotheses computation, the assigns specification is considered incomplete.
+
+    All these functions are memoized.
+*)
+
+val compute: Kernel_function.t -> unit
+
+val is_complete: Kernel_function.t -> bool
+
+val warn: Kernel_function.t -> unit
+(** Displays a warning if the given kernel function has incomplete assigns.
+    Note that the warning is configured with [~once] set to [true]. *)
+
+val wkey_pedantic: Wp_parameters.warn_category
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 1d4b72ae09a86bbf27afc874ced772974131b7d5..d73bf64f1e432e3afe23b30cd12b7a0ad7ea1fc5 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,12 +24,18 @@
 Plugin WP <next-release>
 #########################
 
+- WP          [2020-10-14] New warning "pedantic-assigns". WP needs precise
+                           'assigns ... \from ...' specification about out
+                           pointers (\result and assigned pointers) to generate
+                           precise proof hypotheses.
+- WP          [2020-10-14] Hypotheses: out pointers (\result + written pointers)
 - WP          [2020-10-07] New tactic Bit-Test range
 - WP          [2020-09-21] Added support for Why3 interactive prover (Coq)
+- WP          [2020-09-21] Added support for Why3 Coq interactive prover
 - WP          [2020-09-21] New option -wp-interactive <mode>
 - WP          [2020-09-21] New option -wp-interactive-timeout <seconds>
-- WP          [2020-09-17] New experimental option: -wp-check-model-hypotheses
-                           Generates requires in contracts for model hypotheses
+- WP          [2020-09-17] New experimental option: -wp-check-memory-model
+                           Insert function contracts for model hypotheses
 - WP          [2020-09-17] Hypotheses: assigned memory locations
 - WP          [2020-09-11] Support for generalized @check ACSL annotations
 - WP          [2020-07-06] Removed debug keys "no-xxx-info" (subsumed by "shell")
diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index b24a0ca165b0113a6afb5761142d6c86f4eb22f2..320b6ed8d9d8b5cede3955092bc39d4e63381c2e 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/src/plugins/wp/GuiPanel.ml
@@ -63,11 +63,45 @@ let wp_rte_generated s =
         not mem
       else false
 
+let with_model action kf =
+  let setup = Factory.parse (Wp_parameters.Model.get ()) in
+  let driver = Driver.load_driver () in
+  let model = Factory.instance setup driver in
+  let hypotheses_computer = WpContext.compute_hypotheses model in
+  let name = WpContext.MODEL.id model in
+  action kf name hypotheses_computer
+
+let warn_memory_context kfs =
+  if Wp_parameters.MemoryContext.get () then begin
+    Kernel_function.Set.iter
+      (fun kf -> with_model MemoryContext.warn kf) kfs
+  end
+
+let populate_memory_context kfs =
+  if Wp_parameters.CheckMemoryContext.get () then begin
+    Kernel_function.Set.iter
+      (fun kf -> with_model MemoryContext.add_behavior kf) kfs
+  end
+
 let spawn provers vcs =
   if not (Bag.is_empty vcs) then
     let provers = Why3.Whyconf.Sprover.elements provers#get in
     VC.command ~provers ~tip:true vcs
 
+let treat_hypotheses selection =
+  let kf = match selection with
+    | S_none -> None
+    | S_fun kf -> Some kf
+    | S_prop ip -> Property.get_kf ip
+    | S_call s -> Some (Kernel_function.find_englobing_kf s.s_stmt)
+  in
+  let kfs = match kf with
+    | Some kf -> WpTarget.with_callees kf
+    | None -> Kernel_function.Set.empty
+  in
+  warn_memory_context kfs ;
+  populate_memory_context kfs
+
 let run_and_prove
     (main:Design.main_window_extension_points)
     (provers:GuiConfig.provers)
@@ -76,6 +110,7 @@ let run_and_prove
   begin
     try
       begin
+        treat_hypotheses selection ;
         match selection with
         | S_none -> raise Stop
         | S_fun kf -> spawn provers (VC.generate_kf kf)
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 66988554f5200215e975871247122df3ef43c8be..5264a1b2cfd1fc5cfc5cab6614f82a2bb023c86c 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -63,7 +63,7 @@ PLUGIN_CMO:= \
 	wp_parameters wp_error \
 	dyncall ctypes clabels \
 	Why3Provers \
-	Context Warning MemoryContext wpContext \
+	Context Warning AssignsCompleteness MemoryContext wpContext \
 	LogicUsage RefUsage \
 	Layout Region \
 	RegionAnnot RegionAccess RegionDump RegionAnalysis \
@@ -81,7 +81,7 @@ PLUGIN_CMO:= \
 	Sigma MemLoader \
 	MemEmpty MemZeroAlias MemVar \
 	MemMemory MemTyped MemRegion \
-	wpReached wpRTE wpAnnot \
+	wpReached wpRTE wpAnnot wpTarget \
 	CfgCompiler StmtSemantics \
 	VCS script proof wpo wpReport \
 	Footprint Tactical Strategy \
@@ -234,7 +234,7 @@ WP_API_BASE= \
 	LogicUsage.mli RefUsage.mli \
 	normAtLabels.mli \
 	wpPropId.mli mcfg.ml \
-	Context.mli Warning.mli wpContext.mli \
+	Context.mli Warning.mli AssignsCompleteness.mli wpContext.mli \
 	Lang.mli Repr.mli Passive.mli Splitter.mli \
 	LogicBuiltins.mli Definitions.mli \
 	Cint.mli Cfloat.mli Vset.mli Cstring.mli \
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index b3012f74718fa77cdc0ff4d8e6c73e9ec2b5f40e..b9074b52fab472f4d6611bd53490b8a1f4bc573a 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -50,6 +50,7 @@ type partition = {
   globals : zone list ; (* [ &G , G[...], ... ] *)
   to_heap : zone list ; (* [ p, ... ] *)
   context : zone list ; (* [ p+(..), ... ] *)
+  by_addr : zone list ; (* [ &(x + ..), ... ] *)
 }
 
 (* -------------------------------------------------------------------------- *)
@@ -60,12 +61,13 @@ let empty = {
   globals = [] ;
   context = [] ;
   to_heap = [] ;
+  by_addr = [] ;
 }
 
 let set x p w =
   match p with
   | NotUsed -> w
-  | ByAddr -> w
+  | ByAddr -> { w with by_addr = Var x :: w.by_addr }
   | ByRef | InContext ->
       if Cil.isFunctionType x.vtype then w else
         { w with context = Ptr x :: w.context }
@@ -85,12 +87,11 @@ let set x p w =
       else w
 
 (* -------------------------------------------------------------------------- *)
-(* ANNOTS                                                                     *)
+(* --- Building Annotations                                               --- *)
 (* -------------------------------------------------------------------------- *)
 
 open Logic_const
 
-
 let rec ptr_of = function
   | Ctype t -> Ctype (TPtr(t, []))
   | t when Logic_typing.is_set_type t ->
@@ -186,20 +187,19 @@ let valid_region loc r =
   let t = region_to_term loc r in
   pvalid ~loc (here_label, t)
 
-let global_zones partition =
-  List.map (fun z -> [z]) partition.globals
+let simplify ps =
+  List.sort_uniq Logic_utils.compare_predicate
+    (List.filter (fun p -> not(Logic_utils.is_trivially_true p)) ps)
 
-let context_zones partition =
-  List.map (fun z -> [z]) partition.context
+let ptrset { term_type = t } =
+  let open Logic_typing in
+  is_pointer_type t || (is_set_type t && is_pointer_type (type_of_element t))
 
-let heap_zones partition =
-  let comp a b = Cil_datatype.Typ.compare (type_of_zone a) (type_of_zone b) in
-  List.sort comp partition.to_heap
+(* -------------------------------------------------------------------------- *)
+(* --- Partition Helpers                                                  --- *)
+(* -------------------------------------------------------------------------- *)
 
-(* Note that this function does not return separated zone lists, but well-typed
-   zone lists.
-*)
-let heaps partition =
+let welltyped zones =
   let rec partition_by_type t acc l =
     match l, acc with
     | [], _ ->
@@ -211,8 +211,24 @@ let heaps partition =
     | x :: l, acc ->
         partition_by_type (type_of_zone x) ([x] :: acc) l
   in
-  partition_by_type Cil.voidType [] (heap_zones partition)
+  let compare_zone a b =
+    Cil_datatype.Typ.compare (type_of_zone a) (type_of_zone b) in
+  partition_by_type Cil.voidType [] (List.sort compare_zone zones)
+
+let global_zones partition =
+  List.map (fun z -> [z]) partition.globals
+
+let context_zones partition =
+  List.map (fun z -> [z]) partition.context
 
+let heaps partition = welltyped partition.to_heap
+let addr_of_vars partition = welltyped partition.by_addr
+
+(* -------------------------------------------------------------------------- *)
+(* --- Computing Separation                                               --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* Memory regions shall be separated with each others *)
 let main_separation loc globals context heaps =
   match heaps, context with
   | [], [] ->
@@ -228,21 +244,18 @@ let main_separation loc globals context heaps =
       in
       List.map for_typed_heap heaps
 
+(* Filter assigns *)
 let assigned_locations kf filter =
   let add_from l (e, _ds) =
     if filter e.it_content then e :: l else l
   in
-  let add_assign kf _emitter assigns l = match assigns with
-    | WritesAny ->
-        Wp_parameters.warning
-          ~wkey:Wp_parameters.wkey_imprecise_hypotheses_assigns ~once:true
-          "No assigns for function '%a', model hypotheses will be imprecise"
-          Kernel_function.pretty kf ;
-        l
+  let add_assign _emitter assigns l = match assigns with
+    | WritesAny -> l
     | Writes froms -> List.fold_left add_from l froms
   in
-  Annotations.fold_assigns (add_assign kf) kf Cil.default_behavior_name []
+  Annotations.fold_assigns add_assign kf Cil.default_behavior_name []
 
+(* Locations assigned by pointer from a call *)
 let assigned_via_pointers kf =
   let rec assigned_via_pointer t =
     match t.term_node with
@@ -260,24 +273,94 @@ let assigned_via_pointers kf =
   in
   assigned_locations kf assigned_via_pointer
 
+(* Checks whether a term refers to Post *)
+let post_term t =
+  let exception Post_value in
+  let v = object
+    inherit Cil.nopCilVisitor
+    method! vlogic_label = function
+      | BuiltinLabel Post -> raise Post_value
+      | _ -> Cil.SkipChildren
+    method! vterm_lval = function
+      | TResult _, _ -> raise Post_value
+      | _ -> Cil.DoChildren
+  end in
+  try ignore (Cil.visitCilTerm v t) ; false
+  with Post_value -> true
+
+(* Computes conditions from call assigns *)
+let assigned_separation kf loc globals =
+  let addr_of t = addr_of_lval ~loc t.it_content in
+  let asgnd_ptrs = List.map addr_of (assigned_via_pointers kf) in
+  let folder (req, ens) t =
+    let sep = term_separated_from_regions loc t globals in
+    if post_term t then (req, sep :: ens) else (sep :: req, ens)
+  in
+  List.fold_left folder ([],[]) asgnd_ptrs
+
+(* Computes conditions from partition *)
 let clauses_of_partition kf loc p =
   let globals = global_zones p in
-  let main_sep =
-    main_separation loc globals (context_zones p) (heaps p)
+  let main_sep = main_separation loc globals (context_zones p) (heaps p) in
+  let assigns_sep_req, assigns_sep_ens = assigned_separation kf loc globals in
+  let context_validity = List.map (valid_region loc) (context_zones p) in
+  let reqs = main_sep @ assigns_sep_req @ context_validity in
+  let reqs = simplify reqs in
+  let ens = simplify assigns_sep_ens in
+  reqs, ens
+
+(* Computes conditions from return *)
+let out_pointers_separation kf loc p =
+  let ret_t = Kernel_function.get_return_type kf in
+  let addr_of t = addr_of_lval ~loc t.it_content in
+  let asgnd_ptrs =
+    Extlib.filter_map
+      (* Search assigned pointers via a pointer,
+         e.g. 'assigns *p ;' with '*p' of type pointer or set of pointers *)
+      (fun t -> ptrset t.it_content) addr_of (assigned_via_pointers kf)
+  in
+  let asgnd_ptrs =
+    if Cil.isPointerType ret_t then tresult ~loc ret_t :: asgnd_ptrs
+    else asgnd_ptrs
   in
-  let assigns_sep =
-    let addr_of t = addr_of_lval ~loc t.it_content in
-    List.map
-      (fun t -> term_separated_from_regions loc (addr_of t) globals)
-      (assigned_via_pointers kf)
+  let formals_separation =
+    let formal_zone = function Var v -> v.vformal | _ -> false in
+    let formal_partition =
+      { p with by_addr = List.filter formal_zone p.by_addr }
+    in
+    let formals = addr_of_vars formal_partition in
+    List.map (fun t -> term_separated_from_regions loc t formals) asgnd_ptrs
   in
-  let context_validity =
-    List.map (valid_region loc) (context_zones p)
+  let globals_separation =
+    let globals = global_zones p in
+    List.map (fun t -> term_separated_from_regions loc t globals) asgnd_ptrs
   in
-  let reqs = main_sep @ assigns_sep @ context_validity in
-  let reqs = List.filter (fun p -> not(Logic_utils.is_trivially_true p)) reqs in
-  let reqs = List.sort_uniq Logic_utils.compare_predicate reqs in
-  reqs
+  simplify (formals_separation @ globals_separation)
+
+(* Computes all conditions from behavior *)
+let compute_behavior kf name hypotheses_computer =
+  let partition = hypotheses_computer kf in
+  let loc = Kernel_function.get_location kf in
+  let reqs, ens = clauses_of_partition kf loc partition in
+  let ens = out_pointers_separation kf loc partition @ ens in
+  let reqs = List.map new_predicate reqs in
+  let ens = List.map (fun p -> Normal, new_predicate p) ens in
+  match reqs, ens with
+  | [], [] -> None
+  | reqs, ens ->
+      Some {
+        b_name = Annotations.fresh_behavior_name kf ("wp_" ^  name) ;
+        b_requires = reqs ;
+        b_assumes = [] ;
+        b_post_cond = ens ;
+        b_assigns = WritesAny ;
+        b_allocation = FreeAllocAny ;
+        b_extended = []
+      }
+
+(* -------------------------------------------------------------------------- *)
+(* --- Memoization                                                        --- *)
+(* -------------------------------------------------------------------------- *)
 
 module Table =
   State_builder.Hashtbl
@@ -289,35 +372,61 @@ module Table =
       let dependencies = [ Ast.self ]
     end)
 
-let compute_behavior kf name hypotheses_computer =
-  let partition = hypotheses_computer kf in
-  let loc = Kernel_function.get_location kf in
-  let reqs = clauses_of_partition kf loc partition in
-  let reqs = List.map Logic_const.new_predicate reqs in
-  match reqs with
-  | [] -> None
-  | l1 ->
-      Some {
-        b_name = name ;
-        b_requires = l1 ;
-        b_assumes = [] ;
-        b_post_cond = [] ;
-        b_assigns = WritesAny ;
-        b_allocation = FreeAllocAny ;
-        b_extended = []
-      }
+module RegisteredHypotheses =
+  State_builder.Set_ref
+    (Cil_datatype.Kf.Set)
+    (struct
+      let name = "Wp.MemoryContext.RegisteredHypotheses"
+      let dependencies = [Ast.self]
+    end)
 
 let compute name hypotheses_computer =
   Globals.Functions.iter
     (fun kf -> ignore (compute_behavior kf name hypotheses_computer))
 
 let get_behavior kf name hypotheses_computer =
-  Table.memo (fun kf -> compute_behavior kf name hypotheses_computer) kf
+  Table.memo
+    begin fun kf ->
+      AssignsCompleteness.warn kf ;
+      compute_behavior kf name hypotheses_computer
+    end
+    kf
+
+(* -------------------------------------------------------------------------- *)
+(* --- External API                                                       --- *)
+(* -------------------------------------------------------------------------- *)
+
+let print_memory_context kf bhv fmt =
+  begin
+    let printer = new Printer.extensible_printer () in
+    let pp_vdecl = printer#without_annot printer#vdecl in
+    Format.fprintf fmt "@[<hv 0>@[<hv 3>/*@@@ %a" Cil_printer.pp_behavior bhv ;
+    let vkf = Kernel_function.get_vi kf in
+    Format.fprintf fmt "@ @]*/@]@\n@[<hov 2>%a;@]@\n"
+      pp_vdecl vkf ;
+  end
+
+let warn kf name hyp_computer =
+  match get_behavior kf name hyp_computer with
+  | None -> ()
+  | Some bhv ->
+      Wp_parameters.warning
+        ~current:false ~once:true ~source:(fst(Kernel_function.get_location kf))
+        "@[<hv 0>Memory model hypotheses for function '%s':@ %t@]"
+        (Kernel_function.get_name kf)
+        (print_memory_context kf bhv)
 
 let emitter =
   Emitter.(create "Wp.Hypotheses" [Funspec] ~correctness:[] ~tuning:[])
 
 let add_behavior kf name hypotheses_computer =
-  match get_behavior kf name hypotheses_computer with
-  | None -> ()
-  | Some bhv -> Annotations.add_behaviors emitter kf [bhv]
+  if RegisteredHypotheses.mem kf then ()
+  else begin
+    begin match get_behavior kf name hypotheses_computer with
+      | None -> ()
+      | Some bhv -> Annotations.add_behaviors emitter kf [bhv]
+    end ;
+    RegisteredHypotheses.add kf
+  end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemoryContext.mli b/src/plugins/wp/MemoryContext.mli
index 736617995ed81cf7f7ad010849e1349f9c689712..95cb1638ff8af641e39d534643fb16147dea8a44 100644
--- a/src/plugins/wp/MemoryContext.mli
+++ b/src/plugins/wp/MemoryContext.mli
@@ -35,5 +35,5 @@ val compute: string -> (kernel_function -> partition) -> unit
 
 val add_behavior:
   kernel_function -> string -> (kernel_function -> partition) -> unit
-val get_behavior:
-  kernel_function -> string -> (kernel_function -> partition) -> behavior option
+val warn:
+  kernel_function -> string -> (kernel_function -> partition) -> unit
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index df5426a001849e0295a5b148dd9bf4b25e12069a..a6c0564503dce968927047a94e514f5fc6ae08c7 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -673,6 +673,7 @@ let cfun_spec env kf =
     method !vpredicate p = update_spec_env (pred env p)
     method !vterm t = update_spec_env (vterm env t)
   end in
+  AssignsCompleteness.compute kf ;
   let spec = Annotations.funspec kf in
   ignore (Cil.visitCilFunspec (visitor:>Cil.cilVisitor) spec) ;
   (* Partitioning the accesses of the spec for formals vs globals *)
diff --git a/src/plugins/wp/doc/manual/wp_caveat.tex b/src/plugins/wp/doc/manual/wp_caveat.tex
index 9223f9d67dfc742606487b15eeb708de80f8c8d7..6e7afa77c066bb52273da98252d093d08b6980f3 100644
--- a/src/plugins/wp/doc/manual/wp_caveat.tex
+++ b/src/plugins/wp/doc/manual/wp_caveat.tex
@@ -34,5 +34,5 @@ the user \emph{must} check by manual code review that no aliases are
 introduced \emph{via} pointers passed to formal parameters at call sites.
 
 However, \textsf{WP} warns about the implicit separation hypotheses required by
-the memory model \textit{via} the \texttt{-wp-warn-separation} option, set
+the memory model \textit{via} the \texttt{-wp-warn-memory-model} option, set
 by default.
diff --git a/src/plugins/wp/doc/manual/wp_logic.tex b/src/plugins/wp/doc/manual/wp_logic.tex
index fb06118205256554f6819989501e20158840cbff..83218a58bcd0beba00723c50f67ee54e7cab2308 100644
--- a/src/plugins/wp/doc/manual/wp_logic.tex
+++ b/src/plugins/wp/doc/manual/wp_logic.tex
@@ -178,3 +178,49 @@ detected variables are then assigned to the Hoare memory model.
 
 This optimization is not activated by default, since the non-aliasing
 assumptions at call sites are sometimes irrelevant.
+
+\section{Mixed models hypotheses}
+\label{wp-model-hypotheses}
+
+For the previously presented \textsf{Ref} model, but also for the
+\textsf{Typed}, and \textsf{Caveat} models presented later, WP lists
+the separation and validity hypotheses associated to the choice that
+it make of dispatching each pointer and variable either to the
+\lstinline{Hoare} or to the model $\cal{M}$ used for the heap.
+
+Thus, in addition to user-defined function \lstinline{requires}, WP
+also states as \lstinline{requires} that:
+
+\begin{itemize}
+\item \lstinline{Hoare} variables are separated from each other,
+\item \lstinline{Hoare} variables are separated from the locations in $\cal{M}$,
+\item references are valid memory locations,
+\item locations assigned via a pointer are separated from \lstinline{Hoare}
+  variables whose address is not taken by the function (including via
+  its contract).
+\end{itemize}
+
+Furthermore, the function must ensure that:
+
+\begin{itemize}
+\item locations assigned via a pointer (including returned value when
+  it is a pointer) are separated from \lstinline{Hoare} variables whose address
+  is not taken by the function (including via its contract),
+\item pointers assigned by the function (including returned value when
+  it is a pointer) are separated from function parameters and \lstinline{Hoare}
+  variables whose address is not taken by the function (including via
+  its contract).
+\end{itemize}
+
+In order to precisely generate these hypotheses, WP needs precise
+\lstinline{assigns} specification. In particular each function under
+verification and all its callees needs an \lstinline{assigns} specification.
+Furthermore, if the function assigns or returns a pointer, WP needs
+a correct \lstinline{\from} specification. If the specification is
+incomplete, a warning \lstinline{wp:pedantic-assigns} is triggered.
+Note that WP does not verify that the \lstinline{\from} is correct.
+
+The hypotheses are displayed when the option
+\lstinline{-wp-warn-memory-model} is enable (it is enabled by default).
+They can be verified by WP using the experimental option
+\lstinline{-wp-check-memory-model}.
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index baabcb0c126a097e691c2abfbb2b0f1457321b4e..d72e45d025b283b8c21b9b21886431de6233473e 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -823,10 +823,17 @@ The available \textsf{WP} command-line options related to model selection are:
   makes the \textsf{WP} emitting a warning on each volatile access.
 \item[\tt -wp-(no)-warn-memory-model] this option (de)activate the
   warnings about memory model hypotheses
-  for the generated proof obligations. For each model supporting this feature, and each concerned function,
+  for the generated proof obligations, as described in Section~\ref{wp-model-hypotheses}.
+  For each model supporting this feature, and each concerned function,
   an \textsf{ACSL} specification is printed on output.
   Currently, only the \texttt{Caveat}, \texttt{Typed} and \texttt{Ref} memory models support
-  this feature.
+  this feature. See also experimental option below.
+\item[\tt -wp-(no)-check-memory-model] this \emph{experimental} option generates
+  ACSL contracts for the selected memory model hypotheses, as described
+  in Section~\ref{wp-model-hypotheses} and listed by option
+  \texttt{-wp-warn-memory-model}.
+  Hence, the memory model hypothes are exposed to \textsf{WP} and other plugins.
+  Disabled by default.
 \end{description}
 
 \subsection{Computation Strategy}
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 24cd69441d0aa7e9539bc8bd179110417be6178a..206b3d7609d9d16496e2d701dc64c5dabf1ea3e0 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -89,42 +89,24 @@ let wp_iter_model ?ip ?index job =
     Fmap.iter (fun kf ms -> Models.iter (fun m -> job kf m) ms) !pool
   end
 
-let wp_print_memory_context kf bhv fmt =
-  begin
-    let printer = new Printer.extensible_printer () in
-    let pp_vdecl = printer#without_annot printer#vdecl in
-    Format.fprintf fmt "@[<hv 0>@[<hv 3>/*@@@ %a" Cil_printer.pp_behavior bhv ;
-    let vkf = Kernel_function.get_vi kf in
-    Format.fprintf fmt "@ @]*/@]@\n@[<hov 2>%a;@]@\n"
-      pp_vdecl vkf ;
-  end
-
 let wp_compute_memory_context model =
   let hypotheses_computer = WpContext.compute_hypotheses model in
   let name = WpContext.MODEL.id model in
   MemoryContext.compute name hypotheses_computer
 
-let wp_warn_memory_context () =
+let wp_warn_memory_context model =
   begin
-    wp_iter_model
-      begin fun kf m ->
-        let hypotheses_computer = WpContext.compute_hypotheses m in
-        let model = WpContext.MODEL.id m in
-        let hyp = MemoryContext.get_behavior kf model hypotheses_computer in
-        match hyp with
-        | None -> ()
-        | Some bhv ->
-            Wp_parameters.warning
-              ~current:false
-              "@[<hv 0>Memory model hypotheses for function '%s':@ %t@]"
-              (Kernel_function.get_name kf)
-              (wp_print_memory_context kf bhv)
+    WpTarget.iter
+      begin fun kf ->
+        let hypotheses_computer = WpContext.compute_hypotheses model in
+        let model = WpContext.MODEL.id model in
+        MemoryContext.warn kf model hypotheses_computer
       end
   end
 
 let wp_insert_memory_context model =
   begin
-    Wp_parameters.iter_fct
+    WpTarget.iter
       begin fun kf ->
         let hyp_computer = WpContext.compute_hypotheses model in
         let model_id = WpContext.MODEL.id model in
@@ -157,7 +139,7 @@ let do_wp_print_for goals =
     else Log.print_on_output
         (fun fmt -> Bag.iter (Wpo.pp_goal_flow fmt) goals)
 
-let do_wp_report () =
+let do_wp_report model =
   begin
     let reports = Wp_parameters.Report.get () in
     let jreport = Wp_parameters.ReportJson.get () in
@@ -177,7 +159,7 @@ let do_wp_report () =
         List.iter (WpReport.export stats) reports ;
       end ;
     if Wp_parameters.MemoryContext.get () then
-      wp_warn_memory_context ()
+      wp_warn_memory_context model
   end
 
 (* ------------------------------------------------------------------------ *)
@@ -766,8 +748,11 @@ let cmdline_run () =
     if fct <> Wp_parameters.Fct_none then
       begin
         Wp_parameters.feedback ~ontty:`Feedback "Running WP plugin...";
+        let computer = computer () in
         Ast.compute ();
         Dyncall.compute ();
+        if Wp_parameters.RTE.get () then
+          WpRTE.generate_all computer#model ;
         if Wp_parameters.has_dkey dkey_logicusage then
           begin
             LogicUsage.compute ();
@@ -781,15 +766,15 @@ let cmdline_run () =
         let bhv = Wp_parameters.Behaviors.get () in
         let prop = Wp_parameters.Properties.get () in
         (** TODO entry point *)
-        let computer = computer () in
         if Wp_parameters.has_dkey dkey_builtins then
           begin
             WpContext.on_context (computer#model,WpContext.Global)
               LogicBuiltins.dump ();
           end ;
+        WpTarget.compute computer#model ;
         wp_compute_memory_context computer#model ;
-        if Wp_parameters.CheckModelHypotheses.get () then
-          wp_insert_memory_context computer#model fct ;
+        if Wp_parameters.CheckMemoryContext.get () then
+          wp_insert_memory_context computer#model ;
         let goals = Generator.compute_selection computer ~fct ~bhv ~prop () in
         do_wp_proofs goals ;
         begin
@@ -798,7 +783,7 @@ let cmdline_run () =
           else
             do_wp_print () ;
         end ;
-        do_wp_report () ;
+        do_wp_report computer#model ;
       end
   end
 
diff --git a/src/plugins/wp/tests/test_config b/src/plugins/wp/tests/test_config
index ebf3f27c26f9ec910cfdb25e281a6141d841198d..51675fdbc52d819cf3c99c4480b3130bd0fa64f3 100644
--- a/src/plugins/wp/tests/test_config
+++ b/src/plugins/wp/tests/test_config
@@ -1,2 +1,2 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-prover none -wp-print -wp-share ./share -wp-msg-key shell
+CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-prover none -wp-print -wp-share ./share -wp-msg-key shell -wp-warn-key "pedantic-assigns=inactive"
 OPT:
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 82ac23797226aae576338c46106f95e16f40b717..f5f56f99251f2a4100444ab7bb74b0abc2128e07 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,2 +1,2 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
+CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
 OPT:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
index b8ebbadea5ebd5ac1be8e37f157226b201709da2..c9a28cfb2ae210a0e5e3161fef820e7c1f8ff088 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
@@ -97,7 +97,8 @@ Effect at line 20
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
-  /*@ behavior typed:
+[wp] tests/wp_acsl/assigns_path.i:12: Warning: 
+  Memory model hypotheses for function 'job':
+  /*@ behavior wp_typed:
         requires \separated(b + (..), &p); */
   void job(int n, int *b);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index f318abf289fadf2fa603a1f23a2c77466a989011..e9965d8c184b6a34ceb012ba529c0bce3040c5ca 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
@@ -1876,9 +1876,10 @@ Goal Positivity of Loop variant at loop (file tests/wp_acsl/chunk_typing.i, line
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'function':
+[wp] tests/wp_acsl/chunk_typing.i:21: Warning: 
+  Memory model hypotheses for function 'function':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated(i16 + (..), (char const *)x + (..));
        requires \separated(i32 + (..), (char const *)x + (..));
        requires \separated(i64 + (..), (char const *)x + (..));
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
index 2c16374dc4ab5dda44513eea004949b6fed2b4f0..a6492896347e183c19f0db5379accd1e4c56183e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
@@ -140,3 +140,18 @@ Goal Loop assigns 'qed_ok':
 Prove: true.
 
 ------------------------------------------------------------
+[wp] tests/wp_acsl/funvar_inv.i:26: Warning: 
+  Memory model hypotheses for function 'f':
+  /*@ behavior wp_hoare:
+        ensures \separated(\result, (int *)G + (..)); */
+  int *f(void);
+[wp] tests/wp_acsl/funvar_inv.i:40: Warning: 
+  Memory model hypotheses for function 'f2':
+  /*@ behavior wp_hoare:
+        ensures \separated(\result, (int *)G + (..)); */
+  int *f2(void);
+[wp] tests/wp_acsl/funvar_inv.i:55: Warning: 
+  Memory model hypotheses for function 'g':
+  /*@ behavior wp_hoare:
+        ensures \separated(\result, (int *)G + (..)); */
+  int *g(void);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
index 4339266bbaf17b0b122e18a85903f672b452e038..e261e262d4301be01fe9cddb106761c86a568653 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
@@ -234,11 +234,13 @@ Goal Post-condition 'qed_ko,Eq_oracle_ko' in 'pointer':
 Prove: false.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'compare':
-  /*@ behavior typed:
+[wp] tests/wp_acsl/pointer.i:63: Warning: 
+  Memory model hypotheses for function 'compare':
+  /*@ behavior wp_typed:
         requires \separated(q + (..), &p); */
   void compare(int *q);
-[wp] Warning: Memory model hypotheses for function 'absurd':
-  /*@ behavior typed:
+[wp] tests/wp_acsl/pointer.i:73: Warning: 
+  Memory model hypotheses for function 'absurd':
+  /*@ behavior wp_typed:
         requires \separated(q + (..), &p); */
   void absurd(int *q);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
index 180d946c3170c9be3b7dfdaa9a4df4820f951158..44a78cfe5015b349177603e2c6ae694393fea054 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
@@ -19,7 +19,8 @@
  Functions                 WP     Alt-Ergo  Total   Success
   job                       6        3        9       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
-  /*@ behavior typed:
+[wp] tests/wp_acsl/assigns_path.i:12: Warning: 
+  Memory model hypotheses for function 'job':
+  /*@ behavior wp_typed:
         requires \separated(b + (..), &p); */
   void job(int n, int *b);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
index 48e98d4fa14c783c2f68c1b0a33ea97593912457..7b0245a0e6efb58b2d203320f97dd91e6ecff2c3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
@@ -49,9 +49,10 @@
  Functions                 WP     Alt-Ergo  Total   Success
   function                 20       19       39       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'function':
+[wp] tests/wp_acsl/chunk_typing.i:21: Warning: 
+  Memory model hypotheses for function 'function':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated(i16 + (..), (char const *)x + (..));
        requires \separated(i32 + (..), (char const *)x + (..));
        requires \separated(i64 + (..), (char const *)x + (..));
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
index 9e0fd3122c659339481553df508465ea91fdba64..611e1df5b2346833d7a864082944152d1fc2d6fe 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
@@ -26,7 +26,8 @@
   mixed_array_pointer       -        -        2       0.0%
   absurd                    -        -        2       0.0%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'absurd':
-  /*@ behavior typed_ref:
+[wp] tests/wp_acsl/pointer.i:73: Warning: 
+  Memory model hypotheses for function 'absurd':
+  /*@ behavior wp_typed_ref:
         requires \separated(q + (..), &p); */
   void absurd(int *q);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
index 5e0172dd87d30107441b9959cdf9c1f5460443b4..bc584ec39a2bd1f1c490cfcf15d0c7c3e933b0e6 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
@@ -26,7 +26,8 @@
   mixed_array_pointer       -        -        2       0.0%
   absurd                    -        -        2       0.0%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'absurd':
-  /*@ behavior typed:
+[wp] tests/wp_acsl/pointer.i:73: Warning: 
+  Memory model hypotheses for function 'absurd':
+  /*@ behavior wp_typed:
         requires \separated(q + (..), &p); */
   void absurd(int *q);
diff --git a/src/plugins/wp/tests/wp_bts/bts_2110.i b/src/plugins/wp/tests/wp_bts/bts_2110.i
index 59e26712f6995c7046c95bbf23a93f892c4c334e..807a50f5053ba69291bc3408ccd85bad69fb88a7 100644
--- a/src/plugins/wp/tests/wp_bts/bts_2110.i
+++ b/src/plugins/wp/tests/wp_bts/bts_2110.i
@@ -1,5 +1,5 @@
 /* run.config
-   CMD: @frama-c@ -wp -wp-msg-key shell,cluster,print-generated -wp-prover why3 -wp-gen -wp-share ./share
+   CMD: @frama-c@ -wp -wp-msg-key shell,cluster,print-generated -wp-prover why3 -wp-gen -wp-share ./share -wp-warn-key "pedantic-assigns=inactive"
    OPT:
 */
 
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
index 8c6fd6aed1b7c5243665509741e7e24b10b1b1d3..f5978426720ef2f96d406680c2c8728e7d414f59 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
@@ -52,7 +52,8 @@ Goal Instance of 'Pre-condition (file tests/wp_bts/bts0843.i, line 12) in 'f3''
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f3':
-  /*@ behavior typed:
+[wp] tests/wp_bts/bts0843.i:13: Warning: 
+  Memory model hypotheses for function 'f3':
+  /*@ behavior wp_typed:
         requires \separated(&p, &p->a); */
   void f3(void);
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle
index 640c9952226375d9ac25aa5260796f23f8a44c67..beb9985d22d92f771e20d79592ca3ab408a2442e 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle
@@ -65,7 +65,8 @@ Assume {
 Prove: global(L_two_24) != one_0.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_frame':
-  /*@ behavior typed:
+[wp] tests/wp_bts/bts_1828.i:56: Warning: 
+  Memory model hypotheses for function 'global_frame':
+  /*@ behavior wp_typed:
         requires \separated(one, &zero); */
   void global_frame(int *one, int arg);
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
index 5b00c3b48f392cf59718f82003f6f14f9c6376d4..1f183b1d30a1530c5c404f9a38f7ed12fec5d9ff 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
@@ -44,9 +44,10 @@ Assume {
 Prove: global(L_two_24) != one_0.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_frame':
+[wp] tests/wp_bts/bts_1828.i:56: Warning: 
+  Memory model hypotheses for function 'global_frame':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(zero, one);
        requires \valid(one);
        requires \valid(zero);
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
index fbd210f679cb91ec29196a1b2f0e5f4b01f8f764..c03a3a919adbf377b4708ec6c4893de1c1af9bcd 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
@@ -15,7 +15,8 @@
   f3                        1        -        1       100%
   g3                        1        2        3       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f3':
-  /*@ behavior typed:
+[wp] tests/wp_bts/bts0843.i:13: Warning: 
+  Memory model hypotheses for function 'f3':
+  /*@ behavior wp_typed:
         requires \separated(&p, &p->a); */
   void f3(void);
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
index 91203bd8a7c316be36b9377c010047ff59f965b9..ae39dccf7daf8069747276e8f126cee91ea56590 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
@@ -17,7 +17,8 @@
   local_frame               -        1        1       100%
   global_frame              3        -        5      60.0%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_frame':
-  /*@ behavior typed:
+[wp] tests/wp_bts/bts_1828.i:56: Warning: 
+  Memory model hypotheses for function 'global_frame':
+  /*@ behavior wp_typed:
         requires \separated(one, &zero); */
   void global_frame(int *one, int arg);
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
index e5edde37e9b7b942c93989d95bb6fd04d5118460..43305903b452ccabf5e96e46b022d2bfe3c1ffce 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
@@ -17,9 +17,10 @@
   local_frame               -        1        1       100%
   global_frame              5        -        5       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_frame':
+[wp] tests/wp_bts/bts_1828.i:56: Warning: 
+  Memory model hypotheses for function 'global_frame':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(zero, one);
        requires \valid(one);
        requires \valid(zero);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
index e21f8f5fe4bc97954c318b6c4531baf28e311bc2..56bb306558b56d74141556fc1b026d735ef9cfe9 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
@@ -52,9 +52,10 @@
 [wp] Goal typed_ref_equal_elements_loop_variant_positive : not tried
 [wp] Goal typed_ref_equal_elements_loop_variant_2_decrease : not tried
 [wp] Goal typed_ref_equal_elements_loop_variant_2_positive : not tried
-[wp] Warning: Memory model hypotheses for function 'equal_elements':
+[wp] tests/wp_gallery/frama_c_exo3_solved.old.c:73: Warning: 
+  Memory model hypotheses for function 'equal_elements':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(v1, v2, a + (..));
        requires \valid(v1);
        requires \valid(v2);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
index 0a5004c676571d4ea94cd0cf4e06b37217771f29..53078f53cb88bbc0681c1ce463aef6b08bf1de0e 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
@@ -53,9 +53,10 @@
 [wp] Goal typed_ref_equal_elements_loop_variant_positive : not tried
 [wp] Goal typed_ref_equal_elements_loop_variant_2_decrease : not tried
 [wp] Goal typed_ref_equal_elements_loop_variant_2_positive : not tried
-[wp] Warning: Memory model hypotheses for function 'equal_elements':
+[wp] tests/wp_gallery/frama_c_exo3_solved.old.v2.c:56: Warning: 
+  Memory model hypotheses for function 'equal_elements':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(v1, v2, a + (..));
        requires \valid(v1);
        requires \valid(v2);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
index e75ffe7ec64e8d454c01d3b2497ea7e10bd7e9c7..3903ba3a3a32a691f6e6e2bce73a83b71362f378 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
@@ -44,9 +44,10 @@
  Functions                 WP     Alt-Ergo  Total   Success
   equal_elements           18       16       34       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'equal_elements':
+[wp] tests/wp_gallery/frama_c_exo3_solved.old.c:73: Warning: 
+  Memory model hypotheses for function 'equal_elements':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(v1, v2, a + (..));
        requires \valid(v1);
        requires \valid(v2);
@@ -78,11 +79,3 @@
  Functions                 WP     Alt-Ergo  Total   Success
   equal_elements           29       21       50       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'equal_elements':
-  /*@
-     behavior typed_ref:
-       requires \separated(v1, v2, a + (..));
-       requires \valid(v1);
-       requires \valid(v2);
-     */
-  void equal_elements(int *a, int *v1, int *v2);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
index 7672a505bc9fa5d57e9cd506b0e0b2ed7d01591d..1dfeafb91d559189ced438c76169d59f9f36c303 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
@@ -45,9 +45,10 @@
  Functions                 WP     Alt-Ergo  Total   Success
   equal_elements           17       18       35       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'equal_elements':
+[wp] tests/wp_gallery/frama_c_exo3_solved.old.v2.c:56: Warning: 
+  Memory model hypotheses for function 'equal_elements':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(v1, v2, a + (..));
        requires \valid(v1);
        requires \valid(v2);
@@ -79,11 +80,3 @@
  Functions                 WP     Alt-Ergo  Total   Success
   equal_elements           28       23       51       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'equal_elements':
-  /*@
-     behavior typed_ref:
-       requires \separated(v1, v2, a + (..));
-       requires \valid(v1);
-       requires \valid(v2);
-     */
-  void equal_elements(int *a, int *v1, int *v2);
diff --git a/src/plugins/wp/tests/wp_hoare/alias_assigns_hypotheses.i b/src/plugins/wp/tests/wp_hoare/alias_assigns_hypotheses.i
index d92187251b3139329c7f1f93a37bd33bc2f19656..8188f732108bf5a493deeaf1ff3da39a21cb6619 100644
--- a/src/plugins/wp/tests/wp_hoare/alias_assigns_hypotheses.i
+++ b/src/plugins/wp/tests/wp_hoare/alias_assigns_hypotheses.i
@@ -1,6 +1,6 @@
 /* run.config
    OPT:
-   OPT:-wp-no-warn-memory-model -wp-check-model-hypotheses -then -print
+   OPT:-wp-no-warn-memory-model -wp-check-memory-model -then -print
 */
 
 /* run.config_qualif
diff --git a/src/plugins/wp/tests/wp_hoare/alias_escapes_hypotheses.i b/src/plugins/wp/tests/wp_hoare/alias_escapes_hypotheses.i
new file mode 100644
index 0000000000000000000000000000000000000000..596e833fd35879adb7401fa91f871b8be7b0719d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/alias_escapes_hypotheses.i
@@ -0,0 +1,42 @@
+/* run.config
+   OPT:
+   OPT:-wp-no-warn-memory-model -wp-check-memory-model -then -print
+*/
+
+/* run.config_qualif
+  DONTRUN:
+*/
+
+int a ;
+
+/*@ assigns \result \from \nothing ; */
+int* f1(void){
+  a = 42 ;
+  return (void*) 0 ;
+}
+
+/*@ assigns \result \from &a ; */
+int* f2(void){
+  return &a ;
+}
+
+/*@ assigns \result \from \nothing ; */
+int* f3(int x){
+  return &x ;
+}
+
+/*@ assigns *p \from \nothing ; */
+void fp1(int** p){
+  a = 42 ;
+  *p = (void*) 0 ;
+}
+
+/*@ assigns *p \from &a ; */
+void fp2(int** p){
+  *p = &a ;
+}
+
+/*@ assigns *p \from \nothing ; */
+void fp3(int** p, int x){
+  *p = &x ;
+}
diff --git a/src/plugins/wp/tests/wp_hoare/memory_hypotheses_checking.i b/src/plugins/wp/tests/wp_hoare/memory_hypotheses_checking.i
new file mode 100644
index 0000000000000000000000000000000000000000..1edcae76dccd752b02c2566b78382670f647251d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/memory_hypotheses_checking.i
@@ -0,0 +1,99 @@
+/* run.config
+   OPT:-wp-model +ref -wp-no-warn-memory-model -wp-check-memory-model -then -print
+*/
+
+/* run.config_qualif
+   OPT:-wp-model +ref -wp-no-warn-memory-model -wp-check-memory-model
+*/
+
+int g ;
+
+//@ assigns \nothing ;
+int sep(int* p){
+  return *p + g;
+}
+
+//@ assigns \nothing;
+void call_sep_ok(void){
+  int l = 42;
+  sep(&l);
+}
+
+//@ assigns \nothing ;
+void call_sep_bad_sep(void){
+  sep(&g);
+}
+
+//@ assigns \nothing ;
+void call_sep_bad_valid(void){
+  int * p ;
+  {
+    int l ;
+    p = &l ;
+  }
+  sep(p);
+}
+
+int *p;
+//@ assigns \nothing ;
+int gptr_sep(void){
+  return *p + g;
+}
+
+//@ assigns p \from \nothing ;
+void call_gptr_sep_ok(void){
+  int l = 42;
+  p = &l ;
+  gptr_sep();
+}
+
+//@ assigns p \from &g ;
+void call_gptr_sep_bad(void){
+  p = &g;
+  gptr_sep();
+}
+
+
+/*@ assigns *p ; */
+void assigns_ptr(int *p){
+  *p = g + 42 ;
+}
+
+//@ assigns \nothing;
+void call_assigns_ptr_ok(void){
+  int l = 42;
+  assigns_ptr(&l);
+}
+
+//@ assigns g ;
+void call_assigns_ptr_bad(void){
+  assigns_ptr(&g);
+}
+
+/*@
+  assigns \result \from p ;
+  assigns *p ;
+  ensures \result == p ;
+*/
+int * add_return_ok(int *p){
+  (*p) += g ;
+  return p ;
+}
+
+//@ assigns g ;
+void call_add_return_ok(void){
+  int l = 0;
+  int *p = add_return_ok(&l);
+  *p = 0;
+}
+
+//@ assigns g ;
+void call_add_return_bad(void){
+  int *p = add_return_ok(&g);
+  *p = 0;
+}
+
+//@ assigns \result \from &x ;
+int * bad_return_formal(int x){
+  return &x;
+}
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle
index 832baab84eb61db255327ed172594084b92caa0c..8466ed1f89b2a33727f083057237518820c3eabb 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle
@@ -193,51 +193,59 @@ Effect at line 103
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:17: Warning: 
+  Memory model hypotheses for function 'global_alias':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated(g_alias, (int *)global + (..), &g_alias);
      */
   void global_alias(void);
-[wp] Warning: Memory model hypotheses for function 'global_no_alias':
-  /*@ behavior typed:
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:24: Warning: 
+  Memory model hypotheses for function 'global_no_alias':
+  /*@ behavior wp_typed:
         requires \separated(g_alias, &g_alias); */
   void global_no_alias(void);
-[wp] Warning: Memory model hypotheses for function 'formal_alias':
-  /*@ behavior typed:
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:32: Warning: 
+  Memory model hypotheses for function 'formal_alias':
+  /*@ behavior wp_typed:
         requires \separated(f_alias, (int *)global + (..)); */
   void formal_alias(int *f_alias);
-[wp] Warning: Memory model hypotheses for function 'formal_alias_array':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:48: Warning: 
+  Memory model hypotheses for function 'formal_alias_array':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated((int *)global + (..), &(*alias_array)[0 .. 1]);
        requires \separated(alias_array + (..), (int *)global + (..));
      */
   void formal_alias_array(int (*alias_array)[2]);
-[wp] Warning: Memory model hypotheses for function 'field_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:61: Warning: 
+  Memory model hypotheses for function 'field_alias':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated((int *)global + (..), &x->x);
        requires \separated(x, (int *)global + (..));
      */
   void field_alias(struct X *x);
-[wp] Warning: Memory model hypotheses for function 'field_range_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:73: Warning: 
+  Memory model hypotheses for function 'field_range_alias':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated((int *)global + (..), &(x + (0 .. 3))->x);
        requires \separated(x + (..), (int *)global + (..));
      */
   void field_range_alias(struct X *x);
-[wp] Warning: Memory model hypotheses for function 'set_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:81: Warning: 
+  Memory model hypotheses for function 'set_alias':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
        requires \separated(f_alias, (int *)global + (..), &g_alias);
      */
   void set_alias(int *f_alias);
-[wp] Warning: Memory model hypotheses for function 'comprehension_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:92: Warning: 
+  Memory model hypotheses for function 'comprehension_alias':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires
          \separated(
            (int *)global + (..), &g_alias,
@@ -245,9 +253,10 @@ Prove: true.
            );
      */
   void comprehension_alias(void);
-[wp] Warning: Memory model hypotheses for function 'union_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:102: Warning: 
+  Memory model hypotheses for function 'union_alias':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
        requires \separated(f_alias, (int *)global + (..), &g_alias);
      */
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle
index 3da623e24931019ca8f1a8fbdc64132f1611c015..d0a161603cf991c1248998ebc3fc7474a1dbfb09 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle
@@ -204,7 +204,7 @@ int *g_alias;
     ensures \old(global[0]) ≡ global[0];
     assigns *g_alias;
     
-    behavior typed:
+    behavior wp_typed:
       requires \separated(g_alias, (int *)global + (..), &g_alias);
  */
 void global_alias(void)
@@ -217,7 +217,7 @@ void global_alias(void)
     ensures *g_alias ≡ 1;
     assigns *g_alias;
     
-    behavior typed:
+    behavior wp_typed:
       requires \separated(g_alias, &g_alias);
  */
 void global_no_alias(void)
@@ -231,7 +231,7 @@ void global_no_alias(void)
     ensures \old(global[0]) ≡ global[0];
     assigns *f_alias;
     
-    behavior typed:
+    behavior wp_typed:
       requires \separated(f_alias, (int *)global + (..));
  */
 void formal_alias(int *f_alias)
@@ -256,7 +256,7 @@ void formal_no_alias(int *f_alias)
     ensures \old(global[0]) ≡ global[0];
     assigns (*alias_array)[0 .. 1];
     
-    behavior typed:
+    behavior wp_typed:
       requires \separated((int *)global + (..), &(*alias_array)[0 .. 1]);
       requires \separated(alias_array + (..), (int *)global + (..));
  */
@@ -272,7 +272,7 @@ void formal_alias_array(int (*alias_array)[2])
     ensures \old(global[0]) ≡ global[0];
     assigns x->x;
     
-    behavior typed:
+    behavior wp_typed:
       requires \separated((int *)global + (..), &x->x);
       requires \separated(x, (int *)global + (..));
  */
@@ -287,7 +287,7 @@ void field_alias(struct X *x)
     ensures \old(global[0]) ≡ global[0];
     assigns (x + (0 .. 3))->x;
     
-    behavior typed:
+    behavior wp_typed:
       requires \separated((int *)global + (..), &(x + (0 .. 3))->x);
       requires \separated(x + (..), (int *)global + (..));
  */
@@ -302,7 +302,7 @@ void field_range_alias(struct X *x)
     ensures \old(global[0]) ≡ global[0];
     assigns {*g_alias, *f_alias};
     
-    behavior typed:
+    behavior wp_typed:
       requires
         \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
       requires \separated(f_alias, (int *)global + (..), &g_alias);
@@ -318,7 +318,7 @@ void set_alias(int *f_alias)
     ensures \old(global[0]) ≡ global[0];
     assigns {*alias | int *alias; alias ≡ \at(g_alias,Pre)};
     
-    behavior typed:
+    behavior wp_typed:
       requires
         \separated(
           (int *)global + (..), &g_alias,
@@ -336,7 +336,7 @@ void comprehension_alias(void)
     ensures \old(global[0]) ≡ global[0];
     assigns {*g_alias, *f_alias};
     
-    behavior typed:
+    behavior wp_typed:
       requires
         \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
       requires \separated(f_alias, (int *)global + (..), &g_alias);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_escapes_hypotheses.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_escapes_hypotheses.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..98b310d588224c1d25702c99910934bbb1190db4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/oracle/alias_escapes_hypotheses.0.res.oracle
@@ -0,0 +1,91 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_hoare/alias_escapes_hypotheses.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function f1
+------------------------------------------------------------
+
+Goal Assigns nothing in 'f1' (1/2):
+Effect at line 14
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'f1' (2/2):
+Effect at line 15
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function f2
+------------------------------------------------------------
+
+Goal Assigns nothing in 'f2':
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function f3
+------------------------------------------------------------
+
+Goal Assigns nothing in 'f3':
+Effect at line 25
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fp1
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_escapes_hypotheses.i, line 28) in 'fp1' (1/2):
+Effect at line 30
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_escapes_hypotheses.i, line 28) in 'fp1' (2/2):
+Effect at line 31
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fp2
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_escapes_hypotheses.i, line 34) in 'fp2':
+Effect at line 36
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fp3
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_escapes_hypotheses.i, line 39) in 'fp3':
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+[wp] tests/wp_hoare/alias_escapes_hypotheses.i:13: Warning: 
+  Memory model hypotheses for function 'f1':
+  /*@ behavior wp_typed:
+        ensures \separated(\result, &a); */
+  int *f1(void);
+[wp] tests/wp_hoare/alias_escapes_hypotheses.i:24: Warning: 
+  Memory model hypotheses for function 'f3':
+  /*@ behavior wp_typed:
+        ensures \separated(\result, &x); */
+  int *f3(int x);
+[wp] tests/wp_hoare/alias_escapes_hypotheses.i:29: Warning: 
+  Memory model hypotheses for function 'fp1':
+  /*@ behavior wp_typed:
+        requires \separated(p, &a);
+        ensures \separated(p, &a); */
+  void fp1(int **p);
+[wp] tests/wp_hoare/alias_escapes_hypotheses.i:40: Warning: 
+  Memory model hypotheses for function 'fp3':
+  /*@ behavior wp_typed:
+        ensures \separated(p, &x); */
+  void fp3(int **p, int x);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_escapes_hypotheses.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_escapes_hypotheses.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f5a09c1b43a0e2513d2fd1f2dc70f68f7801815c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/oracle/alias_escapes_hypotheses.1.res.oracle
@@ -0,0 +1,176 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_hoare/alias_escapes_hypotheses.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function f1
+------------------------------------------------------------
+
+Goal Assigns nothing in 'f1' (1/2):
+Effect at line 14
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'f1' (2/2):
+Effect at line 15
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function f1 with behavior wp_typed
+------------------------------------------------------------
+
+Goal Post-condition for 'wp_typed' (file tests/wp_hoare/alias_escapes_hypotheses.i, line 13) in 'f1':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function f2
+------------------------------------------------------------
+
+Goal Assigns nothing in 'f2':
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function f3
+------------------------------------------------------------
+
+Goal Assigns nothing in 'f3':
+Effect at line 25
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function f3 with behavior wp_typed
+------------------------------------------------------------
+
+Goal Post-condition for 'wp_typed' (file tests/wp_hoare/alias_escapes_hypotheses.i, line 24) in 'f3':
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fp1
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_escapes_hypotheses.i, line 28) in 'fp1' (1/2):
+Effect at line 30
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_escapes_hypotheses.i, line 28) in 'fp1' (2/2):
+Effect at line 31
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fp1 with behavior wp_typed
+------------------------------------------------------------
+
+Goal Post-condition for 'wp_typed' (file tests/wp_hoare/alias_escapes_hypotheses.i, line 29) in 'fp1':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fp2
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_escapes_hypotheses.i, line 34) in 'fp2':
+Effect at line 36
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fp3
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/alias_escapes_hypotheses.i, line 39) in 'fp3':
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fp3 with behavior wp_typed
+------------------------------------------------------------
+
+Goal Post-condition for 'wp_typed' (file tests/wp_hoare/alias_escapes_hypotheses.i, line 40) in 'fp3':
+Assume { (* Heap *) Type: region(p.base) <= 0. }
+Prove: global(P_x_46) != p.
+
+------------------------------------------------------------
+/* Generated by Frama-C */
+int a;
+/*@ assigns \result;
+    assigns \result \from \nothing;
+    
+    behavior wp_typed:
+      ensures \separated(\result, &a);
+ */
+int *f1(void)
+{
+  int *__retres;
+  a = 42;
+  __retres = (int *)0;
+  return __retres;
+}
+
+/*@ assigns \result;
+    assigns \result \from &a; */
+int *f2(void)
+{
+  int *__retres;
+  __retres = & a;
+  return __retres;
+}
+
+/*@ assigns \result;
+    assigns \result \from \nothing;
+    
+    behavior wp_typed:
+      ensures \separated(\result, &x);
+ */
+int *f3(int x)
+{
+  int *__retres;
+  __retres = & x;
+  return __retres;
+}
+
+/*@ assigns *p;
+    assigns *p \from \nothing;
+    
+    behavior wp_typed:
+      requires \separated(p, &a);
+      ensures \separated(p, &a);
+ */
+void fp1(int **p)
+{
+  a = 42;
+  *p = (int *)0;
+  return;
+}
+
+/*@ assigns *p;
+    assigns *p \from &a; */
+void fp2(int **p)
+{
+  *p = & a;
+  return;
+}
+
+/*@ assigns *p;
+    assigns *p \from \nothing;
+    
+    behavior wp_typed:
+      ensures \separated(p, &x);
+ */
+void fp3(int **p, int x)
+{
+  *p = & x;
+  return;
+}
+
+
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle
index 54ad8489278e68186e342fc1157d755cd613d62f..242f5a77ff302f76bdf9ebf17e7311f394fdfb07 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle
@@ -85,15 +85,18 @@ Goal Instance of 'Pre-condition (file tests/wp_hoare/byref.i, line 11) in 'f'' i
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/byref.i:14: Warning: 
+  Memory model hypotheses for function 'f':
+  /*@ behavior wp_typed_ref:
         requires \valid(r); */
   void f(int *r);
-[wp] Warning: Memory model hypotheses for function 'wrong_without_ref':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/byref.i:20: Warning: 
+  Memory model hypotheses for function 'wrong_without_ref':
+  /*@ behavior wp_typed_ref:
         requires \valid(q); */
   int wrong_without_ref(int *q);
-[wp] Warning: Memory model hypotheses for function 'pointer':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/byref.i:31: Warning: 
+  Memory model hypotheses for function 'pointer':
+  /*@ behavior wp_typed_ref:
         requires \valid(q); */
   int pointer(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
index d2646994c22e0a1dbada00d2f6169e04da38ab0e..03056370c4a6760b6e4e1e2f3662a4c7bf5753a0 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
@@ -496,11 +496,38 @@ Effect at line 46
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'ref_bd':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var.i:12: Warning: 
+  Memory model hypotheses for function 'ref_ctr':
+  /*@ behavior wp_typed_ref:
+        requires \valid(p); */
+  int ref_ctr(int *p);
+[wp] tests/wp_hoare/dispatch_var.i:44: Warning: 
+  Memory model hypotheses for function 'ref_bd':
+  /*@ behavior wp_typed_ref:
         requires \valid(q); */
   int ref_bd(int *q);
-[wp] Warning: Memory model hypotheses for function 'g':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var.i:83: Warning: 
+  Memory model hypotheses for function 'ref_valid':
+  /*@ behavior wp_typed_ref:
+        requires \valid(p1); */
+  int ref_valid(int *p1);
+[wp] tests/wp_hoare/dispatch_var.i:133: Warning: 
+  Memory model hypotheses for function 'ref_ctr_nr':
+  /*@
+     behavior wp_typed_ref:
+       requires \separated(ref, ref1, ref2);
+       requires \valid(ref);
+       requires \valid(ref1);
+       requires \valid(ref2);
+     */
+  int ref_ctr_nr(int *ref, int *ref1, int *ref2);
+[wp] tests/wp_hoare/dispatch_var.i:158: Warning: 
+  Memory model hypotheses for function 'ref_ctr_nstars':
+  /*@ behavior wp_typed_ref:
+        requires \valid(pp); */
+  int ref_ctr_nstars(int **pp);
+[wp] tests/wp_hoare/dispatch_var.i:194: Warning: 
+  Memory model hypotheses for function 'g':
+  /*@ behavior wp_typed_ref:
         requires \valid(pg); */
   int g(int *pg);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
index 61bf6b67367b214b40e53f5d9d9e9fff16e4a0fe..f4ddcc684505866177434a0690f31e787b73a9da 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
@@ -485,19 +485,23 @@ Goal Assigns (file tests/wp_hoare/dispatch_var2.i, line 13) in 'reset':
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:16: Warning: 
+  Memory model hypotheses for function 'reset':
+  /*@ behavior wp_typed_ref:
         requires \valid(rp); */
   void reset(int *rp);
-[wp] Warning: Memory model hypotheses for function 'incr':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:23: Warning: 
+  Memory model hypotheses for function 'incr':
+  /*@ behavior wp_typed_ref:
         requires \valid(ip); */
   void incr(int *ip);
-[wp] Warning: Memory model hypotheses for function 'load':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:31: Warning: 
+  Memory model hypotheses for function 'load':
+  /*@ behavior wp_typed_ref:
         requires \valid(lp); */
   int load(int *lp);
-[wp] Warning: Memory model hypotheses for function 'call_param_ref':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:70: Warning: 
+  Memory model hypotheses for function 'call_param_ref':
+  /*@ behavior wp_typed_ref:
         requires \valid(q); */
   int call_param_ref(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle
index 44ae58e7b74ba0fb1e7c7ef27a28f0155be239f7..1e932094cc2e77a3a6e96c4fbe00a3594a0f4ca6 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle
@@ -210,19 +210,23 @@ Goal Assigns (file tests/wp_hoare/dispatch_var2.i, line 13) in 'reset':
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:16: Warning: 
+  Memory model hypotheses for function 'reset':
+  /*@ behavior wp_typed_ref:
         requires \valid(rp); */
   void reset(int *rp);
-[wp] Warning: Memory model hypotheses for function 'incr':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:23: Warning: 
+  Memory model hypotheses for function 'incr':
+  /*@ behavior wp_typed_ref:
         requires \valid(ip); */
   void incr(int *ip);
-[wp] Warning: Memory model hypotheses for function 'load':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:31: Warning: 
+  Memory model hypotheses for function 'load':
+  /*@ behavior wp_typed_ref:
         requires \valid(lp); */
   int load(int *lp);
-[wp] Warning: Memory model hypotheses for function 'call_param_ref':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:70: Warning: 
+  Memory model hypotheses for function 'call_param_ref':
+  /*@ behavior wp_typed_ref:
         requires \valid(q); */
   int call_param_ref(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/memory_hypotheses_checking.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/memory_hypotheses_checking.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..380a7e0cc8ace27dc70721782cf090990ab2631b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/oracle/memory_hypotheses_checking.res.oracle
@@ -0,0 +1,486 @@
+# frama-c -wp -wp-model 'Typed (Ref)' [...]
+[kernel] Parsing tests/wp_hoare/memory_hypotheses_checking.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function add_return_ok
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_hoare/memory_hypotheses_checking.i, line 76) in 'add_return_ok':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 74) in 'add_return_ok':
+Effect at line 79
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function add_return_ok with behavior wp_typed_ref
+------------------------------------------------------------
+
+Goal Post-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 78) in 'add_return_ok':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function assigns_ptr
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 57) in 'assigns_ptr':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function bad_return_formal
+------------------------------------------------------------
+
+Goal Assigns nothing in 'bad_return_formal':
+Effect at line 98
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function bad_return_formal with behavior wp_typed_ref
+------------------------------------------------------------
+
+Goal Post-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 97) in 'bad_return_formal':
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function call_add_return_bad
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 90) in 'call_add_return_bad':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 90) in 'call_add_return_bad' (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 90) in 'call_add_return_bad' (2/3):
+Call Result at line 92
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 90) in 'call_add_return_bad' (3/3):
+Effect at line 93
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 78) in 'add_return_ok'' in 'call_add_return_bad' at initialization of 'p_0' (file tests/wp_hoare/memory_hypotheses_checking.i, line 92)
+:
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 78) in 'add_return_ok'' in 'call_add_return_bad' at initialization of 'p_0' (file tests/wp_hoare/memory_hypotheses_checking.i, line 92)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function call_add_return_ok
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 83) in 'call_add_return_ok':
+Call Effect at line 86
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 83) in 'call_add_return_ok' (1/3):
+Call Effect at line 86
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 83) in 'call_add_return_ok' (2/3):
+Call Result at line 86
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 83) in 'call_add_return_ok' (3/3):
+Effect at line 87
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: invalid(Malloc_0, global(L_l_71), 1).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 78) in 'add_return_ok'' in 'call_add_return_ok' at initialization of 'p_0' (file tests/wp_hoare/memory_hypotheses_checking.i, line 86)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 78) in 'add_return_ok'' in 'call_add_return_ok' at initialization of 'p_0' (file tests/wp_hoare/memory_hypotheses_checking.i, line 86)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function call_assigns_ptr_bad
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 68) in 'call_assigns_ptr_bad':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 68) in 'call_assigns_ptr_bad':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 58) in 'assigns_ptr'' in 'call_assigns_ptr_bad' at call 'assigns_ptr' (file tests/wp_hoare/memory_hypotheses_checking.i, line 70)
+:
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 58) in 'assigns_ptr'' in 'call_assigns_ptr_bad' at call 'assigns_ptr' (file tests/wp_hoare/memory_hypotheses_checking.i, line 70)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function call_assigns_ptr_ok
+------------------------------------------------------------
+
+Goal Assigns nothing in 'call_assigns_ptr_ok':
+Call Effect at line 65
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'call_assigns_ptr_ok':
+Call Effect at line 65
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 58) in 'assigns_ptr'' in 'call_assigns_ptr_ok' at call 'assigns_ptr' (file tests/wp_hoare/memory_hypotheses_checking.i, line 65)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 58) in 'assigns_ptr'' in 'call_assigns_ptr_ok' at call 'assigns_ptr' (file tests/wp_hoare/memory_hypotheses_checking.i, line 65)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function call_gptr_sep_bad
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 50) in 'call_gptr_sep_bad':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 50) in 'call_gptr_sep_bad':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 39) in 'gptr_sep'' in 'call_gptr_sep_bad' at call 'gptr_sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 53)
+:
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 39) in 'gptr_sep'' in 'call_gptr_sep_bad' at call 'gptr_sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 53)
+:
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_rw(Malloc_0, global(G_g_20), 1).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function call_gptr_sep_ok
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 43) in 'call_gptr_sep_ok':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_hoare/memory_hypotheses_checking.i, line 43) in 'call_gptr_sep_ok':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 39) in 'gptr_sep'' in 'call_gptr_sep_ok' at call 'gptr_sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 47)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 39) in 'gptr_sep'' in 'call_gptr_sep_ok' at call 'gptr_sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 47)
+:
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_rw(Malloc_0[L_l_46 <- 1], global(L_l_46), 1).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function call_sep_bad_sep
+------------------------------------------------------------
+
+Goal Assigns nothing in 'call_sep_bad_sep':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'call_sep_bad_sep':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_bad_sep' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 24)
+:
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_bad_sep' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 24)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function call_sep_bad_valid
+------------------------------------------------------------
+
+Goal Assigns nothing in 'call_sep_bad_valid' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'call_sep_bad_valid' (2/2):
+Effect at line 32
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'call_sep_bad_valid' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'call_sep_bad_valid' (2/2):
+Effect at line 32
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_bad_valid' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 34)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_bad_valid' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 34)
+:
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_rw(Malloc_0[L_l_37 <- 0], global(L_l_37), 1).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function call_sep_ok
+------------------------------------------------------------
+
+Goal Assigns nothing in 'call_sep_ok':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'call_sep_ok':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_ok' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 19)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_ok' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 19)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function gptr_sep
+------------------------------------------------------------
+
+Goal Assigns nothing in 'gptr_sep':
+Effect at line 40
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function sep
+------------------------------------------------------------
+
+Goal Assigns nothing in 'sep':
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+/* Generated by Frama-C */
+int g;
+/*@ assigns \nothing;
+    
+    behavior wp_typed_ref:
+      requires \separated(p_0, &g);
+      requires \valid(p_0);
+ */
+int sep(int *p_0)
+{
+  int __retres;
+  __retres = *p_0 + g;
+  return __retres;
+}
+
+/*@ assigns \nothing; */
+void call_sep_ok(void)
+{
+  int l = 42;
+  sep(& l);
+  return;
+}
+
+/*@ assigns \nothing; */
+void call_sep_bad_sep(void)
+{
+  sep(& g);
+  return;
+}
+
+/*@ assigns \nothing; */
+void call_sep_bad_valid(void)
+{
+  int *p_0;
+  {
+    int l;
+    p_0 = & l;
+  }
+  sep(p_0);
+  return;
+}
+
+int *p;
+/*@ assigns \nothing;
+    
+    behavior wp_typed_ref:
+      requires \separated(p, &g);
+      requires \valid(p);
+ */
+int gptr_sep(void)
+{
+  int __retres;
+  __retres = *p + g;
+  return __retres;
+}
+
+/*@ assigns p;
+    assigns p \from \nothing; */
+void call_gptr_sep_ok(void)
+{
+  int l = 42;
+  p = & l;
+  gptr_sep();
+  return;
+}
+
+/*@ assigns p;
+    assigns p \from &g; */
+void call_gptr_sep_bad(void)
+{
+  p = & g;
+  gptr_sep();
+  return;
+}
+
+/*@ assigns *p_0;
+    
+    behavior wp_typed_ref:
+      requires \separated(p_0, &g);
+      requires \valid(p_0);
+ */
+void assigns_ptr(int *p_0)
+{
+  *p_0 = g + 42;
+  return;
+}
+
+/*@ assigns \nothing; */
+void call_assigns_ptr_ok(void)
+{
+  int l = 42;
+  assigns_ptr(& l);
+  return;
+}
+
+/*@ assigns g; */
+void call_assigns_ptr_bad(void)
+{
+  assigns_ptr(& g);
+  return;
+}
+
+/*@ ensures \result ≡ \old(p_0);
+    assigns \result, *p_0;
+    assigns \result \from p_0;
+    
+    behavior wp_typed_ref:
+      requires \separated(p_0 + (..), &g);
+      requires \separated(p_0, &g);
+      ensures \separated(\result, &g);
+ */
+int *add_return_ok(int *p_0)
+{
+  *p_0 += g;
+  return p_0;
+}
+
+/*@ assigns g; */
+void call_add_return_ok(void)
+{
+  int l = 0;
+  int *p_0 = add_return_ok(& l);
+  *p_0 = 0;
+  return;
+}
+
+/*@ assigns g; */
+void call_add_return_bad(void)
+{
+  int *p_0 = add_return_ok(& g);
+  *p_0 = 0;
+  return;
+}
+
+/*@ assigns \result;
+    assigns \result \from &x;
+    
+    behavior wp_typed_ref:
+      ensures \separated(\result, &x);
+ */
+int *bad_return_formal(int x)
+{
+  int *__retres;
+  __retres = & x;
+  return __retres;
+}
+
+
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
index c6bec6fef0728d4b3598e5ec6ae9d881cbec4150..bf4453996e1f0c3f7c0390b232a6c5e86e4608d0 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
@@ -141,15 +141,32 @@ Goal Assigns (file tests/wp_hoare/reference.i, line 57) in 'write':
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'call_f2':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/reference.i:14: Warning: 
+  Memory model hypotheses for function 'f':
+  /*@ behavior wp_typed_ref:
+        requires \valid(p); */
+  int f(int *p);
+[wp] tests/wp_hoare/reference.i:30: Warning: 
+  Memory model hypotheses for function 'f2':
+  /*@
+     behavior wp_typed_ref:
+       requires \separated(p2, q);
+       requires \valid(p2);
+       requires \valid(q);
+     */
+  int f2(int *p2, int *q);
+[wp] tests/wp_hoare/reference.i:37: Warning: 
+  Memory model hypotheses for function 'call_f2':
+  /*@ behavior wp_typed_ref:
         requires \valid(ptr); */
   int call_f2(int *ptr, int y);
-[wp] Warning: Memory model hypotheses for function 'call_global':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/reference.i:48: Warning: 
+  Memory model hypotheses for function 'call_global':
+  /*@ behavior wp_typed_ref:
         requires \valid(gl); */
   int call_global(void);
-[wp] Warning: Memory model hypotheses for function 'write':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/reference.i:60: Warning: 
+  Memory model hypotheses for function 'write':
+  /*@ behavior wp_typed_ref:
         requires \valid(pa); */
   void write(int kb, int *pa);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
index 6be3aa72874003dc78af525fd268a665aad32185..49db1a0e74357cad28001df60cbecbc64387bd56 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
@@ -251,13 +251,22 @@ Goal Assigns (file tests/wp_hoare/reference_and_struct.i, line 12) in 'reset':
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/reference_and_struct.i:15: Warning: 
+  Memory model hypotheses for function 'reset':
+  /*@ behavior wp_typed_ref:
         requires \valid(p); */
   void reset(struct T *p);
-[wp] Warning: Memory model hypotheses for function 'call_reset_5_tps':
+[wp] tests/wp_hoare/reference_and_struct.i:48: Warning: 
+  Memory model hypotheses for function 'call_reset_5_tps':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated((struct T **)tps + (..), tps[9] + (0 .. 4));
      */
   void call_reset_5_tps(void);
+[wp] tests/wp_hoare/reference_and_struct.i:88: Warning: 
+  Memory model hypotheses for function 'load_5':
+  /*@
+     behavior wp_typed_ref:
+       requires \separated(hp + (..), (int *)reg_load + (..));
+     */
+  void load_5(int *hp);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
index 2801c12e3a4d356ed5996b851196fd7ed9a0015f..e9a8a909640530b5909b8fe20599229d74472b18 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
@@ -401,15 +401,32 @@ Goal Instance of 'Pre-condition (file tests/wp_hoare/reference_array.i, line 9)
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'load_1_5':
+[wp] tests/wp_hoare/reference_array.i:24: Warning: 
+  Memory model hypotheses for function 'load_5':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
+       requires \separated(hp + (..), (int *)reg_load + (..));
+     */
+  void load_5(int *hp);
+[wp] tests/wp_hoare/reference_array.i:31: Warning: 
+  Memory model hypotheses for function 'add_5':
+  /*@
+     behavior wp_typed_ref:
+       requires
+         \separated(gp + (..), (int *)reg_load + (..), (int *)reg_add + (..));
+     */
+  void add_5(int *gp);
+[wp] tests/wp_hoare/reference_array.i:45: Warning: 
+  Memory model hypotheses for function 'load_1_5':
+  /*@
+     behavior wp_typed_ref:
        requires \separated(lp + (..), (int *)reg_load + (..));
      */
   void load_1_5(int (*lp)[5]);
-[wp] Warning: Memory model hypotheses for function 'add_1_5':
+[wp] tests/wp_hoare/reference_array.i:52: Warning: 
+  Memory model hypotheses for function 'add_1_5':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires
          \separated(ap + (..), (int *)reg_load + (..), (int *)reg_add + (..));
      */
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
index 2c5447e5d1d9013e345c34ecb12cebb4310f5712..576a7de621ccb62b85b0a62392d20f0042b7c374 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
@@ -37,3 +37,8 @@ Goal Post-condition (file tests/wp_hoare/reference_array_simple.i, line 39) in '
 Prove: true.
 
 ------------------------------------------------------------
+[wp] tests/wp_hoare/reference_array_simple.i:40: Warning: 
+  Memory model hypotheses for function 'call_f3':
+  /*@ behavior wp_typed_ref:
+        ensures \separated(\result, (int **)tp + (..)); */
+  int *call_f3(void);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
index 59c0568ee15ab1f2f1a4475f688e303403a07b4b..b99e101310280266d0fc3cf756af8bf32fabd5d8 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
@@ -68,25 +68,28 @@ Assume { (* Heap *) Type: (region(c.base) <= 0) /\ (region(d.base) <= 0). }
 Prove: d != c.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
+[wp] tests/wp_hoare/refguards.i:10: Warning: 
+  Memory model hypotheses for function 'f':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(c, d, {a + (..), b + (..)});
        requires \valid(c);
        requires \valid(d);
      */
   void f(int *a, int *b, int *c, int *d, int k);
-[wp] Warning: Memory model hypotheses for function 'h':
+[wp] tests/wp_hoare/refguards.i:25: Warning: 
+  Memory model hypotheses for function 'h':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(c, d);
        requires \valid(c);
        requires \valid(d);
      */
   void h(int *c, int *d, int k);
-[wp] Warning: Memory model hypotheses for function 's':
+[wp] tests/wp_hoare/refguards.i:39: Warning: 
+  Memory model hypotheses for function 's':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(c, d);
        requires \valid(c);
        requires \valid(d);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
index 33a25d793ff22746cb810bbf039b5d65e0bc4bf5..ca6a95729cf10ea40560483fdf25db1e55cf903c 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
@@ -48,51 +48,59 @@
   comprehension_alias       3        -        3       100%
   union_alias               3        -        3       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:17: Warning: 
+  Memory model hypotheses for function 'global_alias':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated(g_alias, (int *)global + (..), &g_alias);
      */
   void global_alias(void);
-[wp] Warning: Memory model hypotheses for function 'global_no_alias':
-  /*@ behavior typed:
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:24: Warning: 
+  Memory model hypotheses for function 'global_no_alias':
+  /*@ behavior wp_typed:
         requires \separated(g_alias, &g_alias); */
   void global_no_alias(void);
-[wp] Warning: Memory model hypotheses for function 'formal_alias':
-  /*@ behavior typed:
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:32: Warning: 
+  Memory model hypotheses for function 'formal_alias':
+  /*@ behavior wp_typed:
         requires \separated(f_alias, (int *)global + (..)); */
   void formal_alias(int *f_alias);
-[wp] Warning: Memory model hypotheses for function 'formal_alias_array':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:48: Warning: 
+  Memory model hypotheses for function 'formal_alias_array':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated((int *)global + (..), &(*alias_array)[0 .. 1]);
        requires \separated(alias_array + (..), (int *)global + (..));
      */
   void formal_alias_array(int (*alias_array)[2]);
-[wp] Warning: Memory model hypotheses for function 'field_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:61: Warning: 
+  Memory model hypotheses for function 'field_alias':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated((int *)global + (..), &x->x);
        requires \separated(x, (int *)global + (..));
      */
   void field_alias(struct X *x);
-[wp] Warning: Memory model hypotheses for function 'field_range_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:73: Warning: 
+  Memory model hypotheses for function 'field_range_alias':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated((int *)global + (..), &(x + (0 .. 3))->x);
        requires \separated(x + (..), (int *)global + (..));
      */
   void field_range_alias(struct X *x);
-[wp] Warning: Memory model hypotheses for function 'set_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:81: Warning: 
+  Memory model hypotheses for function 'set_alias':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
        requires \separated(f_alias, (int *)global + (..), &g_alias);
      */
   void set_alias(int *f_alias);
-[wp] Warning: Memory model hypotheses for function 'comprehension_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:92: Warning: 
+  Memory model hypotheses for function 'comprehension_alias':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires
          \separated(
            (int *)global + (..), &g_alias,
@@ -100,9 +108,10 @@
            );
      */
   void comprehension_alias(void);
-[wp] Warning: Memory model hypotheses for function 'union_alias':
+[wp] tests/wp_hoare/alias_assigns_hypotheses.i:102: Warning: 
+  Memory model hypotheses for function 'union_alias':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated((int *)global + (..), &g_alias, {g_alias, f_alias});
        requires \separated(f_alias, (int *)global + (..), &g_alias);
      */
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
index 48e1936e19564287ad810f53ddca2ccc7767dc19..8d3ab297b0161e20ed2a81b25a6f776b2f30112d 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
@@ -26,15 +26,18 @@
   formal                    2        -        2       100%
   global                    2        -        2       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/byref.i:14: Warning: 
+  Memory model hypotheses for function 'f':
+  /*@ behavior wp_typed_ref:
         requires \valid(r); */
   void f(int *r);
-[wp] Warning: Memory model hypotheses for function 'wrong_without_ref':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/byref.i:20: Warning: 
+  Memory model hypotheses for function 'wrong_without_ref':
+  /*@ behavior wp_typed_ref:
         requires \valid(q); */
   int wrong_without_ref(int *q);
-[wp] Warning: Memory model hypotheses for function 'pointer':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/byref.i:31: Warning: 
+  Memory model hypotheses for function 'pointer':
+  /*@ behavior wp_typed_ref:
         requires \valid(q); */
   int pointer(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
index d97c3812bd67b8c5da17e69e66ce4c1cbed3317e..ab588be9a5c14dfaecd979bc01834341e6c05cef 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
@@ -99,11 +99,38 @@
   g                         4        -        4       100%
   array_in_struct_param     2        -        2       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'ref_bd':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var.i:12: Warning: 
+  Memory model hypotheses for function 'ref_ctr':
+  /*@ behavior wp_typed_ref:
+        requires \valid(p); */
+  int ref_ctr(int *p);
+[wp] tests/wp_hoare/dispatch_var.i:44: Warning: 
+  Memory model hypotheses for function 'ref_bd':
+  /*@ behavior wp_typed_ref:
         requires \valid(q); */
   int ref_bd(int *q);
-[wp] Warning: Memory model hypotheses for function 'g':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var.i:83: Warning: 
+  Memory model hypotheses for function 'ref_valid':
+  /*@ behavior wp_typed_ref:
+        requires \valid(p1); */
+  int ref_valid(int *p1);
+[wp] tests/wp_hoare/dispatch_var.i:133: Warning: 
+  Memory model hypotheses for function 'ref_ctr_nr':
+  /*@
+     behavior wp_typed_ref:
+       requires \separated(ref, ref1, ref2);
+       requires \valid(ref);
+       requires \valid(ref1);
+       requires \valid(ref2);
+     */
+  int ref_ctr_nr(int *ref, int *ref1, int *ref2);
+[wp] tests/wp_hoare/dispatch_var.i:158: Warning: 
+  Memory model hypotheses for function 'ref_ctr_nstars':
+  /*@ behavior wp_typed_ref:
+        requires \valid(pp); */
+  int ref_ctr_nstars(int **pp);
+[wp] tests/wp_hoare/dispatch_var.i:194: Warning: 
+  Memory model hypotheses for function 'g':
+  /*@ behavior wp_typed_ref:
         requires \valid(pg); */
   int g(int *pg);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
index b5878139820eb2eed4ceb79df18a6690a4635426..701b7f065df03139920f6017569bbcc18b9be799 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
@@ -49,19 +49,23 @@
   call_local                8        -        8       100%
   call_param_ref            6        -        6       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:16: Warning: 
+  Memory model hypotheses for function 'reset':
+  /*@ behavior wp_typed_ref:
         requires \valid(rp); */
   void reset(int *rp);
-[wp] Warning: Memory model hypotheses for function 'incr':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:23: Warning: 
+  Memory model hypotheses for function 'incr':
+  /*@ behavior wp_typed_ref:
         requires \valid(ip); */
   void incr(int *ip);
-[wp] Warning: Memory model hypotheses for function 'load':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:31: Warning: 
+  Memory model hypotheses for function 'load':
+  /*@ behavior wp_typed_ref:
         requires \valid(lp); */
   int load(int *lp);
-[wp] Warning: Memory model hypotheses for function 'call_param_ref':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:70: Warning: 
+  Memory model hypotheses for function 'call_param_ref':
+  /*@ behavior wp_typed_ref:
         requires \valid(q); */
   int call_param_ref(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
index 7a50ede52eb9de48083e80185e8fbe5291b9697e..699d53b416274a7ffe806af5c041dfef6293f5a0 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
@@ -49,19 +49,23 @@
   call_local                8        -        8       100%
   call_param_ref            6        -        6       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:16: Warning: 
+  Memory model hypotheses for function 'reset':
+  /*@ behavior wp_typed_ref:
         requires \valid(rp); */
   void reset(int *rp);
-[wp] Warning: Memory model hypotheses for function 'incr':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:23: Warning: 
+  Memory model hypotheses for function 'incr':
+  /*@ behavior wp_typed_ref:
         requires \valid(ip); */
   void incr(int *ip);
-[wp] Warning: Memory model hypotheses for function 'load':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:31: Warning: 
+  Memory model hypotheses for function 'load':
+  /*@ behavior wp_typed_ref:
         requires \valid(lp); */
   int load(int *lp);
-[wp] Warning: Memory model hypotheses for function 'call_param_ref':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/dispatch_var2.i:70: Warning: 
+  Memory model hypotheses for function 'call_param_ref':
+  /*@ behavior wp_typed_ref:
         requires \valid(q); */
   int call_param_ref(int *q);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/memory_hypotheses_checking.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/memory_hypotheses_checking.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6a5957ad9bc912905cd60d35a230bb32192e39ea
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/memory_hypotheses_checking.res.oracle
@@ -0,0 +1,75 @@
+# frama-c -wp -wp-model 'Typed (Ref)' [...]
+[kernel] Parsing tests/wp_hoare/memory_hypotheses_checking.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 50 goals scheduled
+[wp] [Qed] Goal typed_ref_sep_assigns : Valid
+[wp] [Qed] Goal typed_ref_call_sep_ok_assigns_exit : Valid
+[wp] [Qed] Goal typed_ref_call_sep_ok_assigns_normal : Valid
+[wp] [Qed] Goal typed_ref_call_sep_ok_call_sep_wp_typed_ref_requires : Valid
+[wp] [Qed] Goal typed_ref_call_sep_ok_call_sep_wp_typed_ref_requires_2 : Valid
+[wp] [Qed] Goal typed_ref_call_sep_bad_sep_assigns_exit : Valid
+[wp] [Qed] Goal typed_ref_call_sep_bad_sep_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_ref_call_sep_bad_sep_call_sep_wp_typed_ref_requires : Unsuccess
+[wp] [Qed] Goal typed_ref_call_sep_bad_sep_call_sep_wp_typed_ref_requires_2 : Valid
+[wp] [Qed] Goal typed_ref_call_sep_bad_valid_assigns_exit_part1 : Valid
+[wp] [Qed] Goal typed_ref_call_sep_bad_valid_assigns_exit_part2 : Valid
+[wp] [Qed] Goal typed_ref_call_sep_bad_valid_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_ref_call_sep_bad_valid_assigns_normal_part2 : Valid
+[wp] [Qed] Goal typed_ref_call_sep_bad_valid_call_sep_wp_typed_ref_requires : Valid
+[wp] [Alt-Ergo] Goal typed_ref_call_sep_bad_valid_call_sep_wp_typed_ref_requires_2 : Unsuccess
+[wp] [Qed] Goal typed_ref_gptr_sep_assigns : Valid
+[wp] [Qed] Goal typed_ref_call_gptr_sep_ok_assigns_exit : Valid
+[wp] [Qed] Goal typed_ref_call_gptr_sep_ok_assigns_normal : Valid
+[wp] [Qed] Goal typed_ref_call_gptr_sep_ok_call_gptr_sep_wp_typed_ref_requires : Valid
+[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_ok_call_gptr_sep_wp_typed_ref_requires_2 : Valid
+[wp] [Qed] Goal typed_ref_call_gptr_sep_bad_assigns_exit : Valid
+[wp] [Qed] Goal typed_ref_call_gptr_sep_bad_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_bad_call_gptr_sep_wp_typed_ref_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_bad_call_gptr_sep_wp_typed_ref_requires_2 : Valid
+[wp] [Qed] Goal typed_ref_assigns_ptr_assigns : Valid
+[wp] [Qed] Goal typed_ref_call_assigns_ptr_ok_assigns_exit : Valid
+[wp] [Qed] Goal typed_ref_call_assigns_ptr_ok_assigns_normal : Valid
+[wp] [Qed] Goal typed_ref_call_assigns_ptr_ok_call_assigns_ptr_wp_typed_ref_requires : Valid
+[wp] [Qed] Goal typed_ref_call_assigns_ptr_ok_call_assigns_ptr_wp_typed_ref_requires_2 : Valid
+[wp] [Qed] Goal typed_ref_call_assigns_ptr_bad_assigns_exit : Valid
+[wp] [Qed] Goal typed_ref_call_assigns_ptr_bad_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_ref_call_assigns_ptr_bad_call_assigns_ptr_wp_typed_ref_requires : Unsuccess
+[wp] [Qed] Goal typed_ref_call_assigns_ptr_bad_call_assigns_ptr_wp_typed_ref_requires_2 : Valid
+[wp] [Qed] Goal typed_ref_add_return_ok_ensures : Valid
+[wp] [Qed] Goal typed_ref_add_return_ok_assigns : Valid
+[wp] [Qed] Goal typed_ref_add_return_ok_wp_typed_ref_ensures : Valid
+[wp] [Qed] Goal typed_ref_call_add_return_ok_assigns_exit : Valid
+[wp] [Qed] Goal typed_ref_call_add_return_ok_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_ref_call_add_return_ok_assigns_normal_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_ref_call_add_return_ok_assigns_normal_part3 : Valid
+[wp] [Qed] Goal typed_ref_call_add_return_ok_call_add_return_ok_wp_typed_ref_requires : Valid
+[wp] [Qed] Goal typed_ref_call_add_return_ok_call_add_return_ok_wp_typed_ref_requires_2 : Valid
+[wp] [Qed] Goal typed_ref_call_add_return_bad_assigns_exit : Valid
+[wp] [Qed] Goal typed_ref_call_add_return_bad_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_ref_call_add_return_bad_assigns_normal_part2 : Valid
+[wp] [Qed] Goal typed_ref_call_add_return_bad_assigns_normal_part3 : Valid
+[wp] [Alt-Ergo] Goal typed_ref_call_add_return_bad_call_add_return_ok_wp_typed_ref_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ref_call_add_return_bad_call_add_return_ok_wp_typed_ref_requires_2 : Unsuccess
+[wp] [Qed] Goal typed_ref_bad_return_formal_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_ref_bad_return_formal_wp_typed_ref_ensures : Unsuccess
+[wp] Proved goals:   43 / 50
+  Qed:            40 
+  Alt-Ergo:        3  (unsuccess: 7)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  sep                       1        -        1       100%
+  call_sep_ok               4        -        4       100%
+  call_sep_bad_sep          3        -        4      75.0%
+  call_sep_bad_valid        5        -        6      83.3%
+  gptr_sep                  1        -        1       100%
+  call_gptr_sep_ok          3        1        4       100%
+  call_gptr_sep_bad         2        1        4      75.0%
+  assigns_ptr               1        -        1       100%
+  call_assigns_ptr_ok       4        -        4       100%
+  call_assigns_ptr_bad      3        -        4      75.0%
+  add_return_ok             3        -        3       100%
+  call_add_return_ok        5        1        6       100%
+  call_add_return_bad       4        -        6      66.7%
+  bad_return_formal         1        -        2      50.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
index 81897c8db12744ff443786b8e730f7f1adcccc89..6fa2c547d939685057c4e3ce840a76ab810eb7e8 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
@@ -36,15 +36,32 @@
   call_global               5        -        5       100%
   write                     2        -        2       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'call_f2':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/reference.i:14: Warning: 
+  Memory model hypotheses for function 'f':
+  /*@ behavior wp_typed_ref:
+        requires \valid(p); */
+  int f(int *p);
+[wp] tests/wp_hoare/reference.i:30: Warning: 
+  Memory model hypotheses for function 'f2':
+  /*@
+     behavior wp_typed_ref:
+       requires \separated(p2, q);
+       requires \valid(p2);
+       requires \valid(q);
+     */
+  int f2(int *p2, int *q);
+[wp] tests/wp_hoare/reference.i:37: Warning: 
+  Memory model hypotheses for function 'call_f2':
+  /*@ behavior wp_typed_ref:
         requires \valid(ptr); */
   int call_f2(int *ptr, int y);
-[wp] Warning: Memory model hypotheses for function 'call_global':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/reference.i:48: Warning: 
+  Memory model hypotheses for function 'call_global':
+  /*@ behavior wp_typed_ref:
         requires \valid(gl); */
   int call_global(void);
-[wp] Warning: Memory model hypotheses for function 'write':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/reference.i:60: Warning: 
+  Memory model hypotheses for function 'write':
+  /*@ behavior wp_typed_ref:
         requires \valid(pa); */
   void write(int kb, int *pa);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
index 9da7484d4d2dbe1ef5e6c0d68b4f796d572e69ac..a4e3ed789ba72a4140a2684e13f6d9013acdb46b 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
@@ -49,13 +49,22 @@
   call_on_array_in_struct_global   3   1      4       100%
   call_array_in_struct_param   5     -        5       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
-  /*@ behavior typed_ref:
+[wp] tests/wp_hoare/reference_and_struct.i:15: Warning: 
+  Memory model hypotheses for function 'reset':
+  /*@ behavior wp_typed_ref:
         requires \valid(p); */
   void reset(struct T *p);
-[wp] Warning: Memory model hypotheses for function 'call_reset_5_tps':
+[wp] tests/wp_hoare/reference_and_struct.i:48: Warning: 
+  Memory model hypotheses for function 'call_reset_5_tps':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated((struct T **)tps + (..), tps[9] + (0 .. 4));
      */
   void call_reset_5_tps(void);
+[wp] tests/wp_hoare/reference_and_struct.i:88: Warning: 
+  Memory model hypotheses for function 'load_5':
+  /*@
+     behavior wp_typed_ref:
+       requires \separated(hp + (..), (int *)reg_load + (..));
+     */
+  void load_5(int *hp);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
index 5fa325b91701864750b7557fa6443415d74dbdb9..2df672162a74515bca9c937e13606ac49af6b508 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
@@ -51,15 +51,32 @@
   calls_on_array_dim_2_to_1   5      3        8       100%
   calls_on_array_dim_2      5        3        8       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'load_1_5':
+[wp] tests/wp_hoare/reference_array.i:24: Warning: 
+  Memory model hypotheses for function 'load_5':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
+       requires \separated(hp + (..), (int *)reg_load + (..));
+     */
+  void load_5(int *hp);
+[wp] tests/wp_hoare/reference_array.i:31: Warning: 
+  Memory model hypotheses for function 'add_5':
+  /*@
+     behavior wp_typed_ref:
+       requires
+         \separated(gp + (..), (int *)reg_load + (..), (int *)reg_add + (..));
+     */
+  void add_5(int *gp);
+[wp] tests/wp_hoare/reference_array.i:45: Warning: 
+  Memory model hypotheses for function 'load_1_5':
+  /*@
+     behavior wp_typed_ref:
        requires \separated(lp + (..), (int *)reg_load + (..));
      */
   void load_1_5(int (*lp)[5]);
-[wp] Warning: Memory model hypotheses for function 'add_1_5':
+[wp] tests/wp_hoare/reference_array.i:52: Warning: 
+  Memory model hypotheses for function 'add_1_5':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires
          \separated(ap + (..), (int *)reg_load + (..), (int *)reg_add + (..));
      */
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle
index b5390221da4d396ad6e3c0fdb1de95711c8dad3d..7b00985377bce93debde6c76f033a655f68b5e06 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle
@@ -14,3 +14,8 @@
   call_f2                   1        -        1       100%
   call_f3                   1        -        1       100%
 ------------------------------------------------------------
+[wp] tests/wp_hoare/reference_array_simple.i:40: Warning: 
+  Memory model hypotheses for function 'call_f3':
+  /*@ behavior wp_typed_ref:
+        ensures \separated(\result, (int **)tp + (..)); */
+  int *call_f3(void);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
index 02a4bffe2c4d64132a21a44142ddcf9bf1b3f99f..3fba6a750b4f8d97faebe8f14aca0aa61237fea0 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
@@ -22,25 +22,28 @@
   h                         1        -        1       100%
   s                         5        -        6      83.3%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
+[wp] tests/wp_hoare/refguards.i:10: Warning: 
+  Memory model hypotheses for function 'f':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(c, d, {a + (..), b + (..)});
        requires \valid(c);
        requires \valid(d);
      */
   void f(int *a, int *b, int *c, int *d, int k);
-[wp] Warning: Memory model hypotheses for function 'h':
+[wp] tests/wp_hoare/refguards.i:25: Warning: 
+  Memory model hypotheses for function 'h':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(c, d);
        requires \valid(c);
        requires \valid(d);
      */
   void h(int *c, int *d, int k);
-[wp] Warning: Memory model hypotheses for function 's':
+[wp] tests/wp_hoare/refguards.i:39: Warning: 
+  Memory model hypotheses for function 's':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(c, d);
        requires \valid(c);
        requires \valid(d);
diff --git a/src/plugins/wp/tests/wp_plugin/model.i b/src/plugins/wp/tests/wp_plugin/model.i
index 81b49ed20d473590181d159b37f404a4564e5395..fd0dd051a717b1544e9f13d4c0be5d06f2c410fa 100644
--- a/src/plugins/wp/tests/wp_plugin/model.i
+++ b/src/plugins/wp/tests/wp_plugin/model.i
@@ -1,5 +1,5 @@
 /* run.config
-   CMD: @frama-c@ -wp-share ./share -wp-msg-key cluster,shell,print-generated -wp-prover why3
+   CMD: @frama-c@ -wp-share ./share -wp-msg-key cluster,shell,print-generated -wp-prover why3 -wp-warn-key "pedantic-assigns=inactive"
    OPT: -wp-model Typed -wp -wp-gen -wp-print -then -wp-model Typed+ref -wp -wp-gen -wp-print
 */
 
diff --git a/src/plugins/wp/tests/wp_plugin/nosession.i b/src/plugins/wp/tests/wp_plugin/nosession.i
index 46b01faf9e1da3618797ea1027ac7f7fd80fd9f6..bb038ffd831fcb13d4ecbfeeef7154c92d576820 100644
--- a/src/plugins/wp/tests/wp_plugin/nosession.i
+++ b/src/plugins/wp/tests/wp_plugin/nosession.i
@@ -3,7 +3,7 @@
 */
 
 /* run.config_qualif
-   CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp-share ./share -wp-msg-key shell
+   CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp-share ./share -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive
    OPT: -wp -wp-prover alt-ergo -wp-session shall_not_exists_dir -wp-cache offline -wp-no-cache-env
    COMMENT: The session directory shall not be created
  */
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
index e71c6e9ae9aea0d46a37b93de7f0bd295d0e1fb5..ad37a67830bf85dd03dd6f3a058108f367ee9ea3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -372,19 +372,23 @@ Tags: Call h1.
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'guarded_call':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/dynamic.i:41: Warning: 
+  Memory model hypotheses for function 'guarded_call':
+  /*@ behavior wp_typed:
         requires \separated(p, &X); */
   void guarded_call(struct S *p);
-[wp] Warning: Memory model hypotheses for function 'behavior':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/dynamic.i:63: Warning: 
+  Memory model hypotheses for function 'behavior':
+  /*@ behavior wp_typed:
         requires \separated(p + (..), &X1); */
   int behavior(int (*p)(void));
-[wp] Warning: Memory model hypotheses for function 'some_behaviors':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/dynamic.i:76: Warning: 
+  Memory model hypotheses for function 'some_behaviors':
+  /*@ behavior wp_typed:
         requires \separated(p + (..), &X1); */
   int some_behaviors(int (*p)(void));
-[wp] Warning: Memory model hypotheses for function 'missing_context':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/dynamic.i:85: Warning: 
+  Memory model hypotheses for function 'missing_context':
+  /*@ behavior wp_typed:
         requires \separated(p, &X1); */
   int missing_context(int (*p)(void));
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
index a3bcc315fdac6c66cfa7881ddf59d613adc25e89..07bb9ac0b9f9b3ef4f2352b015497127b6465484 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
@@ -100,11 +100,13 @@ Assume { (* Heap *) Type: linked(Malloc_0). }
 Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), -5), 10).
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f1_ok':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/overassign.i:14: Warning: 
+  Memory model hypotheses for function 'f1_ok':
+  /*@ behavior wp_typed:
         requires \separated(p + (0 .. 9), &p); */
   void f1_ok(void);
-[wp] Warning: Memory model hypotheses for function 'f2_ok':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/overassign.i:17: Warning: 
+  Memory model hypotheses for function 'f2_ok':
+  /*@ behavior wp_typed:
         requires \separated(p + (10 .. 19), &p); */
   void f2_ok(void);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
index fc8605283009333c1cc2ed29037b8ce30203b737..19f37ddeabbbc865df8040fd01e2f84dde96bd3c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
@@ -32,10 +32,11 @@ Call Effect at line 14
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'receive':
+[wp] tests/wp_plugin/post_assigns.i:12: Warning: 
+  Memory model hypotheses for function 'receive':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated(message + (..), &size);
-       requires \separated(message + (0 .. \at(size,Post)), &size);
+       ensures \separated(message + (0 .. \at(size,Post)), &size);
      */
   void receive(int n, char *message);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
index fdfb80b6c398acb479a2221181fa65057e0b48bf..e5d8aa84c061c2c39a06fe1f5257ffadeaea8003 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
@@ -66,50 +66,59 @@ Goal Post-condition (file tests/wp_plugin/sep.i, line 48) in 'f8_pq_a':
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f2_p_a':
-  /*@ behavior typed_caveat:
+[wp] tests/wp_plugin/sep.i:18: Warning: 
+  Memory model hypotheses for function 'f2_p_a':
+  /*@ behavior wp_typed_caveat:
         requires \separated(p, &a);
         requires \valid(p); */
   void f2_p_a(int *p);
-[wp] Warning: Memory model hypotheses for function 'f3_p_ab':
-  /*@ behavior typed_caveat:
-        requires \separated(p, &a, &b);
-        requires \valid(p); */
+[wp] tests/wp_plugin/sep.i:22: Warning: 
+  Memory model hypotheses for function 'f3_p_ab':
+  /*@
+     behavior wp_typed_caveat:
+       requires \separated(p, &a, &b);
+       requires \valid(p);
+     */
   void f3_p_ab(int *p);
-[wp] Warning: Memory model hypotheses for function 'f4_pq_ab':
+[wp] tests/wp_plugin/sep.i:26: Warning: 
+  Memory model hypotheses for function 'f4_pq_ab':
   /*@
-     behavior typed_caveat:
+     behavior wp_typed_caveat:
        requires \separated(p, q, &a, &b);
        requires \valid(p);
        requires \valid(q);
      */
   void f4_pq_ab(int *p, int *q);
-[wp] Warning: Memory model hypotheses for function 'f5_pq':
+[wp] tests/wp_plugin/sep.i:30: Warning: 
+  Memory model hypotheses for function 'f5_pq':
   /*@
-     behavior typed_caveat:
+     behavior wp_typed_caveat:
        requires \separated(p, q);
        requires \valid(p);
        requires \valid(q);
      */
   void f5_pq(int *p, int *q);
-[wp] Warning: Memory model hypotheses for function 'f6_Pa':
+[wp] tests/wp_plugin/sep.i:34: Warning: 
+  Memory model hypotheses for function 'f6_Pa':
   /*@
-     behavior typed_caveat:
+     behavior wp_typed_caveat:
        requires \separated(p + (..), &a);
        requires \valid(p + (..));
      */
   void f6_Pa(int *p, int k);
-[wp] Warning: Memory model hypotheses for function 'f7_pq_ad':
+[wp] tests/wp_plugin/sep.i:43: Warning: 
+  Memory model hypotheses for function 'f7_pq_ad':
   /*@
-     behavior typed_caveat:
+     behavior wp_typed_caveat:
        requires \separated(p, q, &a, &d);
        requires \valid(p);
        requires \valid(q);
      */
   void f7_pq_ad(int *p, int *q);
-[wp] Warning: Memory model hypotheses for function 'f8_pq_a':
+[wp] tests/wp_plugin/sep.i:49: Warning: 
+  Memory model hypotheses for function 'f8_pq_a':
   /*@
-     behavior typed_caveat:
+     behavior wp_typed_caveat:
        requires \separated(p, q, &a);
        requires \valid(p);
        requires \valid(q);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle
index fde06aafdfce56ba5edb411f57ea36f78d4cec28..00afcb0afdf228e6888c4e919210cda1e0acfc7a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle
@@ -42,3 +42,11 @@ Assume {
 Prove: valid_rw(Malloc_0, p, 2).
 
 ------------------------------------------------------------
+[wp] tests/wp_plugin/subset_fopen.c:13: Warning: 
+  Memory model hypotheses for function 'fopen':
+  /*@
+     behavior wp_typed:
+       requires \separated(&_p__fc_fopen, {filename + (..), mode + (..)});
+       ensures \separated(\result, &_p__fc_fopen);
+     */
+  FILE *fopen(char const * __restrict filename, char const * __restrict mode);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
index 8f0c8d4ce8a3ca974c104502d4572ad66bf635a6..2df04eb693e0221ae001c0fbd615d432dec4cd3c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
@@ -35,7 +35,8 @@ Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 35):
 Prove: EqS1_st_v(w, w_1).
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job_struct_assigns':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/volatile.i:32: Warning: 
+  Memory model hypotheses for function 'job_struct_assigns':
+  /*@ behavior wp_typed:
         requires \separated(p, &sv); */
   void job_struct_assigns(struct st_v *p);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
index 8f7b2282f202b7a6ab2c4fb7f9faa450a8594c32..63e2b65a2c49a5ca6bf4edcaf5f179a9121e0b6d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
@@ -69,7 +69,8 @@ tests/wp_plugin/volatile.i:35: warning from wp:
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job_struct_assigns':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/volatile.i:32: Warning: 
+  Memory model hypotheses for function 'job_struct_assigns':
+  /*@ behavior wp_typed:
         requires \separated(p, &sv); */
   void job_struct_assigns(struct st_v *p);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
index 9144906c8da84fbc097b34efdbe590b66f253b4a..e3e408c44c11240b3f222cc20901d0fcf6b2d977 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
@@ -67,19 +67,23 @@
   missing_context           4        -        5      80.0%
   no_call                   4        -        4       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'guarded_call':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/dynamic.i:41: Warning: 
+  Memory model hypotheses for function 'guarded_call':
+  /*@ behavior wp_typed:
         requires \separated(p, &X); */
   void guarded_call(struct S *p);
-[wp] Warning: Memory model hypotheses for function 'behavior':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/dynamic.i:63: Warning: 
+  Memory model hypotheses for function 'behavior':
+  /*@ behavior wp_typed:
         requires \separated(p + (..), &X1); */
   int behavior(int (*p)(void));
-[wp] Warning: Memory model hypotheses for function 'some_behaviors':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/dynamic.i:76: Warning: 
+  Memory model hypotheses for function 'some_behaviors':
+  /*@ behavior wp_typed:
         requires \separated(p + (..), &X1); */
   int some_behaviors(int (*p)(void));
-[wp] Warning: Memory model hypotheses for function 'missing_context':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/dynamic.i:85: Warning: 
+  Memory model hypotheses for function 'missing_context':
+  /*@ behavior wp_typed:
         requires \separated(p, &X1); */
   int missing_context(int (*p)(void));
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
index 5bfb2cf3e3404fc852f21bd6bce54e9d187991a5..76de1d842d7dfc708fbbd538f479ca9b714345e9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
@@ -27,11 +27,13 @@
   f5_ko                     -        -        2       0.0%
   f6_ko                     -        -        2       0.0%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f1_ok':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/overassign.i:14: Warning: 
+  Memory model hypotheses for function 'f1_ok':
+  /*@ behavior wp_typed:
         requires \separated(p + (0 .. 9), &p); */
   void f1_ok(void);
-[wp] Warning: Memory model hypotheses for function 'f2_ok':
-  /*@ behavior typed:
+[wp] tests/wp_plugin/overassign.i:17: Warning: 
+  Memory model hypotheses for function 'f2_ok':
+  /*@ behavior wp_typed:
         requires \separated(p + (10 .. 19), &p); */
   void f2_ok(void);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
index 5f2225e888c8039688ad6f032109704023a8750c..7aee3baaefaec1b15258306f2a55889dd80911ba 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
@@ -14,10 +14,11 @@
  Functions                 WP     Alt-Ergo  Total   Success
   receive                   5        -        5       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'receive':
+[wp] tests/wp_plugin/post_assigns.i:12: Warning: 
+  Memory model hypotheses for function 'receive':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated(message + (..), &size);
-       requires \separated(message + (0 .. \at(size,Post)), &size);
+       ensures \separated(message + (0 .. \at(size,Post)), &size);
      */
   void receive(int n, char *message);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
index 7f76d80b00a10d94eb30f412df38843d33541efa..55f410c2efe359058200eed08eb2f0595a0ab2fc 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
@@ -15,3 +15,11 @@
  Functions                 WP     Alt-Ergo  Total   Success
   f                         3        1        5      80.0%
 ------------------------------------------------------------
+[wp] tests/wp_plugin/subset_fopen.c:13: Warning: 
+  Memory model hypotheses for function 'fopen':
+  /*@
+     behavior wp_typed:
+       requires \separated(&_p__fc_fopen, {filename + (..), mode + (..)});
+       ensures \separated(\result, &_p__fc_fopen);
+     */
+  FILE *fopen(char const * __restrict filename, char const * __restrict mode);
diff --git a/src/plugins/wp/tests/wp_plugin/rte.i b/src/plugins/wp/tests/wp_plugin/rte.i
index 65e8988e572951b8de7ff768207b7c4e88fdfa86..f41d80662719bdfed9a22dd9405c62bee91a106a 100644
--- a/src/plugins/wp/tests/wp_plugin/rte.i
+++ b/src/plugins/wp/tests/wp_plugin/rte.i
@@ -1,5 +1,5 @@
 /* run.config
-   CMD: @frama-c@ -wp -wp-prover none -wp-share ./share -wp-msg-key shell -wp-msg-key rte
+   CMD: @frama-c@ -wp -wp-prover none -wp-share ./share -wp-msg-key shell,rte -wp-warn-key "pedantic-assigns=inactive"
    OPT: -wp-rte -no-warn-invalid-bool -then -print -no-unicode
    OPT: -wp-rte -no-warn-signed-overflow -then -print -no-unicode
    OPT: -wp-rte -warn-unsigned-overflow -then -print -no-unicode
diff --git a/src/plugins/wp/tests/wp_plugin/stmt.c b/src/plugins/wp/tests/wp_plugin/stmt.c
index 58e04b9d85fccbba9f6eb09c1738dffc0c98768c..df45bff806e6f85034d9af3b89d04427f64516dd 100644
--- a/src/plugins/wp/tests/wp_plugin/stmt.c
+++ b/src/plugins/wp/tests/wp_plugin/stmt.c
@@ -4,7 +4,7 @@
 
 /* run.config_qualif
    OPT: -load-module report -then -report
-   EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key shell @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
+   EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-warn-key pedantic-assigns=inactive -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key shell @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
 */
 
 /*@ ensures a > 0 ==> \result == a + b;
diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config
index 36003c91eeff9b752b08515c756f5e0268465e56..57d4ae071a433f4d3cecca0d8a218c0557f02e6d 100644
--- a/src/plugins/wp/tests/wp_region/test_config
+++ b/src/plugins/wp/tests/wp_region/test_config
@@ -1,3 +1,3 @@
 CMD: @frama-c@ -no-autoload-plugins -load-module wp
 LOG: @PTEST_NAME@/region/job.dot
-OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-out @PTEST_DIR@/result/@PTEST_NAME@ -wp-fct job
+OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-out @PTEST_DIR@/result/@PTEST_NAME@ -wp-fct job
diff --git a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
index 1cb5b23e556d9e985e712eca70660864d7d9e896..598ec02c22b31480783d0e71c8ee206b3c3ca225 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
@@ -25,3 +25,19 @@ Assume {
 Prove: `x_2 = `x_1.
 
 ------------------------------------------------------------
+[wp] tests/wp_tip/chunk_printing.i:19: Warning: 
+  Memory model hypotheses for function 'get_int':
+  /*@
+     behavior wp_typed:
+       requires \separated(v, &y);
+       ensures \separated(\result, &y);
+     */
+  int *get_int(struct V *v);
+[wp] tests/wp_tip/chunk_printing.i:25: Warning: 
+  Memory model hypotheses for function 'get_uint':
+  /*@
+     behavior wp_typed:
+       requires \separated(v, &y);
+       ensures \separated(\result, &y);
+     */
+  unsigned int *get_uint(struct V *v);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
index c00b06312b62e50529b76e36b62185d8eeb09d9b..b7a091489fb93752d1a9cc9aca36bad12fb18539 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
@@ -18,3 +18,11 @@ Assume {
 Prove: P_equal(1, 1).
 
 ------------------------------------------------------------
+[wp] tests/wp_typed/mvar.i:8: Warning: 
+  Memory model hypotheses for function 'Write':
+  /*@
+     behavior wp_typed:
+       requires \separated(p + (..), (char *)A + (..));
+       requires \separated(p + (0 ..), (char *)A + (..));
+     */
+  extern void Write(char *p, int n);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
index fef31f965305408e602c2e3191f7fea8c84510e2..a58a157b823fe1a0b4e6ad4fa3dadced366513f7 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
@@ -18,3 +18,11 @@ Assume {
 Prove: P_equal(1, 1).
 
 ------------------------------------------------------------
+[wp] tests/wp_typed/mvar.i:8: Warning: 
+  Memory model hypotheses for function 'Write':
+  /*@
+     behavior wp_typed_ref:
+       requires \separated(p + (..), (char *)A + (..));
+       requires \separated(p + (0 ..), (char *)A + (..));
+     */
+  extern void Write(char *p, int n);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
index d2e3f2a9cd72abe8c290a08496c943a44251a532..8da6181fa48f73c8f2e46181035f04cd3962ddbe 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
@@ -59,3 +59,8 @@ Assume {
 Prove: !valid_rw(Malloc_0[L_y_25 <- 0], a, 1).
 
 ------------------------------------------------------------
+[wp] tests/wp_typed/unit_alloc.i:34: Warning: 
+  Memory model hypotheses for function 'h':
+  /*@ behavior wp_typed:
+        ensures \separated(\result, &x); */
+  int *h(int x);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
index 115e7900443a3b47594946cdc03820b159258291..1444f81cf6e1e9bac9d8b672b5e5dd31bbb95c26 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
@@ -59,3 +59,8 @@ Assume {
 Prove: !valid_rw(Malloc_0[L_y_25 <- 0], a, 1).
 
 ------------------------------------------------------------
+[wp] tests/wp_typed/unit_alloc.i:34: Warning: 
+  Memory model hypotheses for function 'h':
+  /*@ behavior wp_typed_ref:
+        ensures \separated(\result, &x); */
+  int *h(int x);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle
index c0eec98834070f47edced3f7b7288673ae2a08bc..2ffd064c6d514e4f7cb6597ab668144d4c42f52d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle
@@ -10,7 +10,8 @@ Goal Post-condition (file tests/wp_typed/unit_ite.i, line 2) in 'check':
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'check':
-  /*@ behavior typed_ref:
+[wp] tests/wp_typed/unit_ite.i:3: Warning: 
+  Memory model hypotheses for function 'check':
+  /*@ behavior wp_typed_ref:
         requires \valid(p); */
   void check(int x, int *p);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
index 98b60be4d4acc85fc0c73725a7e1ca124159ed51..7a7b1b25d56460d9600a2462fbc1f0b38cc49dd2 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
@@ -26,9 +26,10 @@ Goal Assertion 'PJ' (file tests/wp_typed/unit_labels.i, line 10):
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'duplet':
+[wp] tests/wp_typed/unit_labels.i:7: Warning: 
+  Memory model hypotheses for function 'duplet':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(pi, pj, a + (..));
        requires \valid(pi);
        requires \valid(pj);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle
index 9cd81cf810713b1a3524c268452769cbb34bcf1c..c64b78b42d0c66a04811a8d73c495b3391677218 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle
@@ -17,7 +17,8 @@ Goal Establishment of Invariant (file tests/wp_typed/unit_loopscope.i, line 13):
 Prove: false.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
-  /*@ behavior typed_ref:
+[wp] tests/wp_typed/unit_loopscope.i:9: Warning: 
+  Memory model hypotheses for function 'f':
+  /*@ behavior wp_typed_ref:
         requires \valid(written); */
   void f(unsigned int *written);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle
index b49ad5f8dddc52f47a74259da71cc92795e32b34..a1ac6afa9ad4cade781c71f184ac01d88984ab73 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle
@@ -115,9 +115,10 @@ Effect at line 68
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
+[wp] tests/wp_typed/user_injector.i:58: Warning: 
+  Memory model hypotheses for function 'job':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires
          \separated(
            error, (int *)service_id + (..), (int *)service_result + (..), &seq,
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
index abbc64b85dacff64fa8d779ed0d10ab167bc9959..e571b4fc2cce83e61a9d3f99da28c56e0219ce79 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
@@ -40,9 +40,10 @@ Goal Assigns 'E' in 'swap':
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'swap':
+[wp] tests/wp_typed/user_swap.i:13: Warning: 
+  Memory model hypotheses for function 'swap':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(a, b);
        requires \valid(a);
        requires \valid(b);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
index 65452ad8fe8dcf8a886ab9f392404f71630df81b..78b8c7b8aa18c2c5a17fd72a2676a229852a0754 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
@@ -13,3 +13,11 @@
  Functions                 WP     Alt-Ergo  Total   Success
   Job                       -        1        1       100%
 ------------------------------------------------------------
+[wp] tests/wp_typed/mvar.i:8: Warning: 
+  Memory model hypotheses for function 'Write':
+  /*@
+     behavior wp_typed:
+       requires \separated(p + (..), (char *)A + (..));
+       requires \separated(p + (0 ..), (char *)A + (..));
+     */
+  extern void Write(char *p, int n);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle
index 18546f909a348ac909e1a04f80648b14d3305b68..712b34468831a3e10cca1ff6bcd086bd32b3692c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle
@@ -20,3 +20,8 @@
   g                         1        -        1       100%
   h                         -        1        1       100%
 ------------------------------------------------------------
+[wp] tests/wp_typed/unit_alloc.i:34: Warning: 
+  Memory model hypotheses for function 'h':
+  /*@ behavior wp_typed:
+        ensures \separated(\result, &x); */
+  int *h(int x);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle
index 86359ce6ec2a844ed6a61b3b7b1ff36e8998a6bf..d0b9a9657e2c615dad9eaae6835cce059b2f024d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle
@@ -20,3 +20,8 @@
   g                         1        -        1       100%
   h                         -        1        1       100%
 ------------------------------------------------------------
+[wp] tests/wp_typed/unit_alloc.i:34: Warning: 
+  Memory model hypotheses for function 'h':
+  /*@ behavior wp_typed_ref:
+        ensures \separated(\result, &x); */
+  int *h(int x);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
index 4417ddd127acc3f894426f6829b8d8b4766afaf2..a5bd933b1bcfeaffaa80b436a76fac246c85eddb 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
@@ -14,7 +14,8 @@
  Functions                 WP     Alt-Ergo  Total   Success
   f                         1        -        2      50.0%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
-  /*@ behavior typed_ref:
+[wp] tests/wp_typed/unit_loopscope.i:9: Warning: 
+  Memory model hypotheses for function 'f':
+  /*@ behavior wp_typed_ref:
         requires \valid(written); */
   void f(unsigned int *written);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
index 20fdb332cff1128c6e165033300ad73bfea348fc..68842329caa54bde292887e7f660019aa75204a9 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
@@ -29,9 +29,10 @@
  Functions                 WP     Alt-Ergo  Total   Success
   job                      20        -       20       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
+[wp] tests/wp_typed/user_injector.i:58: Warning: 
+  Memory model hypotheses for function 'job':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires
          \separated(
            error, (int *)service_id + (..), (int *)service_result + (..), &seq,
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
index 93b4fb88899dc8766046ac491738f5ce0f679df6..ad44942e79c58b466fce26436dad805a9512eab4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
@@ -25,9 +25,10 @@
  Functions                 WP     Alt-Ergo  Total   Success
   job                      16        -       16       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
+[wp] tests/wp_typed/user_injector.i:58: Warning: 
+  Memory model hypotheses for function 'job':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires
          \separated(
            error, (int *)service_id + (..), (int *)service_result + (..), &seq,
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
index 1a4f9fd916dc87ddda1ca6877dad7c9460da89d1..d37ff58f250004ef4d1fb0e0262f230040f9f336 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
@@ -16,9 +16,10 @@
   swap                      3        -        3       100%
   main                      3        -        3       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'swap':
+[wp] tests/wp_typed/user_swap.i:13: Warning: 
+  Memory model hypotheses for function 'swap':
   /*@
-     behavior typed_ref:
+     behavior wp_typed_ref:
        requires \separated(a, b);
        requires \valid(a);
        requires \valid(b);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
index b4a9f732ab57d81a13ed8b594f0a2c991ce7980e..7f6f4e1316280036e5df8c8d578bbb2b5e487f1b 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
@@ -68,25 +68,28 @@ Assume {
 Prove: P_OBS(x_2, x_3, x_4).
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'implicit':
+[wp] tests/wp_usage/caveat.i:17: Warning: 
+  Memory model hypotheses for function 'implicit':
   /*@
-     behavior typed_caveat:
+     behavior wp_typed_caveat:
        requires \separated(a, r);
        requires \valid(a);
        requires \valid(r);
      */
   void implicit(struct S *a, int *r);
-[wp] Warning: Memory model hypotheses for function 'explicit':
+[wp] tests/wp_usage/caveat.i:32: Warning: 
+  Memory model hypotheses for function 'explicit':
   /*@
-     behavior typed_caveat:
+     behavior wp_typed_caveat:
        requires \separated(a, r);
        requires \valid(a);
        requires \valid(r);
      */
   void explicit(struct S *a, int *r);
-[wp] Warning: Memory model hypotheses for function 'observer':
+[wp] tests/wp_usage/caveat.i:47: Warning: 
+  Memory model hypotheses for function 'observer':
   /*@
-     behavior typed_caveat:
+     behavior wp_typed_caveat:
        requires \separated(a, r);
        requires \valid(a);
        requires \valid(r);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
index c4439057d741e22283cc74f24ba42ade076657f5..bd126749ac28da329e21c30afd6113528bb91909 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
@@ -97,9 +97,10 @@ Effect at line 25
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
+[wp] tests/wp_usage/caveat2.i:17: Warning: 
+  Memory model hypotheses for function 'job':
   /*@
-     behavior typed_caveat:
+     behavior wp_typed_caveat:
        requires \separated(p, b + (..));
        requires \valid(b + (..));
        requires \valid(p);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
index d15c7f73b49722c9b671268208fb84518250c69e..82cb1e098dcda026410bc2a0a3703518227ddfac 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
@@ -154,7 +154,8 @@ Effect at line 24
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
-  /*@ behavior typed_caveat:
+[wp] tests/wp_usage/caveat_range.i:16: Warning: 
+  Memory model hypotheses for function 'reset':
+  /*@ behavior wp_typed_caveat:
         requires \valid(p + (..)); */
   void reset(struct S *p);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle
index 0243fc9b1786ecd5d354be89f6212db6e707dc29..1f25e6893d061ae45ba834ecb380c4a3d8acfdb3 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle
@@ -19,7 +19,8 @@ Goal Instance of 'Pre-condition (file tests/wp_usage/global.c, line 14) in 'foo'
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'foo':
-  /*@ behavior typed:
+[wp] tests/wp_usage/global.c:16: Warning: 
+  Memory model hypotheses for function 'foo':
+  /*@ behavior wp_typed:
         requires \separated(a, &GLOBAL); */
   void foo(int *a);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
index 6d03c92ee56c2b284a167e6eb2a17091cf840e08..3489aa287459e7a28ac2466a765b8a28f44a3e89 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
@@ -19,8 +19,11 @@ Goal Instance of 'Pre-condition (file tests/wp_usage/global.c, line 14) in 'foo'
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'foo':
-  /*@ behavior typed_ref:
-        requires \separated(a, &GLOBAL);
-        requires \valid(a); */
+[wp] tests/wp_usage/global.c:16: Warning: 
+  Memory model hypotheses for function 'foo':
+  /*@
+     behavior wp_typed_ref:
+       requires \separated(a, &GLOBAL);
+       requires \valid(a);
+     */
   void foo(int *a);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
index 71a2cdaccb60d2b018b7d2eaa18b5ce4cbc57b8c..c15cbee10c3bd49b6bdb5e70c103a1ebac5cb9ff 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
@@ -167,9 +167,10 @@ Effect at line 59
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'memcpy_context_vars':
+[wp] tests/wp_usage/issue-189-bis.i:48: Warning: 
+  Memory model hypotheses for function 'memcpy_context_vars':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated(src, dst);
        requires \valid(dst);
        requires \valid(src);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
index 0b9c5b7d7e604f10f869d9801c20aba6bed6f7ea..5cd9f57c585ba881735715218f8d80be0aab2e2d 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
@@ -22,9 +22,10 @@ Effect at line 17
 Prove: true.
 
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'f':
+[wp] tests/wp_usage/issue-189.i:16: Warning: 
+  Memory model hypotheses for function 'f':
   /*@
-     behavior typed_caveat:
+     behavior wp_typed_caveat:
        requires \separated(ptr, src);
        requires \valid(ptr);
      */
diff --git a/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle
index a22e16a5c310bb1d8147af73a86dcb698042c5d4..7d8d28eb790f018916ce262e1b7e0edf862b4c89 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle
@@ -17,3 +17,8 @@ Goal Pre-condition (file tests/wp_usage/ref-usage-lemmas.i, line 30) in 'main':
 Prove: true.
 
 ------------------------------------------------------------
+[wp] tests/wp_usage/ref-usage-lemmas.i:26: Warning: 
+  Memory model hypotheses for function 'foo':
+  /*@ behavior wp_typed:
+        requires \separated(x, &b); */
+  void foo(int *x);
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
index 6c1a2b8821961dcbaf564314c55b39872a1ef6bc..86f77567c02d0caf7aab6020ddf1b5cb07631098 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
@@ -20,9 +20,10 @@
  Functions                 WP     Alt-Ergo  Total   Success
   job                       6        3        9       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'job':
+[wp] tests/wp_usage/caveat2.i:17: Warning: 
+  Memory model hypotheses for function 'job':
   /*@
-     behavior typed_caveat:
+     behavior wp_typed_caveat:
        requires \separated(p, b + (..));
        requires \valid(b + (..));
        requires \valid(p);
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
index 050004166a73ac6f66a23eadb0131b5b510a598c..9a6fb8012b0a3107d34e7c4cc2c8de9d47b70141 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
@@ -22,7 +22,8 @@
  Functions                 WP     Alt-Ergo  Total   Success
   reset                     7        5       12       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'reset':
-  /*@ behavior typed_caveat:
+[wp] tests/wp_usage/caveat_range.i:16: Warning: 
+  Memory model hypotheses for function 'reset':
+  /*@ behavior wp_typed_caveat:
         requires \valid(p + (..)); */
   void reset(struct S *p);
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
index c2679dccf0ddd1ca3dbebec9e4eb51a652063629..e73a38c074fdf04dbda90f7e6ef41eaca850a587 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
@@ -20,9 +20,10 @@
  Functions                 WP     Alt-Ergo  Total   Success
   memcpy_context_vars       7        3       10       100%
 ------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'memcpy_context_vars':
+[wp] tests/wp_usage/issue-189-bis.i:48: Warning: 
+  Memory model hypotheses for function 'memcpy_context_vars':
   /*@
-     behavior typed:
+     behavior wp_typed:
        requires \separated(src, dst);
        requires \valid(dst);
        requires \valid(src);
diff --git a/src/plugins/wp/tests/wp_usage/save_load.i b/src/plugins/wp/tests/wp_usage/save_load.i
index 544dae3b38c163cf97bf18d231031964ab6bc82e..8e908e8b69636dbd586fb832035975253a0cb13f 100644
--- a/src/plugins/wp/tests/wp_usage/save_load.i
+++ b/src/plugins/wp/tests/wp_usage/save_load.i
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -no-autoload-plugins -load-module wp -wp-share ./share -wp -wp-print -wp-prover none @PTEST_FILE@ -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@.sav.err
-   CMD: @frama-c@ -no-autoload-plugins -load-module wp -load @PTEST_DIR@/@PTEST_NAME@.sav
+   EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -no-autoload-plugins -load-module wp -wp-warn-key pedantic-assigns=inactive -wp-share ./share -wp -wp-print -wp-prover none @PTEST_FILE@ -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@.sav.err
+   CMD: @frama-c@ -no-autoload-plugins -load-module wp -load @PTEST_DIR@/@PTEST_NAME@.sav -wp-warn-key pedantic-assigns=inactive
    OPT: -print
    OPT: -wp -wp-prover none -wp-print
 */
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 441d8cbfb9a77ad409cac7eaec0ee71afb1318db..e794026a1b9b924327314e1634c0567b4fecd6ba 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -521,6 +521,22 @@ let user_prop_names p =
   | IPGlobalInvariant _
   | IPOther _ -> []
 
+let user_bhv_names p =
+  let open Property in
+  let fors = match p with
+    | Property.IPCodeAnnot { ica_ca } ->
+        let fors = match ica_ca.annot_content with
+          | Cil_types.AAssert (fors, _)
+          | Cil_types.AStmtSpec (fors, _)
+          | Cil_types.AInvariant (fors, _, _)
+          | Cil_types.AAssigns (fors, _)
+          | Cil_types.AAllocation (fors, _)
+          | Cil_types.AExtended (fors, _, _) -> fors
+          | _ -> []
+        in fors
+    | _ -> []
+  in Extlib.may_map ~dft:fors (fun b -> b.b_name :: fors) (get_behavior p)
+
 let string_of_termination_kind = function
     Normal -> "post"
   | Exits -> "exits"
@@ -772,8 +788,7 @@ let select_default pid =
   let names = user_prop_pid pid in
   not (List.mem "no_wp" names)
 
-let select_by_name asked_names pid =
-  let names = user_prop_pid pid in
+let are_selected_names asked names =
   if List.mem "no_wp" names then false
   else
     let is_minus s = try s.[0] = '-' with _ -> false in
@@ -791,10 +806,16 @@ let select_by_name asked_names pid =
                then a && (not (eval ()))
                else a || (eval ()))
     in
-    match List.fold_left eval None asked_names with
+    match List.fold_left eval None asked with
     | Some false -> false
     | _ -> true
 
+
+let select_by_name asked_names pid =
+  let names = user_prop_pid pid in
+  are_selected_names asked_names names
+
+
 let select_call_pre s_call asked_pre pid =
   match pid.p_kind with
   | PKPre (_, p_stmt, p_prop) ->
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index c0020de8a10f437c2e9dabf26dd57814e7e60cfc..29098180bbefd8e1aff6209038722fc25eb84660 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -80,6 +80,12 @@ val get_propid : prop_id -> string (** Unique identifier of [prop_id] *)
 val get_legacy : prop_id -> string (** Unique legacy identifier of [prop_id] *)
 val pp_propid : Format.formatter -> prop_id -> unit (** Print unique id of [prop_id] *)
 
+val user_bhv_names: Property.identified_property -> string list
+val user_prop_names: Property.identified_property -> string list
+val are_selected_names: string list -> string list -> bool
+(** [are_selected_names asked names] checks if [names] of a property are
+    selected according to [asked] names. *)
+
 type prop_kind =
   | PKTactic      (** tactical sub-goal *)
   | PKCheck       (** internal check *)
diff --git a/src/plugins/wp/wpRTE.ml b/src/plugins/wp/wpRTE.ml
index 74e6fdd198f0571fc00914d254d51eacbe7e330e..a6bc0690c67b02c398b4a689d52472dda12c11fb 100644
--- a/src/plugins/wp/wpRTE.ml
+++ b/src/plugins/wp/wpRTE.ml
@@ -102,6 +102,9 @@ let generate model kf =
   List.iter (configure ~update ~generate:true kf cint) generator ;
   if !update then !Db.RteGen.annotate_kf kf
 
+let generate_all model =
+  Wp_parameters.iter_kf (generate model)
+
 let missing_guards model kf =
   let update = ref false in
   let cint = WpContext.on_context (model,WpContext.Kf kf) Cint.current () in
diff --git a/src/plugins/wp/wpRTE.mli b/src/plugins/wp/wpRTE.mli
index 53b0fc8eb4bedfaa029cf571b2a7bb01f75ea752..86ce77c668afd0e0d5c608baa35653d5e0b6c809 100644
--- a/src/plugins/wp/wpRTE.mli
+++ b/src/plugins/wp/wpRTE.mli
@@ -24,6 +24,9 @@
     for the given function and model. *)
 val generate : WpContext.model -> Kernel_function.t -> unit
 
+(** Invoke RTE on all selected functions *)
+val generate_all : WpContext.model -> unit
+
 (** Returns [true] if RTE annotations should be generated for
     the given function and model (and are not generated yet). *)
 val missing_guards : WpContext.model -> Kernel_function.t -> bool
diff --git a/src/plugins/wp/wpTarget.ml b/src/plugins/wp/wpTarget.ml
new file mode 100644
index 0000000000000000000000000000000000000000..1f3ad92c7afdc70c729c73edec3a98e559e29ffb
--- /dev/null
+++ b/src/plugins/wp/wpTarget.ml
@@ -0,0 +1,169 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+module Fct = Cil_datatype.Kf.Set
+
+module TargetKfs =
+  State_builder.Set_ref
+    (Fct)
+    (struct
+      let dependencies = [ Ast.self ]
+      let name = "WpTarget.TargetKfs"
+    end)
+
+let get_called_stmt stmt =
+  match stmt.skind with
+  | Instr (Call(_, fct, _, _)) ->
+      begin match Kernel_function.get_called fct with
+        | Some kf -> [kf]
+        | None -> Extlib.(opt_conv [] (opt_map snd (Dyncall.get stmt)))
+      end
+  | Instr (Local_init (_,ConsInit(vi,_,_),_)) -> [ Globals.Functions.get vi ]
+  | _ -> []
+
+module Callees =
+  State_builder.Hashtbl
+    (Cil_datatype.Kf.Hashtbl)
+    (Fct)
+    (struct
+      let dependencies = [Ast.self]
+      let name = "WpTarget.Callees"
+      let size = 17
+    end)
+
+(** Note: we add the kf received in parameter in the set only if it has a
+    definition (and thus if it does not have one, we add nothing as it has
+    no visible callee).
+
+    This prevent to warn on prototypes that have a contract but are unused. If
+    the function is used, it will be added to the set via its caller(s) if they
+    are under verification.
+*)
+let with_callees kf =
+  try
+    let stmts = (Kernel_function.get_definition kf).sallstmts in
+    let fold s stmt =
+      List.fold_left (fun s kf -> Fct.add kf s) s (get_called_stmt stmt)
+    in
+    List.fold_left fold (Fct.singleton kf) stmts
+  with Kernel_function.No_Definition -> Fct.empty
+
+let with_callees = Callees.memo with_callees
+
+let add_with_callees kf =
+  Fct.iter TargetKfs.add (with_callees kf)
+
+exception Found
+
+let check_properties behaviors props kf =
+  let open Property in
+  let exists_selected_behavior l =
+    behaviors = [] || List.exists (fun b -> List.mem b behaviors) l
+  in
+  let check_ip ip =
+    if exists_selected_behavior (WpPropId.user_bhv_names ip) then
+      let names = WpPropId.user_prop_names ip in
+      if props = [] || WpPropId.are_selected_names props names then raise Found
+  in
+  let check_bhv_requires kf kinstr bv =
+    List.iter (fun p -> check_ip (ip_of_requires kf kinstr bv p)) bv.b_requires
+  in
+  let check_bhv_ensures kf kinstr bv =
+    List.iter (fun p -> check_ip (ip_of_ensures kf kinstr bv p)) bv.b_post_cond
+  in
+  let opt_check = function None -> () | Some p -> check_ip p in
+  let check_bhv_assigns kf kinstr bv =
+    opt_check (ip_assigns_of_behavior kf kinstr ~active:[] bv)
+  in
+  let check_bhv_allocation kf kinstr bv =
+    opt_check (ip_allocation_of_behavior kf kinstr ~active:[] bv)
+  in
+  let check_complete_disjoint kf kinstr =
+    try
+      let spec = Annotations.funspec kf in
+      let comp = ip_complete_of_spec kf kinstr ~active:[] spec in
+      let disj = ip_disjoint_of_spec kf kinstr ~active:[] spec in
+      List.iter check_ip comp ;
+      List.iter check_ip disj ;
+    with Annotations.No_funspec _ -> ()
+  in
+  let check_bhv kf kinstr bv =
+    check_bhv_assigns kf kinstr bv ;
+    check_bhv_allocation kf kinstr bv ;
+    check_bhv_ensures kf kinstr bv ;
+    check_complete_disjoint kf kinstr
+  in
+  let check_code () =
+    let stmts =
+      try (Kernel_function.get_definition kf).sallstmts
+      with Kernel_function.No_Definition -> []
+    in
+    let check stmt _ ca =
+      List.iter check_ip (ip_of_code_annot kf stmt ca)
+    in
+    let check_call stmt =
+      let check_callee kf =
+        let kf_behaviors = Annotations.behaviors kf in
+        List.iter (check_bhv_requires kf Kglobal) kf_behaviors
+      in
+      List.iter check_callee (get_called_stmt stmt)
+    in
+    let check_stmt stmt =
+      check_call stmt ;
+      Annotations.iter_code_annot (check stmt) stmt
+    in
+    List.iter check_stmt stmts
+  in
+  let check_funbhv _ bv = check_bhv kf Kglobal bv in
+  Annotations.iter_behaviors check_funbhv kf ;
+  check_code ()
+
+let add_with_behaviors behaviors props kf =
+  if behaviors = [] && props = [] then
+    add_with_callees kf
+  else begin
+    try check_properties behaviors props kf
+    with Found -> add_with_callees kf
+  end
+
+let compute model =
+  let insert_rte kf =
+    if Wp_parameters.RTE.get () then
+      WpRTE.generate model kf
+  in
+  let behaviors = Wp_parameters.Behaviors.get() in
+  let props = Wp_parameters.Properties.get () in
+  let add_kf kf =
+    insert_rte kf ;
+    add_with_behaviors behaviors props kf
+  in
+  Wp_parameters.iter_kf add_kf
+
+let compute model =
+  if not (TargetKfs.is_computed ()) then begin
+    compute model ;
+    TargetKfs.mark_as_computed ()
+  end
+
+let iter = TargetKfs.iter
diff --git a/src/plugins/wp/wpTarget.mli b/src/plugins/wp/wpTarget.mli
new file mode 100644
index 0000000000000000000000000000000000000000..22cc8ce147b8d85376c77e84a550fc1c1af629fa
--- /dev/null
+++ b/src/plugins/wp/wpTarget.mli
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** This module computes the set of kernel functions that are considered by
+    the command line options transmitted to WP. That is:
+
+    - all functions on which a verification must be tried,
+    - all functions that are called by the previous ones,
+    - including those parameterized via the 'calls' clause.
+
+    It takes in account the options -wp-bhv and -wp-props so that if all
+    functions are initially selected but in fact some of them are filtered out
+    by these options, they are not considered.
+*)
+
+val compute: WpContext.model -> unit
+val iter: (Kernel_function.t -> unit) -> unit
+
+
+val with_callees: Kernel_function.t -> Kernel_function.Set.t
+(** @returns the set composed of the given kernel_function together with its
+    callees. If this function does not have a definition, the empty set is
+    returned.
+*)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 9335161d010553d664de54516270ead945483112..661340a06cac4a55f71232edca60236a7e379eaf 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1065,25 +1065,17 @@ module MemoryContext =
       let help = "Warn Against Memory Model Hypotheses"
     end)
 
-let wkey_imprecise_hypotheses_assigns =
-  register_warn_category "hypotheses:assigns"
-let () = set_warn_status wkey_imprecise_hypotheses_assigns Log.Winactive
-
 let () = Parameter_customize.set_group wp_po
 let () = Parameter_customize.do_not_save ()
 
-module CheckModelHypotheses =
+module CheckMemoryContext =
   False
     (struct
-      let option_name = "-wp-check-model-hypotheses"
+      let option_name = "-wp-check-memory-model"
       let help = "Insert memory model hypotheses in function contracts and \
                   check them on call. (experimental)"
     end)
 
-let wkey_imprecise_hypotheses_assigns =
-  register_warn_category "hypotheses:assigns"
-let () = set_warn_status wkey_imprecise_hypotheses_assigns Log.Winactive
-
 let () = Parameter_customize.set_group wp_po
 module OutputDir =
   String(struct
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 97392faa580e3f4b36d686429ba3eb7b53c90c1d..ab805c2b51ff00e88db86e089f7729756a71ca73 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -150,14 +150,12 @@ module Report: Parameter_sig.String_list
 module ReportJson: Parameter_sig.String
 module ReportName: Parameter_sig.String
 module MemoryContext: Parameter_sig.Bool
-module CheckModelHypotheses: Parameter_sig.Bool
+module CheckMemoryContext: Parameter_sig.Bool
 module SmokeTests: Parameter_sig.Bool
 module SmokeDeadloop: Parameter_sig.Bool
 module SmokeDeadcode: Parameter_sig.Bool
 module SmokeDeadcall: Parameter_sig.Bool
 
-val wkey_imprecise_hypotheses_assigns: warn_category
-
 (** {2 Getters} *)
 
 val has_out : unit -> bool
diff --git a/tests/spec/assignable_location.i b/tests/spec/assignable_location.i
index f7165642c352a6b605e3a3bc682e338dad40c2a0..70968c3735ad313c5896d7125e9f350e4c4a509d 100644
--- a/tests/spec/assignable_location.i
+++ b/tests/spec/assignable_location.i
@@ -1,4 +1,4 @@
-/* run.config 
+/* run.config
 OPT: -kernel-warn-key=annot-error=active
 */
 
@@ -18,6 +18,13 @@ double annotations_to_accept(typetab *t) {
   return f(t);
 }
 
+/*@ behavior acc_0: assigns \result \from &x ;
+    behavior acc_1: assigns \result \from &f ;
+*/
+int * from_address_to_accept(int f){
+  return (void*)0 ;
+}
+
 
 int g(void);
 
@@ -39,3 +46,10 @@ int annotations_to_reject(void) {
   //@ behavior to_reject_6: assigns x \from lx;
   return g();
 }
+
+/*@ behavior rej_0: assigns \result \from &l ; */
+int * from_address_to_reject(int f){
+  int l ;
+  //@ behavior rej_1: assigns l \from &lx ;
+  return (void*)0 ;
+}
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 66c93e7d3a8fb3ec726efdd2efa913a36d46b1ba..baf66eaa6b7c65976cc5218477b20cb503d4d012 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,5 +1,5 @@
 /* run.config
-OPT: -wp -wp-prover qed -wp-msg-key shell
+OPT: -wp -wp-prover qed -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive
 OPT: -eva -eva-use-spec f
 OPT: -print
 */
diff --git a/tests/spec/oracle/assignable_location.res.oracle b/tests/spec/oracle/assignable_location.res.oracle
index 161492d3b4694091d6717a36526e2768606e9378..775b7573457de6e89e8f89b34a7728b717a216c2 100644
--- a/tests/spec/oracle/assignable_location.res.oracle
+++ b/tests/spec/oracle/assignable_location.res.oracle
@@ -1,23 +1,27 @@
 [kernel] Parsing tests/spec/assignable_location.i (no preprocessing)
-[kernel:annot-error] tests/spec/assignable_location.i:36: Warning: 
+[kernel:annot-error] tests/spec/assignable_location.i:43: Warning: 
   unexpected token ';'
-[kernel:annot-error] tests/spec/assignable_location.i:28: Warning: 
+[kernel:annot-error] tests/spec/assignable_location.i:35: Warning: 
   not an addressable left value: \result. Ignoring logic specification of function annotations_to_reject
-[kernel:annot-error] tests/spec/assignable_location.i:30: Warning: 
+[kernel:annot-error] tests/spec/assignable_location.i:37: Warning: 
   not an assignable left value: *t. Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:31: Warning: 
+[kernel:annot-error] tests/spec/assignable_location.i:38: Warning: 
   not an assignable left value: *(t + 0). Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:32: Warning: 
+[kernel:annot-error] tests/spec/assignable_location.i:39: Warning: 
   not an assignable left value: *(t + (0 .. 0)). Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:33: Warning: 
+[kernel:annot-error] tests/spec/assignable_location.i:40: Warning: 
   not an assignable left value: (int)x. Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:34: Warning: 
+[kernel:annot-error] tests/spec/assignable_location.i:41: Warning: 
   not an assignable left value: (char)x. Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:35: Warning: 
+[kernel:annot-error] tests/spec/assignable_location.i:42: Warning: 
   not an addressable left value: (char)x. Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:37: Warning: 
+[kernel:annot-error] tests/spec/assignable_location.i:44: Warning: 
   not an addressable left value: \empty. Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:38: Warning: 
-  not an assignable left value: lx. Ignoring code annotation
-[kernel:annot-error] tests/spec/assignable_location.i:39: Warning: 
+[kernel:annot-error] tests/spec/assignable_location.i:45: Warning: 
   not an assignable left value: lx. Ignoring code annotation
+[kernel:annot-error] tests/spec/assignable_location.i:46: Warning: 
+  not a valid dependency: lx. Ignoring code annotation
+[kernel:annot-error] tests/spec/assignable_location.i:50: Warning: 
+  unbound logic variable l. Ignoring logic specification of function from_address_to_reject
+[kernel:annot-error] tests/spec/assignable_location.i:53: Warning: 
+  not an addressable left value: lx. Ignoring code annotation