From e949c8fb2eb2be962dc58a58b103236c9b76a9ad Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Tue, 6 Sep 2022 19:24:07 +0200 Subject: [PATCH] [wp] update test on dynamic calls following move to kernel --- src/plugins/wp/tests/wp_plugin/dynamic.i | 8 ++++---- .../wp_plugin/oracle/dynamic.0.res.oracle | 18 +++++++++--------- .../wp_plugin/oracle/dynamic.1.res.oracle | 18 +++++++++--------- 3 files changed, 22 insertions(+), 22 deletions(-) diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i b/src/plugins/wp/tests/wp_plugin/dynamic.i index 29074a37258..5f99f4d3594 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 2f88edb1b06..bececbaad42 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 b8dbe6a04e4..ce2177fcedb 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): -- GitLab