diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle index 6a9d0d76d5bf3e1ba27de6b20d4b44ee07820c23..a9538e54c89821a6f8c7d562fae1dae738cea2d1 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle +++ b/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 diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle index 8bccdefb12eafaac722c3254b53bfa3198d7eb9d..219867a51e043e72526ac820fa3552b925fac17d 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle +++ b/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 diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml index 98b350f6eb6a6254cb254de4be8f6f4ccaa877a4..16a29702a4b7e841355528775337a6c58abc7371 100644 --- a/src/plugins/wp/wpAnnot.ml +++ b/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