[wp] refactor contract to prepare stmt

src/plugins/wp/cfgAnnot.ml

@@ -180,7 +180,37 @@ let get_disjoint_behaviors kf =
     ) spec.spec_disjoint_behaviors
 
 (* -------------------------------------------------------------------------- *)
-(* --- Called Contract                                                    --- *)
+(* --- Contracts                                                          --- *)
+(* -------------------------------------------------------------------------- *)
+
+type contract = {
+  contract_pre : WpPropId.pred_info list ;
+  contract_post : WpPropId.pred_info list ;
+  contract_exit : WpPropId.pred_info list ;
+  contract_smoke : WpPropId.pred_info list ;
+  contract_assigns : Cil_types.assigns ;
+}
+
+let assigns_upper_bound behaviors =
+  let collect_assigns (def, assigns) bhv =
+    (* Default behavior prevails *)
+    if Cil.is_default_behavior bhv then Some bhv.b_assigns, None
+    else if Option.is_some def then def, None
+    else begin
+      (* Note that here, def is None *)
+      match assigns, bhv.b_assigns with
+      | None, a -> None, Some a
+      | Some WritesAny, _ | Some _, WritesAny -> None, Some WritesAny
+      | Some (Writes a), Writes b -> None, Some (Writes (a @ b))
+    end
+  in
+  match List.fold_left collect_assigns (None, None) behaviors with
+  | Some a, _ -> a (* default behavior first *)
+  | _, Some a -> a (* else combined behaviors *)
+  | _ -> WritesAny
+
+(* -------------------------------------------------------------------------- *)
+(* --- Call Contracts                                                     --- *)
 (* -------------------------------------------------------------------------- *)
 
 (*TODO: put it in Status_by_call ? *)
@@ -199,42 +229,16 @@ let setup_preconditions 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 ;
-  call_exit : WpPropId.pred_info list ;
-  call_smoke : WpPropId.pred_info list ;
-  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 assigns_upper_bound behaviors =
-  let collect_assigns (def, assigns) bhv =
-    (* Default behavior prevails *)
-    if Cil.is_default_behavior bhv then Some bhv.b_assigns, None
-    else if Option.is_some def then def, None
-    else begin
-      (* Note that here, def is None *)
-      match assigns, bhv.b_assigns with
-      | None, a -> None, Some a
-      | Some WritesAny, _ | Some _, WritesAny -> None, Some WritesAny
-      | Some (Writes a), Writes b -> None, Some (Writes (a @ b))
-    end
-  in
-  match List.fold_left collect_assigns (None, None) behaviors with
-  | Some a, _ -> a (* default behavior first *)
-  | _, Some a -> a (* else combined behaviors *)
-  | _ -> WritesAny
-
 module CallContract = WpContext.StaticGenerator(Kernel_function)
     (struct
       type key = kernel_function
-      type data = call_contract
+      type data = contract
       let name = "Wp.CfgAnnot.CallContract"
       let compile kf =
         let cpre : WpPropId.pred_info list ref = ref [] in
@@ -255,11 +259,11 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
               ) bhv.b_post_cond ;
           end behaviors ;
         {
-          call_pre = List.rev !cpre ;
-          call_post = List.rev !cpost ;
-          call_exit = List.rev !cexit ;
-          call_smoke = [] ;
-          call_assigns = assigns_upper_bound behaviors
+          contract_pre = List.rev !cpre ;
+          contract_post = List.rev !cpost ;
+          contract_exit = List.rev !cexit ;
+          contract_smoke = [] ;
+          contract_assigns = assigns_upper_bound behaviors
         }
     end)
 
@@ -269,11 +273,7 @@ let get_call_contract ?smoking kf =
   | None -> cc
   | Some s ->
       let g = smoke kf ~id:"dead_call" ~unreachable:s () in
-      { cc with
-        call_smoke = [ g ] ;
-        call_post = cc.call_post ;
-        call_exit = cc.call_exit ;
-      }
+      { cc with contract_smoke = [ g ] }
 
 (* -------------------------------------------------------------------------- *)
 (* --- Code Assertions                                                    --- *)

src/plugins/wp/cfgAnnot.mli

@@ -91,16 +91,16 @@ val get_loop_contract : ?smoking:bool ->
 (* --- Property Accessors : Call Contracts                                --- *)
 (* -------------------------------------------------------------------------- *)
 
-type call_contract = {
-  call_pre : pred_info list ;
-  call_post : pred_info list ;
-  call_exit : pred_info list ;
-  call_smoke : pred_info list ;
-  call_assigns : assigns ;
+type contract = {
+  contract_pre : pred_info list ;
+  contract_post : pred_info list ;
+  contract_exit : pred_info list ;
+  contract_smoke : pred_info list ;
+  contract_assigns : assigns ;
 }
 
 val get_precond_at : kernel_function -> stmt -> pred_info -> pred_info
-val get_call_contract : ?smoking:stmt -> kernel_function -> call_contract
+val get_call_contract : ?smoking:stmt -> kernel_function -> contract
 
 (* -------------------------------------------------------------------------- *)
 (* --- Clear Tablesnts                                                    --- *)

src/plugins/wp/cfgCalculus.ml

@@ -99,8 +99,7 @@ let is_active_mode ~mode ~goal (p: Property.t) =
   | IPDecrease { id_ca = Some ca } -> is_selected_ca mode ~goal ca
   | IPComplete _ | IPDisjoint _ -> is_default_bhv mode
   | IPOther _ -> true
-  | IPFrom _ | IPGlobalInvariant _ | IPTypeInvariant _ ->
-      (*TODO: is it in pass or not ? *) assert false
+  | IPFrom _ | IPGlobalInvariant _ | IPTypeInvariant _
   | IPAxiomatic _ | IPAxiom _ | IPLemma _
   | IPExtended _ | IPBehavior _
   | IPReachable _ | IPPropertyInstance _
@@ -304,13 +303,13 @@ struct
          WpLog.SmokeDeadcall.get ()
       then Some s else None in
     let c = CfgAnnot.get_call_contract ?smoking kf in
-    let p_post = List.fold_right (prove_property env) c.call_smoke wr in
-    let p_exit = List.fold_right (prove_property env) c.call_smoke env.wk in
+    let p_post = List.fold_right (prove_property env) c.contract_smoke wr in
+    let p_exit = List.fold_right (prove_property env) c.contract_smoke env.wk in
     let w_call = W.call env.we s r kf es
-        ~pre:c.call_pre
-        ~post:c.call_post
-        ~pexit:c.call_exit
-        ~assigns:c.call_assigns
+        ~pre:c.contract_pre
+        ~post:c.contract_post
+        ~pexit:c.contract_exit
+        ~assigns:c.contract_assigns
         ~p_post ~p_exit in
     if is_default_bhv env.mode then
       let pre =
@@ -318,7 +317,7 @@ struct
             if is_selected_callpre env p then
               Some (CfgAnnot.get_precond_at kf s p)
             else None
-          ) c.call_pre
+          ) c.contract_pre
       in W.call_goal_precond env.we s kf es ~pre w_call
     else w_call