[wp] FIxes hypotheses computation for GUI

src/plugins/wp/GuiPanel.ml

@@ -63,32 +63,45 @@ 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 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
-  Kernel_function.Set.iter
-    (fun kf -> MemoryContext.warn kf name hypotheses_computer)
-    (merge_scopes vcs)
+  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.CheckModelHypotheses.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
-    warn_memory_context vcs ;
     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)
@@ -97,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)

src/plugins/wp/MemoryContext.ml

@@ -390,7 +390,20 @@ let warn kf name hyp_computer =
 let emitter =
   Emitter.(create "Wp.Hypotheses" [Funspec] ~correctness:[] ~tuning:[])
 
+module RegisteredHypotheses =
+  State_builder.Set_ref
+    (Cil_datatype.Kf.Set)
+    (struct
+      let name = "Wp.MemoryContext.RegisteredHypotheses"
+      let dependencies = [Ast.self]
+    end)
+
 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