From 8b9651b0ab257d07d4bc668e59ca3f4e82aa50a7 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 18 Jan 2019 16:52:36 +0100
Subject: [PATCH] [WP/test]
---
src/plugins/wp/tests/wp_plugin/dynamic.i | 2 +-
src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle | 5 ++++-
.../wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle | 2 ++
3 files changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i b/src/plugins/wp/tests/wp_plugin/dynamic.i
index 6ff90d2effd..e1c5eed1bda 100644
--- a/src/plugins/wp/tests/wp_plugin/dynamic.i
+++ b/src/plugins/wp/tests/wp_plugin/dynamic.i
@@ -74,7 +74,7 @@ int behavior (int (*p)(void)) {
@ assigns \nothing;
@ ensures X1==\old(X1); */
int some_behaviors (int (*p)(void)) {
- //@ calls h1, h2, h0;
+ //@ for bhv1,bhv0: calls h1, h2, h0;
return (*p)();
}
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 d32fd01c4b0..bf4dd0108f3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -5,10 +5,13 @@
[wp] tests/wp_plugin/dynamic.i:30: Calls f1 f2
[wp] tests/wp_plugin/dynamic.i:44: Calls g
[wp] tests/wp_plugin/dynamic.i:65: Calls h1 h2
-[wp] tests/wp_plugin/dynamic.i:78: Calls h1 h2 h0
+[wp] tests/wp_plugin/dynamic.i:78: Calls (for bhv1) h1 h2 h0
+[wp] tests/wp_plugin/dynamic.i:78: Calls (for bhv0) h1 h2 h0
[wp] tests/wp_plugin/dynamic.i:91: Calls unreachable_g
[wp:calls] Dynamic call(s): 5.
[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] 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 a9a4d1e883a..b3976cc55b4 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,6 +2,8 @@
[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] Warning: Missing RTE guards
[wp] 46 goals scheduled
[wp] [Qed] Goal typed_behavior_stmt_for_bhv1_calls_h1_h2 : Valid
--
GitLab