diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i b/src/plugins/wp/tests/wp_plugin/dynamic.i index 29074a3725889a4838217a6e0b0fb23820de4ad4..5f99f4d359485c90c2660c6eb9867ed0a61ac87b 100644 --- a/src/plugins/wp/tests/wp_plugin/dynamic.i +++ b/src/plugins/wp/tests/wp_plugin/dynamic.i @@ -1,11 +1,11 @@ /* run.config - OPT: -wp-dynamic -wp-msg-key "calls" -wp-skip-fct="guarded_call" - OPT: -wp-dynamic -wp-msg-key "calls" -wp-fct="guarded_call" -wp-no-let + OPT: -kernel-msg-key "dyncalls" -wp-skip-fct="guarded_call" + OPT: -kernel-msg-key "dyncalls" -wp-fct="guarded_call" -wp-no-let */ /* run.config_qualif - OPT: -wp-dynamic -wp -wp-skip-fct="guarded_call" - OPT: -wp-dynamic -wp -wp-fct="guarded_call" -wp-no-let + OPT: -wp -wp-skip-fct="guarded_call" + OPT: -wp -wp-fct="guarded_call" -wp-no-let */ //----------------------------------------------------------------------------- /*@ diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle index 2f88edb1b0627c657c8fc40f61b990172364e794..bececbaad42cafd8511a33f73a9fd62c20824cb0 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle @@ -1,15 +1,15 @@ # frama-c -wp [...] [kernel] Parsing dynamic.i (no preprocessing) [wp] Running WP plugin... -[wp:calls] Computing dynamic calls. -[wp] dynamic.i:32: Calls f1 f2 -[wp] dynamic.i:46: Calls g -[wp] dynamic.i:67: Calls h1 h2 -[wp] dynamic.i:80: Calls (for bhv1) h1 h2 h0 -[wp] dynamic.i:80: Calls (for bhv0) h1 h2 h0 -[wp] dynamic.i:89: Calls h1 -[wp] dynamic.i:102: Calls unreachable_g -[wp:calls] Dynamic call(s): 6. +[kernel:dyncalls] Computing dynamic calls. +[kernel:dyncalls] dynamic.i:32: Calls (for default!) f1 f2 +[kernel:dyncalls] dynamic.i:46: Calls (for default!) g +[kernel:dyncalls] dynamic.i:67: Calls (for default!) h1 h2 +[kernel:dyncalls] dynamic.i:80: Calls h1 h2 h0 +[kernel:dyncalls] dynamic.i:80: Calls h1 h2 h0 +[kernel:dyncalls] dynamic.i:89: Calls (for default!) h1 +[kernel:dyncalls] dynamic.i:102: Calls (for default!) unreachable_g +[kernel:dyncalls] Dynamic call(s): 6. [wp] Warning: Missing RTE guards [wp] dynamic.i:80: Warning: Missing 'calls' for default behavior diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.1.res.oracle index b8dbe6a04e4341d99182d7b7dae57ba8ff9534c6..ce2177fcedb4ee8f324535a46daf2fd3cc9c9daa 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.1.res.oracle @@ -1,15 +1,15 @@ # frama-c -wp -wp-no-let [...] [kernel] Parsing dynamic.i (no preprocessing) [wp] Running WP plugin... -[wp:calls] Computing dynamic calls. -[wp] dynamic.i:32: Calls f1 f2 -[wp] dynamic.i:46: Calls g -[wp] dynamic.i:67: Calls h1 h2 -[wp] dynamic.i:80: Calls (for bhv1) h1 h2 h0 -[wp] dynamic.i:80: Calls (for bhv0) h1 h2 h0 -[wp] dynamic.i:89: Calls h1 -[wp] dynamic.i:102: Calls unreachable_g -[wp:calls] Dynamic call(s): 6. +[kernel:dyncalls] Computing dynamic calls. +[kernel:dyncalls] dynamic.i:32: Calls (for default!) f1 f2 +[kernel:dyncalls] dynamic.i:46: Calls (for default!) g +[kernel:dyncalls] dynamic.i:67: Calls (for default!) h1 h2 +[kernel:dyncalls] dynamic.i:80: Calls h1 h2 h0 +[kernel:dyncalls] dynamic.i:80: Calls h1 h2 h0 +[kernel:dyncalls] dynamic.i:89: Calls (for default!) h1 +[kernel:dyncalls] dynamic.i:102: Calls (for default!) unreachable_g +[kernel:dyncalls] Dynamic call(s): 6. [wp] Warning: Missing RTE guards Goal Call point g in 'guarded_call' at instruction (file dynamic.i, line 46):