Commit 474f91e0 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'master' into fix/wp/assigns-cfg

parents dc9ee50f 2511f4c1
......@@ -72,6 +72,10 @@
lexbuf.lex_curr_p <-
{ lexbuf.lex_curr_p with pos_lnum = succ lexbuf.lex_curr_p.pos_lnum }
(*TODO[LC] Think about projectification ... *)
let dkey = Wp_parameters.register_category "includes"
let dkey_driver = Wp_parameters.register_category "driver"
let rec conv_bal default (name,bal) =
match bal with
| `Default -> conv_bal default (name,default)
......@@ -460,7 +464,7 @@ and bal = parse
let load_file ?(ontty=`Transient) file =
try
let path = Datatype.Filepath.of_string file in
Wp_parameters.feedback ~ontty "Loading driver '%a'"
Wp_parameters.feedback ~dkey:dkey_driver ~ontty "Loading driver '%a'"
Datatype.Filepath.pretty path;
let driver_dir = Filename.dirname file in
let inc = open_in file in
......@@ -482,10 +486,6 @@ and bal = parse
~current:false
"Error in driver '%s': %s" file (Printexc.to_string exn)
(*TODO[LC] Think about projectification ... *)
let dkey = Wp_parameters.register_category "includes"
let dkey_driver = Wp_parameters.register_category "driver"
let loaded : (string list, driver) Hashtbl.t =Hashtbl.create 10
let load_driver () =
let drivers = Wp_parameters.Drivers.get () in
......
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp/bug_rte.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[rte] annotating function bug
------------------------------------------------------------
Function bug
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/cfg_loop.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function loop_continue
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/sharing.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
---------------------------------------------
......
......@@ -3,7 +3,6 @@
[kernel] tests/wp/stmtcompiler_test.i:136: Warning:
Body of function if_assert falls-through. Adding a return statement
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp/stmtcompiler_test.i:145: Warning:
No code nor implicit assigns clause for function behavior1, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/stmtcompiler_test_rela.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function empty
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/wp_behav.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] tests/wp/wp_behav.c:172: Warning:
Ignored specification 'for b1' (generalize to all behavior)
[wp] Warning: Missing RTE guards
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/wp_behavior.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function behaviors
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/wp_behavior.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function behaviors
......
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp/wp_call_pre.c:53: Warning:
No code nor implicit assigns clause for function g, generating default assigns from the prototype
[kernel] tests/wp/wp_call_pre.c:53: Warning:
......
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp/wp_call_pre.c:53: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
......
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp/wp_call_pre.c:53: Warning:
No code nor implicit assigns clause for function g, generating default assigns from the prototype
[kernel] tests/wp/wp_call_pre.c:53: Warning:
......
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp/wp_call_pre.c:53: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
......
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
Goal Pre-condition 'qed_ok,Rstmt' at instruction (file tests/wp/wp_call_pre.c, line 47):
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/wp_eqb.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp:print-generated]
......
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp/wp_strategy.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function bts0513
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/wp_strategy.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function default_behaviors with behavior default_for_stmt_54
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/arith.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Global
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assign_array.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function jobA
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assigned_initialized_memtyped.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function array
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment