[wp] add spec populate for API calls

src/plugins/wp/cfgGenerator.ml

@@ -54,6 +54,16 @@ let get_kf_infos model kf ?bhv ?prop () =
     Wp_parameters.warning ~current:false ~once:true "Missing RTE guards" ;
   infos
 
+(* -------------------------------------------------------------------------- *)
+(* --- Target preparation                                                 --- *)
+(* -------------------------------------------------------------------------- *)
+
+let prepare_ip model ip =
+  Option.iter (WpTarget.compute_kf model) @@ Property.get_kf ip
+
+let prepare_main model ?fct ?bhv ?prop () =
+  WpTarget.compute model ?fct ?bhv ?prop ()
+
 (* -------------------------------------------------------------------------- *)
 (* --- Behavior Selection                                                 --- *)
 (* -------------------------------------------------------------------------- *)
@@ -265,6 +275,7 @@ struct
     end
 
   let compute_ip model ip =
+    prepare_ip model ip ;
     let pool = empty () in
     strategy_ip model pool ip ;
     compute model pool
@@ -275,6 +286,7 @@ struct
     Bag.empty
 
   let compute_main model ?fct ?bhv ?prop () =
+    prepare_main model ?fct ?bhv ?prop () ;
     let pool = empty () in
     strategy_main model pool ?fct ?bhv ?prop () ;
     compute model pool
@@ -334,11 +346,13 @@ let dumper setup driver =
     object
       method model = model
       method compute_ip ip =
+        prepare_ip model ip ;
         let pool = empty () in
         strategy_ip model pool ip ;
         dump pool ; Bag.empty
       method compute_call _ = Bag.empty
       method compute_main ?fct ?bhv ?prop () =
+        prepare_main model ?fct ?bhv ?prop () ;
         let pool = empty () in
         strategy_main model pool ?fct ?bhv ?prop () ;
         dump pool ; Bag.empty

src/plugins/wp/gui/GuiPanel.ml

@@ -37,32 +37,6 @@ let reload_callback = ref (fun () -> ())
 let on_reload f = reload_callback := f
 let reload () = !reload_callback ()
 
-module Wp_rte_generated =
-  Kernel_function.Make_Table
-    (Datatype.Unit)
-    (struct
-      let name = "GuiSource.Rte_generated"
-      let size = 8
-      let dependencies = [ Ast.self ]
-    end)
-
-let kf_of_selection = function
-  | S_none -> None
-  | S_fun kf -> Some kf
-  | S_prop ip -> Property.get_kf ip
-  | S_call s -> Some s.s_caller
-
-let wp_rte_generated s =
-  match kf_of_selection s with
-  | None -> false
-  | Some kf ->
-    if Wp_parameters.RTE.get () then
-      let mem = Wp_rte_generated.mem kf in
-      if not mem then
-        Wp_rte_generated.add kf () ;
-      not mem
-    else false
-
 let with_model action kf =
   let setup = Factory.parse (Wp_parameters.Model.get ()) in
   let driver = Driver.load_driver () in
@@ -117,10 +91,7 @@ let run_and_prove
         | S_prop ip -> spawn provers (VC.generate_ip ip)
         | S_call s -> spawn provers (VC.generate_call s.s_stmt)
       end ;
-      if wp_rte_generated selection then
-        main#redisplay ()
-      else
-        reload ()
+      main#redisplay ()
     with Stop -> ()
   end
 

src/plugins/wp/register.ml

@@ -816,7 +816,7 @@ let cmdline_run () =
             WpContext.on_context (model,WpContext.Global)
               LogicBuiltins.dump ();
           end ;
-        WpTarget.compute model ;
+        WpTarget.compute model ~fct ~bhv ~prop () ;
         wp_compute_memory_context model ;
         if Wp_parameters.CheckMemoryContext.get () then
           wp_insert_memory_context model ;

src/plugins/wp/wpTarget.ml

@@ -71,7 +71,7 @@ let with_callees kf =
 
 let with_callees = Callees.memo with_callees
 
-let add_with_callees ~populate_spec kf =
+let add_with_callees kf =
   let add kf =
     let insert_spec kf =
       let specs =
@@ -81,7 +81,7 @@ let add_with_callees ~populate_spec kf =
       in
       Populate_spec.populate_funspec ~do_body:true kf specs
     in
-    if populate_spec then insert_spec kf ;
+    insert_spec kf ;
     TargetKfs.add kf
   in
   Fct.iter add (with_callees kf)
@@ -155,29 +155,25 @@ let check_properties behaviors props kf =
 
 let add_with_behaviors behaviors props kf =
   if behaviors = [] && props = [] then
-    add_with_callees ~populate_spec:true kf
+    add_with_callees kf
   else begin
     try check_properties behaviors props kf
-    with Found -> add_with_callees ~populate_spec:true 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_kf model bhv prop kf =
+  let rtes = Wp_parameters.RTE.get () in
+  if rtes then WpRTE.generate model kf ;
+  add_with_behaviors bhv prop kf
 
-let compute model =
-  if not (TargetKfs.is_computed ()) then begin
-    compute model ;
-    TargetKfs.mark_as_computed ()
-  end
+let compute model
+  ?(fct=Wp_parameters.get_fct())
+  ?(bhv=Wp_parameters.Behaviors.get())
+  ?(prop=Wp_parameters.Properties.get ()) ()
+  =
+  Wp_parameters.iter_fct (compute_kf model bhv prop) fct
+
+let compute_kf model kf =
+  compute_kf model [] [] kf
 
 let iter = TargetKfs.iter

src/plugins/wp/wpTarget.mli

@@ -32,7 +32,26 @@
     by these options, they are not considered.
 *)
 
-val compute: WpContext.model -> unit
+val compute: WpContext.model ->
+  ?fct:Wp_parameters.functions ->
+  ?bhv:string list ->
+  ?prop:string list ->
+  unit ->
+  unit
+(** Compute the entire set, populating specification related to:
+    - exits
+    - terminates
+    - assigns (for functions without body)
+*)
+
+val compute_kf: WpContext.model -> Kernel_function.t -> unit
+(** Compute the target properties associated to the given kernel function. It
+    also populates exits, terminates and assigns for the function and its
+    callees, as well as RTE assertions if they are asked on command  line.
+
+    @since Frama-C+dev
+*)
+
 val iter: (Kernel_function.t -> unit) -> unit