[WP/test]

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)();
 }
 

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

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