diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index 2904da424d07f67ad359bbdc42ec4b329f6b9696..b3012f74718fa77cdc0ff4d8e6c73e9ec2b5f40e 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -279,10 +279,18 @@ let clauses_of_partition kf loc p =
   let reqs = List.sort_uniq Logic_utils.compare_predicate reqs in
   reqs
 
-let emitter =
-  Emitter.(create "Wp.Hypotheses" [Funspec] ~correctness:[] ~tuning:[])
-
-let get_behavior kf name partition =
+module Table =
+  State_builder.Hashtbl
+    (Cil_datatype.Kf.Hashtbl)
+    (Datatype.Option(Cil_datatype.Funbehavior))
+    (struct
+      let name = "MemoryContext.Table"
+      let size = 17
+      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
@@ -299,7 +307,17 @@ let get_behavior kf name partition =
         b_extended = []
       }
 
-let add_behavior kf name partition =
-  match get_behavior kf name partition with
+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
+
+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]
diff --git a/src/plugins/wp/MemoryContext.mli b/src/plugins/wp/MemoryContext.mli
index 6c406b1aab8091d7474ac3fdf9c920de5ad506c3..736617995ed81cf7f7ad010849e1349f9c689712 100644
--- a/src/plugins/wp/MemoryContext.mli
+++ b/src/plugins/wp/MemoryContext.mli
@@ -24,12 +24,16 @@ open Cil_types
 
 type param = NotUsed | ByAddr | ByValue | ByShift | ByRef | InContext | InArray
 
-val pp_param : Format.formatter -> param -> unit
+val pp_param: Format.formatter -> param -> unit
 
 type partition
 
-val empty : partition
-val set : varinfo -> param -> partition -> partition
+val empty: partition
+val set: varinfo -> param -> partition -> partition
 
-val add_behavior : kernel_function -> string -> partition -> unit
-val get_behavior : kernel_function -> string -> partition -> behavior option
+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
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 580ac96104604bad0b3dd26b964aebd431b40460..78dc895d0133414e056986586b4deeb45b8a24c7 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -99,13 +99,18 @@ let wp_print_memory_context kf bhv fmt =
       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 () =
   begin
     wp_iter_model
       begin fun kf m ->
-        let partition = WpContext.compute_hypotheses m kf in
+        let hypotheses_computer = WpContext.compute_hypotheses m in
         let model = WpContext.MODEL.id m in
-        let hyp = MemoryContext.get_behavior kf model partition in
+        let hyp = MemoryContext.get_behavior kf model hypotheses_computer in
         match hyp with
         | None -> ()
         | Some bhv ->
@@ -121,9 +126,9 @@ let wp_insert_memory_context model =
   begin
     Wp_parameters.iter_fct
       begin fun kf ->
-        let hyp = WpContext.compute_hypotheses model kf in
+        let hyp_computer = WpContext.compute_hypotheses model in
         let model_id = WpContext.MODEL.id model in
-        MemoryContext.add_behavior kf model_id hyp
+        MemoryContext.add_behavior kf model_id hyp_computer
       end
   end
 
@@ -171,9 +176,9 @@ let do_wp_report () =
         end ;
         List.iter (WpReport.export stats) reports ;
       end ;
-    if Wp_parameters.MemoryContext.get () then
-      wp_warn_memory_context ()
-  end
+      if Wp_parameters.MemoryContext.get () then
+        wp_warn_memory_context ()
+    end
 
 (* ------------------------------------------------------------------------ *)
 (* ---  Wp Results                                                      --- *)
@@ -812,6 +817,7 @@ let cmdline_run () =
         WpContext.on_context (computer#model,WpContext.Global)
           LogicBuiltins.dump ();
       end ;
+    wp_compute_memory_context computer#model ;
     if Wp_parameters.CheckModelHypotheses.get () then
       wp_insert_memory_context computer#model fct ;
     Generator.compute_selection computer ~fct ~bhv ~prop ()
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
index 824ee1a6e3133d0e01ae5f4aeceac1314c20cbab..f27ec49d1b76b21fa56b659de40a911b560d62f2 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
@@ -2,10 +2,10 @@
 [kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
-[kernel] tests/wp/wp_call_pre.c:53: Warning: 
-  No code nor implicit assigns clause for function g, generating default assigns from the prototype
 [kernel] tests/wp/wp_call_pre.c:53: Warning: 
   No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel] tests/wp/wp_call_pre.c:53: Warning: 
+  No code nor implicit assigns clause for function g, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
 [wp] 10 goals scheduled
 [wp] [Qed] Goal typed_call_g_call_g_requires_qed_ok_Rga : Valid