diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index b24a0ca165b0113a6afb5761142d6c86f4eb22f2..d95fde6f349c1a07b9b94820fe7e953ba95a8878 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/src/plugins/wp/GuiPanel.ml
@@ -63,9 +63,30 @@ let wp_rte_generated s =
         not mem
       else false
 
+let merge_scopes vcs =
+  Bag.fold_left
+    begin fun s vc ->
+       match VC.get_scope vc with
+       | WpContext.Global -> s
+       | WpContext.Kf kf ->
+          Kernel_function.Set.union (WpTarget.with_callees kf) s
+    end
+    Kernel_function.Set.empty vcs
+
+let warn_memory_context vcs =
+  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
+  Kernel_function.Set.iter
+    (fun kf -> MemoryContext.warn kf name hypotheses_computer)
+    (merge_scopes vcs)
+
 let spawn provers vcs =
   if not (Bag.is_empty vcs) then
     let provers = Why3.Whyconf.Sprover.elements provers#get in
+    warn_memory_context vcs ;
     VC.command ~provers ~tip:true vcs
 
 let run_and_prove
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index 760468e073e6343db3d37289c2536db06b91bc6d..7a295a841fb35888c817f9dcf5d29ca3a50d0d8a 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -382,7 +382,7 @@ let warn kf name hyp_computer =
   | None -> ()
   | Some bhv ->
       Wp_parameters.warning
-        ~current:false ~once:true
+        ~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)
diff --git a/src/plugins/wp/WpTarget.ml b/src/plugins/wp/WpTarget.ml
index 10d122bee5a79927ac7c2e3d9bb71dfb0880e672..b83ced128099629fbcf48620e817e1389f8a8d03 100644
--- a/src/plugins/wp/WpTarget.ml
+++ b/src/plugins/wp/WpTarget.ml
@@ -52,6 +52,16 @@ let calls_visitor callees = object(self)
     | _ -> Cil.SkipChildren
 end
 
+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).
@@ -60,16 +70,18 @@ end
     the function is used, it will be added to the set via its caller(s) if they
     are under verification.
 *)
+let with_callees kf =
+  if Kernel_function.has_definition kf then begin
+    let set = ref (Fct.singleton kf) in
+    ignore (Visitor.visitFramacKf (calls_visitor set) kf) ;
+    !set
+  end else
+    Fct.empty
+
+let with_callees = Callees.memo with_callees
+
 let add_with_callees kf =
-  let component kf =
-    if Kernel_function.has_definition kf then begin
-      let set = ref (Fct.singleton kf) in
-      ignore (Visitor.visitFramacKf (calls_visitor set) kf) ;
-      !set
-    end else
-      Fct.empty
-  in
-  Fct.iter TargetKfs.add (component kf)
+  Fct.iter TargetKfs.add (with_callees kf)
 
 exception Found
 
diff --git a/src/plugins/wp/WpTarget.mli b/src/plugins/wp/WpTarget.mli
index c5af30b5a9cd742cd4957fc4c3524c40c5462309..22cc8ce147b8d85376c77e84a550fc1c1af629fa 100644
--- a/src/plugins/wp/WpTarget.mli
+++ b/src/plugins/wp/WpTarget.mli
@@ -20,5 +20,24 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** 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.
+*)