From 457849ba6ff943ee62a66f598fe076029b38d726 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 24 Jan 2019 15:48:43 +0100
Subject: [PATCH] [WP] prettier warning when missing calls
---
.../wp/tests/wp_plugin/oracle/dynamic.res.oracle | 3 +--
.../tests/wp_plugin/oracle_qualif/dynamic.res.oracle | 3 +--
src/plugins/wp/wpAnnot.ml | 12 ++++++++++--
3 files changed, 12 insertions(+), 6 deletions(-)
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 6a9d0d76d5b..a9538e54c89 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 8bccdefb12e..219867a51e0 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 98b350f6eb6..16a29702a4b 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
--
GitLab