Skip to content
Snippets Groups Projects
Commit e949c8fb authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[wp] update test on dynamic calls following move to kernel

parent f8931ddf
No related branches found
No related tags found
No related merge requests found
/* 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
*/
//-----------------------------------------------------------------------------
/*@
......
# 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
......
# 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):
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment