diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i b/src/plugins/wp/tests/wp_plugin/dynamic.i index 6ff90d2effdb54a71cafae02e7440d08da70e788..e1c5eed1bdab73780be3b8d245133964e7cabb43 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 d32fd01c4b0275d310244a14cd5f62e87a174fa6..bf4dd0108f3be3b7038c570ea0b70f0009c67574 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 a9a4d1e883ab5c873a2288103cb142346e09fdae..b3976cc55b41db5a9b3dd360f5feb8055a32b281 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