[wp] compute static calls

src/plugins/wp/cfgCalculus.ml

@@ -262,7 +262,32 @@ struct
           Varinfo.pretty x ; p
     | Asm _ ->
         M.use_assigns env.we None (WpPropId.mk_asm_assigns_desc s) p
-    | Call _ -> assert false
+    | Call(r,fct,es,_) ->
+        begin
+          match Kernel_function.get_called fct with
+          | Some kf -> call env s r kf es (WpAnnot.get_call_contract kf) p
+          | None ->
+              (*TODO: dynamic call *)
+              assert false
+        end
+
+  and call env s r kf es (c : WpAnnot.call_contract) wr : M.t_prop =
+    let filter ps = List.filter (is_selected env ~goal:false) ps in
+    let w_call = M.call env.we s r kf es
+      ~pre:(filter c.call_pre)
+      ~post:(filter c.call_post)
+      ~pexit:(filter c.call_exit)
+      ~assigns:c.call_assigns
+      ~p_post:wr ~p_exit:env.wk in
+    if is_default_bhv env.mode then
+      let pre =
+        List.filter_map (fun p ->
+            if is_selected env ~goal:true p then
+              Some (WpAnnot.get_precond_at kf s p)
+            else None
+          ) c.call_pre
+      in M.call_goal_precond env.we s kf es ~pre w_call
+    else w_call
 
   let body env ~ensures ~exits w =
     let rw = List.fold_right (prove_property env) ensures w in

src/plugins/wp/wpAnnot.ml

@@ -236,6 +236,22 @@ let get_behavior kf ki ~active bhv =
 (* --- Called Contract                                                    --- *)
 (* -------------------------------------------------------------------------- *)
 
+(*TODO: put it in Status_by_call ? *)
+module AllPrecondStatus =
+  State_builder.Hashtbl(Kernel_function.Hashtbl)(Datatype.Unit)
+    (struct
+      let name = "Call Preconditions Proxy Generated"
+      let dependencies = [Ast.self]
+      let size = 32
+    end)
+
+let setup_preconditions kf =
+  if not (AllPrecondStatus.mem kf) then
+    begin
+      AllPrecondStatus.add kf () ;
+      Statuses_by_call.setup_all_preconditions_proxies kf ;
+    end
+
 type call_contract = {
   call_pre : WpPropId.pred_info list ;
   call_post : WpPropId.pred_info list ;
@@ -243,12 +259,19 @@ type call_contract = {
   call_assigns : Cil_types.assigns ;
 }
 
+let get_precond_at kf stmt (id,p) =
+  let pi = WpPropId.property_of_id id in
+  let pi_at = Statuses_by_call.precondition_at_call kf pi stmt in
+  let id_at = WpPropId.mk_call_pre_id kf stmt pi pi_at in
+  id_at , p
+
 let get_call_contract kf =
   let cpre : WpPropId.pred_info list ref = ref [] in
   let cpost : WpPropId.pred_info list ref = ref [] in
   let cexit : WpPropId.pred_info list ref = ref [] in
   let cwrites = ref [] in
   let add c f x = c := (f x) :: !c in
+  setup_preconditions kf ;
   List.iter
     begin fun bhv ->
       let assumes =

src/plugins/wp/wpAnnot.mli

@@ -104,12 +104,13 @@ val get_loop_contract : kernel_function -> stmt -> loop_contract
 (* -------------------------------------------------------------------------- *)
 
 type call_contract = {
-  call_pre : WpPropId.pred_info list ;
-  call_post : WpPropId.pred_info list ;
-  call_exit : WpPropId.pred_info list ;
-  call_assigns : Cil_types.assigns ;
+  call_pre : pred_info list ;
+  call_post : pred_info list ;
+  call_exit : pred_info list ;
+  call_assigns : assigns ;
 }
 
+val get_precond_at : kernel_function -> stmt -> pred_info -> pred_info
 val get_call_contract : kernel_function -> call_contract
 
 (* -------------------------------------------------------------------------- *)