[wp] fix cfg-infos annots

src/plugins/wp/cfgCalculus.ml

@@ -277,7 +277,10 @@ struct
           | None ->
               match Dyncall.get ~bhv:env.mode.bhv.b_name s with
               | None ->
-                  WpLog.warning ~once:true "Missing dynamic-call infos." ;
+                  WpLog.warning ~once:true "Missing 'calls' for %s"
+                    (if Cil.is_default_behavior env.mode.bhv
+                     then "default behavior"
+                     else env.mode.bhv.b_name) ;
                   let any = WpPropId.mk_stmt_assigns_any_desc s in
                   W.use_assigns env.we None any (W.merge env.we w env.wk)
               | Some(prop,kfs) ->

src/plugins/wp/cfgInfos.ml

@@ -72,6 +72,51 @@ let selected ~bhv ~prop pid =
   (prop = [] || WpPropId.select_by_name prop pid) &&
   (bhv = [] || WpPropId.select_for_behaviors bhv pid)
 
+let selected_default ~bhv =
+  bhv=[] || List.mem Cil.default_behavior_name bhv
+
+let selected_name ~prop name =
+  prop=[] || WpPropId.are_selected_names prop [name]
+
+let selected_assigns ~prop = function
+  | Cil_types.WritesAny -> false
+  | _ -> selected_name ~prop "@assigns"
+
+let selected_allocates ~prop = function
+  | Cil_types.FreeAllocAny -> false
+  | _ -> (selected_name ~prop "@allocates" || selected_name ~prop "@frees")
+
+let selected_precond ~prop ip =
+  prop = [] ||
+  let tk_name = "@ensures" in
+  let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
+  WpPropId.are_selected_names prop (tk_name :: tp_names)
+
+let selected_postcond ~prop (tk,ip) =
+  prop = [] ||
+  let tk_name = "@" ^ WpPropId.string_of_termination_kind tk in
+  let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
+  WpPropId.are_selected_names prop (tk_name :: tp_names)
+
+let selected_requires ~prop (b : Cil_types.funbehavior) =
+  List.exists (selected_precond ~prop) b.b_requires
+
+let selected_call ~bhv ~prop kf =
+  bhv = [] && List.exists (selected_requires ~prop) (Annotations.behaviors kf)
+
+let selected_disjoint_complete ~bhv ~prop =
+  selected_default ~bhv &&
+  ( selected_name ~prop "@disjoint_behaviors" ||
+    selected_name ~prop "@disjoint_behaviors" )
+
+let selected_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
+  (bhv = [] || List.mem b.b_name bhv) &&
+  begin
+    (selected_assigns ~prop b.b_assigns) ||
+    (selected_allocates ~prop b.b_allocation) ||
+    (List.exists (selected_postcond ~prop) b.b_post_cond)
+  end
+
 (* -------------------------------------------------------------------------- *)
 (* --- Calls                                                              --- *)
 (* -------------------------------------------------------------------------- *)
@@ -143,6 +188,10 @@ let compile Key.{ kf ; bhv ; prop } =
   (* Root Reachability *)
   let v0 = cfg.entry_point in
   Vhash.add infos.unreachable v0 false ;
+  (* Spec Iteration *)
+  if selected_disjoint_complete ~bhv ~prop ||
+     List.exists (selected_bhv ~bhv ~prop) (Annotations.behaviors kf)
+  then infos.annots <- true ;
   (* Stmt Iteration *)
   Shash.iter
     (fun stmt (src,_) ->
@@ -154,7 +203,9 @@ let compile Key.{ kf ; bhv ; prop } =
          infos.doomed <- Bag.concat infos.doomed (Bag.list pids)
        else
          begin
-           if List.exists (selected ~bhv ~prop) pids
+           if not infos.annots &&
+              ( List.exists (selected ~bhv ~prop) pids ||
+                Fset.exists (selected_call ~bhv ~prop) fs )
            then infos.annots <- true ;
            infos.calls <- Fset.union fs infos.calls ;
          end

src/plugins/wp/wpPropId.ml

@@ -476,13 +476,13 @@ let ident_names names =
   List.filter (function "" -> true
                       | _ as n -> '\"' <> (String.get n 0) ) names
 
-let pred_names p =
+let user_pred_names p =
   let p_names = ident_names p.tp_statement.pred_name in
   if p.tp_kind = Check then "@check"::p_names else p_names
 
 let code_annot_names ca = match ca.annot_content with
-  | AAssert (_, pred)  -> "@assert" :: pred_names pred
-  | AInvariant (_,_,pred) -> "@invariant":: pred_names pred
+  | AAssert (_, pred)  -> "@assert" :: user_pred_names pred
+  | AInvariant (_,_,pred) -> "@invariant":: user_pred_names pred
   | AVariant (term, _) -> "@variant"::(ident_names term.term_name)
   | AExtended(_,_,{ext_name}) -> [Printf.sprintf "@%s" ext_name]
   | _ -> [] (* TODO : add some more names ? *)
@@ -493,7 +493,7 @@ let user_prop_names p =
   let open Property in match p with
   | IPPredicate {ip_kind; ip_pred} ->
       Format.asprintf  "@@%a" Property.pretty_predicate_kind ip_kind ::
-      pred_names ip_pred.ip_content
+      user_pred_names ip_pred.ip_content
   | IPExtended {ie_ext={ext_name}} -> [ Printf.sprintf "@%s" ext_name ]
   | IPCodeAnnot {ica_ca} -> code_annot_names ica_ca
   | IPComplete {ic_bhvs} ->
@@ -511,7 +511,7 @@ let user_prop_names p =
   | IPDecrease {id_ca=Some ca} -> "@decreases"::code_annot_names ca
   | IPDecrease _ -> [ "@decreases" ]
   | IPLemma {il_name = a; il_pred = l} ->
-      let names = "@lemma"::a::pred_names l in
+      let names = "@lemma"::a::user_pred_names l in
       begin
         match LogicUsage.section_of_lemma a with
         | LogicUsage.Toplevel _ -> names
@@ -546,7 +546,7 @@ let user_bhv_names p =
   in Option.fold ~none:fors ~some:(fun b -> b.b_name :: fors) (get_behavior p)
 
 let string_of_termination_kind = function
-    Normal -> "post"
+    Normal -> "ensures"
   | Exits -> "exits"
   | Breaks -> "breaks"
   | Continues -> "continues"

src/plugins/wp/wpPropId.mli

@@ -79,6 +79,7 @@ val get_propid : prop_id -> string (** Unique identifier of [prop_id] *)
 val get_legacy : prop_id -> string (** Unique legacy identifier of [prop_id] *)
 val pp_propid : Format.formatter -> prop_id -> unit (** Print unique id of [prop_id] *)
 
+val user_pred_names: toplevel_predicate -> string list
 val user_bhv_names: Property.identified_property -> string list
 val user_prop_names: Property.identified_property -> string list
 val are_selected_names: string list -> string list -> bool