[WP] prettier warning when missing calls

src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle

@@ -11,8 +11,7 @@
 [wp] tests/wp_plugin/dynamic.i:100: Calls unreachable_g
 [wp:calls] Dynamic call(s): 6.
 [wp] Loading driver 'share/wp.driver'
-[wp] tests/wp_plugin/dynamic.i:78: Warning: 
-  Missigns 'calls' clause dedicated to dynamic calls (see WP manual)
+[wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior
 [wp] Warning: Missing RTE guards
 ------------------------------------------------------------
   Function behavior with behavior bhv1

src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle

@@ -2,8 +2,7 @@
 [kernel] Parsing tests/wp_plugin/dynamic.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
-[wp] tests/wp_plugin/dynamic.i:78: Warning: 
-  Missigns 'calls' clause dedicated to dynamic calls (see WP manual)
+[wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior
 [wp] Warning: Missing RTE guards
 [wp] 51 goals scheduled
 [wp] [Qed] Goal typed_behavior_stmt_calls_h1_h2_for_bhv1 : Valid

src/plugins/wp/wpAnnot.ml

@@ -219,6 +219,10 @@ let name_of_asked_bhv = function
   | FunBhv None -> Cil.default_behavior_name
   | StmtBhv (_, _, _, bhv) -> bhv.b_name
 
+let asked_bhv = function
+  | FunBhv None -> None
+  | FunBhv (Some bhv) | StmtBhv (_,_,_,bhv) -> Some bhv.b_name
+
 (* This is to code what properties the user asked for in a given behavior. *)
 type asked_prop =
   | AllProps
@@ -765,11 +769,15 @@ let get_call_annots config v s fct =
   | Cil2cfg.Static kf -> add_call_annots config s kf l_post empty
 
   | Cil2cfg.Dynamic _ ->
-      let calls = Dyncall.get ~bhv:(name_of_asked_bhv config.cur_bhv) s in
+      let bhv = asked_bhv config.cur_bhv in
+      let calls = Dyncall.get ?bhv s in
       if calls=[] then
         begin
           Wp_parameters.warning ~once:true ~source:(fst (Stmt.loc s))
-            "Missigns 'calls' clause dedicated to dynamic calls (see WP manual)";
+            "Missing 'calls' for %s"
+            (match bhv with
+             | None -> "default behavior"
+             | Some b -> b) ;
           let annots = WpStrategy.add_call_assigns_any WpStrategy.empty_acc s in
           WpStrategy.empty_acc, (annots , annots)
         end