diff --git a/src/plugins/wp/driver.mll b/src/plugins/wp/driver.mll
index 06fc29c30ff8ddb988ac2bc9297ddab8563caa34..9e4d708e49395f25207af0caa10f356244a39d01 100644
--- a/src/plugins/wp/driver.mll
+++ b/src/plugins/wp/driver.mll
@@ -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
diff --git a/src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle b/src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle
index 5d27599429e5f10ea21f937458c88d6c52032373..8e96b463d843796406c704b871a801fd6fbf776e 100644
--- a/src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle b/src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle
index fde404cb14e6dbcb899b1df90bf9bc5c4e843a46..e3e370f250f473cb8875e20f101e9b47b6cfa02e 100644
--- a/src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
index 6a9b973a8bddcd39196f9824696ebc782a926358..1a343c630528b7e9168bb0126b3d7d389f3a8413 100644
--- a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
@@ -1,7 +1,6 @@
# 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
---------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
index bf984a624a755a5b279949cd47ed1c23473c1262..d7c91e8c587cda072659f627edf1409be880ede6 100644
--- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test_rela.res.oracle b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test_rela.res.oracle
index fbd89c4d7c463bd67fdca3170ba6945dd9442966..06fb66f8e03c9eb736c46bff3d8295dc7674e8ca 100644
--- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test_rela.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test_rela.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
index 5db0bbd2e089f7c5811d8009888780310f29455d..5d027100e9993d57ffab79a3eaf4675645c65204 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle
index 9c8ae39d6579bccf309f953d0bb6eb652233c42d..c28768d2976ffbf2d6c9b20e5988bcf6b50cb208 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle
index a1618f682664022f6c47fb2dd1c2b4cc510c20b9..e6e7eac38d3a52d4a34a9410eee8e1b1a7b2a27b 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
index 653c11e9d55b4ef858d0250cdf9c0f6aac06d1ac..308fadbaa3174eed5309c7908a2c3c04383345eb 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
@@ -1,7 +1,6 @@
# 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:
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle
index a11eb1bd13533267d4f6b9d3e980acf8a79decd9..c8d77c934815cd6db79395b4ab9616605d187395 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
index 90c952b11ab801c2c9efffedb44dff22c8d23338..330ae3ce02fdefc65332fe4ef2477b65bc20f885 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
@@ -1,7 +1,6 @@
# 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:
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
index e2054c417374920469a8439b414cb115d54f3094..29adcc554a584024d6373d1168abfae012ab848a 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle
index 42f82c479853582025c316db4b6433e6b100c1b2..2b2fcb498fc51449dccece6ee703b7d4185276d5 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.4.res.oracle
@@ -1,7 +1,6 @@
# 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):
diff --git a/src/plugins/wp/tests/wp/oracle/wp_eqb.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_eqb.res.oracle
index 909dc7f4acb381c3826cc686dd4daab80834e3ed..2ab50ab1a473720ca44010c93006af5f69074bba 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_eqb.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_eqb.res.oracle
@@ -1,7 +1,6 @@
# 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]
diff --git a/src/plugins/wp/tests/wp/oracle/wp_strategy.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_strategy.0.res.oracle
index f9a46f91a873bdf14bf309947068c8ec9f109420..db0e3c425b6e087e9635be7eab73370ce9e72e7b 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_strategy.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_strategy.0.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp/oracle/wp_strategy.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_strategy.1.res.oracle
index 0613c6137dca1ca0f826ad40dd0fc8251e0e88b9..b3d21c9f32f1cee3d6159fdaacaea1e22e053ffb 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_strategy.1.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_strategy.1.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle
index e086a73e2e010e925515733bca74c7992059dc1e..219463ff468295f11b65a46be3f09de1cbf859a8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assign_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assign_array.res.oracle
index a358aef50a348cd9014ed089e6857abaf34da3f2..c7024e87f063a7ffc614d93f8758bd9dd31e52f6 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assign_array.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assign_array.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
index 0e876ef057d58194dae3bd3f882f82b996fd1bda..97405e3f05094dc1e00ff8b5ea4a0116d4336bc0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
@@ -1,7 +1,6 @@
# 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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
index ee074a6bd82978cba93ad34b9370e3b075483db2..a4e3a95a8411e0fad2073413b324aa2485515e56 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assigned_initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function array
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
index 3e39ff665dfca5ddbdd3617d49f40abeeb0024bc..ebcccafc2c730d44c51a8a748fb7a42c124f2c07 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assigned_not_initialized_memtyped.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function array
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memvar.res.oracle
index 34ed9b45a88b966dd72e667d6d5a4d043d988d93..ac2da1bad2c19bb1e74f8aca0043bea66021bdf5 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memvar.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assigned_not_initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function array
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
index 0c4bd8dfbdfced7b662260ad12ba7264848f940e..b8ebbadea5ebd5ac1be8e37f157226b201709da2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assigns_path.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
index 35b9d8777b712221cdd59f1d23729cb2c9156d96..47e610fd2656f2c5ea36eb0cf51ac486776d7645 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function call_assigns_all
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
index da37a8a78a065d2a74d321c598706bed1d4a3084..564b0922bf517645be26e01bd384ba93f17ec04e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/axioms.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
index 545557ea6d64a714e443efaa902b22ca123e0740..436b0b25bccda83473908c41a960a977fff56a72 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/base_offset.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
index 70d1558a270afd984352f05fee911ed8f71bc1c3..320a3fd9ef45d2ece137443e12d54dc8fd2b4ecb 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/bitwise.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function band
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/bitwise2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/bitwise2.res.oracle
index 93a098b82182b131c38a3fba3754d8b758c02d10..107c96ad0ad4ac2eb88940c98f7ff9726181977f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/bitwise2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/bitwise2.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job1
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle
index a3bc5a8c09bbefbfedf38d930c39ae2c8c780c59..30094770c411e4aa75176fddc8e066d4a72b9dd0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/block_length.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
index ea971496a84eeef7fce6ea5c19ceae7878256dec..61274ae7016221aea497a6e1da08c24d18c39a02 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/boolean.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_u8_is_continue_assigns_part3 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
index bae891952be7ca996280d35951a229bd1336993e..795c0dfaafc34ca26946948a2665e97dde5f859d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle
index 6de4c09508772db4e0a498cd8342d9401c6e88eb..d9362c1ce5cc1fe74d725ed4624ae6a958693cf7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
index db600bf51f7bba62adcd95988f5b589ddb7fa068..38d790b5a4d7ec91bd75576bd168291c4eac1231 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index 72d6142a7ae9a1b19088aa984720d20caba2956c..8df080b73dbf0ccb41efe60f2e256eb3f86c0d4b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_acsl/chunk_typing.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function function
------------------------------------------------------------
Function function
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
index f066a94e1eb05f0ceb3f905405e624205a997b7a..40c1a5853ba9a3b15b69d970d38ae3fd4867bcf2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_acsl/chunk_typing_usable.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function usable_axiom
[rte] annotating function usable_lemma
[wp] 3 goals scheduled
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
index 8ce615934da8264b474018856ccfe959b005583b..27e7dccf57532b66742c01ee93edb017b646013d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Global
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/ctor.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/ctor.res.oracle
index 6a6bd49b1a01dafc18260e0d12b3ddff5141c855..dc62954e6b56dc190839ba2e88927577dc635871 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/ctor.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/ctor.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/ctor.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Axiomatic 'Event'
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/div_mod.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/div_mod.res.oracle
index 91eb8c84ada2f687e4648035e003eaac5f5bd9b9..670b0774270e298341dd46d12f96d11cc431aa67 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/div_mod.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/div_mod.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/e_imply.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/e_imply.res.oracle
index b6ef93ebb149ffb7d229fb2a13648258cbd2db62..ea5fa8f594547d2bf9cc4d1969c692bad80c8188 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/e_imply.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/e_imply.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/e_imply.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
index 3a3c58f00c05df2dbf9f333e5bcb987f3ed4fc9b..a543f1f54a26874ef7f4f376be1c4b2d51369253 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/equal.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function simple_array
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
index b43e2d4a8152b36cd0531f01f796d4665b036ec1..54ae1cc9e6b493c54f2fbed3298c0e419efb64b3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Global
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
index d1a648f8189a2f4429714cfb27e2cf3890c45531..47c04b9140b066c0dc43a1ac6cec9c18ac6744db 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
@@ -5,7 +5,6 @@
[kernel:parser:decimal-float] tests/wp_acsl/float_const.i:19: Warning:
Floating-point constant 0.1 is not represented exactly. Will use 0x1.999999999999ap-4.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
[wp:print-generated]
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
index 98e419a07aee8ba4ba48cee5ccb3604e37bc21c3..2c16374dc4ab5dda44513eea004949b6fed2b4f0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp_acsl/funvar_inv.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_acsl/funvar_inv.i:24: Warning:
Can not compare pointers in Empty model
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle
index 1e8b67744c38ef7bd61f9b0ed242afdea349b035..9ed2d133feedc53a1329bd81aaf5f4c4960d8e9d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_acsl/funvar_inv.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
index 6b7463a9cd6fe372fa0d12a2c30aa428cbe48498..233aa076c4f47f9a17aefdc2159597328de1ab61 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Axiomatic 'Th'
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/implicit_enum_cast.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/implicit_enum_cast.res.oracle
index eb1d9e231e865f0617f96b469f30cf34c5808723..42361373ebac6c8663e3e5546108a194331eb896 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/implicit_enum_cast.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/implicit_enum_cast.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/implicit_enum_cast.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function bar
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
index a1016679f96bf1124f0d163eec275e1e005514b5..5a0fc4b056cc4d4e20fa1c9abef0dcf5cf6072f2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/inductive.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] 3 goals scheduled
---------------------------------------------
--- Context 'typed' Cluster 'Compound'
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
index fa3df7a23c2dfe79628ecb33c9faafbe31eaed1d..d6d7a763dabdbea22d9406d84cb02d2b21587f8d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/init_label.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp_acsl/init_label.i:27: Warning:
No code nor implicit assigns clause for function main, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
index ce62bdd3dcb6bc382affb839cfc6bc059ffb20a3..c072c17ac8b64cf178f59ff7f1087f5bcdb32880 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-no-let [...]
[kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function fa1
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
index ec03acf8c197dad4cb8666eb3bd4c9c80359baf1..9501f9dee9b89f89211b0539e9b92a7d6dd01576 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-no-let [...]
[kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function fa1
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle
index 2e42b9e3cb6a8630994a1fb4c7b1a47a9d35b696..c1cd26ad0172b9be22729b1c29f15e9e44681a06 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/init_value_mem.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle
index 9a56e40c6559a000edbcd84c661d7d221bdb1f6d..c84b034766cb8247a37687e4559607b6510b27eb 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp_acsl/init_value_mem.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_acsl/init_value_mem.i:24: Warning:
Can not load value in Empty model
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
index 391310e752a810f4c24a79f1233708b798619757..106088887237948475c2ecd809f1749403db46fb 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/initialized_memtyped.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function formal
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle
index a243863d16ac7d5d0b344bbedb01ec951f90f0e4..5a91bd928d651804096c4ff7df91b8872952db8d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function globals
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/intbool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/intbool.res.oracle
index 753b578819b62e9364dbca8337b287cebf45f950..be8e2dc018cf0f402c6f5db0a4ed3f9484ec68fe 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/intbool.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/intbool.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/intbool.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function bug
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle
index f1bb59e94b46d298d0042efddae2e4398c206640..a9d75cace6c480bb82fe3bd6f959244041928bb4 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/invalid_pointer.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_acsl/invalid_pointer.c:21: Warning: void object
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/label_escape.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/label_escape.res.oracle
index 69e92d2508b73b01a15556d24710437e2dab2264..4fca509b7392b2e7a3b27d079450d68e8503c62e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/label_escape.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/label_escape.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/label_escape.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
index 85d318865a1934c7bb5c8f657a5ea7317cb64852..631003d71ae2bd9f15345fe79b47e6560a2aa869 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/logic.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_acsl/logic.i:65: Warning:
Cast with incompatible pointers types (source: __anonstruct_Buint_4*)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle
index d6d7c7ffd7f9c9eccad217d19b140b14684eb9d4..c4c9cd16d8a6f2fab6c268ab7db6f9a08b92b855 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/looplabels.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function copy
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle
index 7d61a351b3eaf5debd682c5568fa7e3159307953..16ac874aa695270bd9cf2784c559eb4e32c7fa23 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/null.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Global
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
index 76387c61d8110277aae032a327ba43d0482dcd2d..4339266bbaf17b0b122e18a85903f672b452e038 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/pointer.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_acsl/pointer.i:50: Warning:
Uncomparable locations p_0 and mem:t.(0)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/post_result.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/post_result.res.oracle
index 0f84cd85b5cd7a46cd0967aa751957bce8f12f13..ea63412d59c5d71be853ac19c19e87d65ecbae1a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/post_result.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/post_result.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/post_result.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function correct
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle
index 0071a69eb1e7fb791cc0233cb8322a7c9a4b96a0..eac17274f2665b22412eeef5c0f3cdc6d7215b32 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle
@@ -37,7 +37,6 @@
[kernel:annot-error] tests/wp_acsl/precedence.i:176: Warning:
P is not a logic variable. Ignoring code annotation
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function bitwise
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
index cc8be9b8f30eaa467abd089ef3985f5513521604..666a26c85f56963f5b071d371f368c685ab8e46c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/predicates_functions.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] 1 goal scheduled
[wp:print-generated]
theory WP
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/range.res.oracle
index 84774868393af390c003b21be78894daabd7b934..e0054bf13b602a75c7f62e23aa586efff7111dd3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/range.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/range.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/range.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function test
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/reads.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/reads.res.oracle
index 3a8f0e7073f21c2fd8b6fa11751e7b29521945c7..430cdc96add4646c44083c74bfc1b93928ca43d1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/reads.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/reads.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/reads.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle
index da2599913d086186fdfc2beb58e1ef65993d3322..43d8c4d3eceaa9b41e44c062e7c6911fc91ab7ca 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/record.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
index 42be62e61943aacc4721bde62a57dd5b2d7b9a34..f4bf9c3fb0ee68f5f3174bd207003e8881f3eb04 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/simpl_is_type.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function check_acsl
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/sizeof.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/sizeof.res.oracle
index f7f75c471935ecbc0714fc8b0b5e947d60fb64d1..36be29ece00d5befea013d85ab46a0f7ef6cfa1e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/sizeof.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/sizeof.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/sizeof.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function foo
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index 671f41e12dab20cba05bfa5d58879b49162d44be..2e93da0b17ef4d14c9bd0856053b0a18debf5b1e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte -wp-no-let [...]
[kernel] Parsing tests/wp_acsl/struct_fields.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function foo
[wp] 2 goals scheduled
---------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_use_case.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_use_case.res.oracle
index 0c38eb7360b7bfa42438f241c774cb8a16d84fb8..64f1be48e24c86ff4c8a415eec93aa0fa33581d0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_use_case.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_use_case.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
[kernel] Parsing tests/wp_acsl/struct_use_case.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle
index 41bb0db407147d61133f3a2d16373ed8ce45e1a8..ed60c90f28251a77c85ba2795070ecd1e677415e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/sum_types.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] 3 goals scheduled
---------------------------------------------
--- Context 'typed' Cluster 'A_A'
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/tset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/tset.res.oracle
index 50ee7b41eb8b5ccfacdd869f64bc9b502f7f82b3..60245b69a897f75bf1485cc637107cacb55a45d3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/tset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/tset.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/tset.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Global
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/type_guard.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/type_guard.res.oracle
index 272aafaea491f208989b8333e68fb50e0ad5d0ac..795eedf06cd80d6c7b0ebd3e2d5e5384c049503b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/type_guard.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/type_guard.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/type_guard.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle
index fd300d3519d9efe6d15d2ed49b727063784ac000..9cc603d5697fb6981218c143fa1352eff8620530 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/unit_bit_test.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function rotate_left
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle
index d4de7cfa3f0f970563a557098110b87b7e45f8d3..ed47c09c4a64ce354e0558afdac39b0e2c0c76cf 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/unit_bool.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Axiomatic 'Foo'
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unit_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unit_compare.res.oracle
index daf696e3420f36a45f874ab2cb9adacde0e679ec..b0b0dba7b56f820f5ccdc133b8d9012b4f41d519 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/unit_compare.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/unit_compare.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/unit_compare.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
index ba6653276cc75ae8be4101cb33aa82a76395cc3b..0becba4e3779f4a17ec4a22b65cbde6ffa263a4b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/unsupported_builtin.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp_acsl/unsupported_builtin.i:10: Warning:
No code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle
index bb65f617048e92dcc6b68dd241c9719529e8b3be..c617b1318c2d2ecbab5e0c441ba6513bfc85a418 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/user_def_type_guard.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts0708.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts0708.res.oracle
index bcd622025b443a3f54f6d4cf76267067003c2ed0..fc7dbb7557375a27b8f636f82c2ff029d6d9dca5 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts0708.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts0708.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts0708.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
index 6fe18cd99667572b5720131e87fce90b8bddf1f7..8c6fd6aed1b7c5243665509741e7e24b10b1b1d3 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts0843.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f3
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle
index bf5748d6871b1eb64d32887e583b80a946760f7c..0340355af423b21ba8a63a6e43d4a90ecf02a36e 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts779.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle
index 59fb21a87df970d7586c084d7b416099a704bf30..fcb5d4edc8639f9d425fbee2ebd30647340de889 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_bts/bts788.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts986.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts986.res.oracle
index f0a8fc075ef2b1ef704531b09a173e69cbcce599..f7dbfc4d45a09b6b9ad0e8b85880c2960ff53936 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts986.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts986.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts986.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_0896.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_0896.res.oracle
index 2918c8ef8abf5cae6128a95b2987705aa82f5cec..8e39845f5244432af66b2c8cb5089df1639ff511 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_0896.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_0896.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_0896.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1174.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1174.res.oracle
index 0f15882a71638c4b6817b680fb0d30129b4f6887..377b382940609689df319629a70bdfd49c887b52 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1174.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1174.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_1174.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1176.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1176.res.oracle
index f309987b2d579bf867a56342a3c81a72c432cfbd..b56f41848c0865b4acdef17fdac95ef7fa48e55a 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1176.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1176.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_1176.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1360.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1360.res.oracle
index 717419064133157a6bc6d19b725979e2d733fe50..7c44e0c9ee57925c84a2e57dd1e15ff1a96f603f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1360.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1360.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_bts/bts_1360.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function foo_correct
[rte] annotating function foo_wrong
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle
index 07498d37853ed0b526e39db6fbf78d2dfa216971..d59e50a899d25afd1fed7894040cff25c96ebba0 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_1382.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_bts/bts_1382.i:18: Warning:
Cast with incompatible pointers types (source: sint32*) (target: sint8*)
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1462.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1462.res.oracle
index bbb9f2c50e5c2187e02a4836419b5a7a53d54e31..aa5c4e320017bf051c70668612f5c91e0cea0fe1 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1462.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1462.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_1462.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function local
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1586.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1586.res.oracle
index c2ffd640b72c7d3ba1fd4514b60ecd7e4456ca47..4020061d0ec44c03bc9d59578561dc3b7965518b 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1586.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1586.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_1586.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function compute_bizarre with behavior Bizarre
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1588.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1588.res.oracle
index 00b3e3e05a966b9e870ac215440527f43dc9441d..a688528d7bc5b18ca5ddde8d44aa69c4c8583364 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1588.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1588.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_1588.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_bts/bts_1588.i:19: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1601.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1601.res.oracle
index 897003473316c3a94c56e22d00d8626c152a9aa4..a7a44770530b48f65807c1cdfeb42ca20823b9ac 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1601.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1601.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_1601.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function foo
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1647.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1647.res.oracle
index 72a0500b84a012502e2064d05b13353e7d840196..d2d36e4287a387e29ae21351c92540767d685465 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1647.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1647.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_1647.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1776.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1776.res.oracle
index a7a3e7e5f916a0f2f38761dbf8ec5caf0a5d80f8..aff5dc75447d73eeda97747d7a31ae338cbc89c4 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1776.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1776.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_1776.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle
index 66651f78d70d24a450248991ff34bba6060340aa..640c9952226375d9ac25aa5260796f23f8a44c67 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_1828.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function global_frame
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
index 04d57e170900455a062ad50f0c10577dcc0a57d9..5b00c3b48f392cf59718f82003f6f14f9c6376d4 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_bts/bts_1828.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function global_frame
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2040.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2040.res.oracle
index 69059aeba4873a76afba9c3df04a20dd76e0e1ea..3601e1976dd36c501db6dff8996b4430a3abb9cf 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2040.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2040.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_2040.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function call
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle
index 3aaa31af0f66251205832210b85c9d2de28f5238..a59bf7022499d7715b34018a9c0b5b37229f4b9c 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_2079.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
index b1af7c7da5cf23d35ee6e70c4dbfdb89fb3af036..38acae5e6e428d50a0186a79f24373926e87e957 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_2110.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
---------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2159.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2159.res.oracle
index aac7caf8ba126a5f68785b6f0999837bce7388a9..445eee0ff7667ada42e020df177835474aa85f27 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2159.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2159.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_2159.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2201.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2201.res.oracle
index 9669fdaf70d1e473e934014e843acd650c4b1db3..61491a01bbbc8eb4bb111c8c08a71bdf6e391b0a 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2201.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2201.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_2201.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2246.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2246.res.oracle
index 961bf49840094db6af8e8b4f91cc980e5af0bdeb..9d81968e9e5457308a1058107e00dcc574be8b46 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2246.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2246.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_2246.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function bad
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle
index f38cfc4e5fd899a8c35a4e59f8b143d23457487a..550dd7a5454b01100b579c964ea4a0784253e269 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_2501.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] 2 goals scheduled
[wp] 2 goals generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/ergo_typecheck.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/ergo_typecheck.res.oracle
index 694a8eed3ce377d9b01781323efae6aa05baa8a4..5cbab700501139b9988a526165935592e16c5bb3 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/ergo_typecheck.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/ergo_typecheck.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/ergo_typecheck.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
index b37af5db7fee1f02ca661429b7f9954e48c38d54..b7b15905eb28679b166ca6e89fcfb8e5bcbc97c8 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/ex5.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function dummy
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue-364.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue-364.res.oracle
index ae3e885d9102d1aaf30d13185e12852f38e45c0b..cb25cf5612d6889bfaae292402eabc65e15e5e33 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue-364.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue-364.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue-364.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue-516.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue-516.res.oracle
index 9bf1f55fb108cb0f070e334ef8477d3704698b31..7a59fcea651b51295a354f4963df487bc73e6335 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue-516.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue-516.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue-516.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No definition for 'to_logic_list' interpreted as reads nothing
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
index 2b2e6c21c2df88606ff2a10ab33ab0e66f8f3272..cb499212b74e034784cefec5bc0743455477de99 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue-684-exit.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function inconditional_exit
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle
index f84001a741b81c764034372d35bdefbf903406f3..9dd3dd748e7ee050326d660ce198563a2c639db4 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte -wp-steps 50 [...]
[kernel] Parsing tests/wp_bts/issue_141.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function f
[rte] annotating function main
[wp] tests/wp_bts/issue_141.i:18: Warning:
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_198.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_198.res.oracle
index 3995ac6f0b637b0ab3ea9a463f2ed9f6e838ff9e..e7f427ccd5d7c4cafa4fbdc06014a05b965aa853 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_198.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_198.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_198.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Global
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_447.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_447.res.oracle
index e034a5bf910e1e91fc6c1ddb3273ef13ff0805f6..f8dc63d5e2026929898298dece6f3877bb581932 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_447.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_447.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_447.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Global
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle
index 99a9aed869aba27df4dcc5f81f4bf76cb47161f2..9c1dde973cc4e3eb98f278b9b5e659b8b357387b 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_453.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f1
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_494.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_494.res.oracle
index 297b4d981860ff3428f2fa865dc0c1739945acb6..faaeeb6e2dd17053e3ed2dd5f8cb9a5eb2890623 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_494.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_494.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_494.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle
index 179be9f834bcce480b9e2d76af6eea6f591bb5be..69016b5d1ff4920ddce03d5b1be0a83071485b7d 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_508.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function add
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_711.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_711.res.oracle
index 786b948ba145cf3846cd5d627264465f6d001c4a..d30781324d40f3bac332a4451a931fcc924badb3 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_711.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_711.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_711.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Axiomatic 'LISTS'
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle
index 3d37a96e7d7d04c126f309232865a95e64b7cb7c..e41e8f471f50b9d327ff0a48c2556f9a990f57af 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_715_a.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp_bts/issue_715_a.i:6: Warning:
No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
index 06b261910a55579c8431e60213bf9906b379709c..8c82bc192bafd62b31a091cb7954318093d79a85 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_715_b.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp_bts/issue_715_b.i:9: Warning:
No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
index d54cb3838366d89778e8abc0cccae8de0cef42f0..14535c7cf0c072d0d5733260c788e4cb80ebb297 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_751.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function acquire
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle
index 81c0ed9a9db7f1fea76ada3447ea8325532e6c3f..0021dc1ad13f35291453f98e675313a297afc67c 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_801.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function LoopCurrent
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle
index 3c3d2d46a68d9024af31e4d184d6a5d81b5478d4..ede0b64f8b9bb21f73b923ba01523ba756be0499 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_81.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function getMax
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
index 65c234448ba7d4d4dff459d117eb43ab42bf7ee7..6af1e96a96a3ebadd603d0249caef12e68caca2f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_825.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function issue
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle
index d1e95f07802a37aca4d1c87ef2585aad84f75219..6505c959c081e472fd5b92a077fddf9aac826e27 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_837.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function bar
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle
index f3dbc6f8d161250a1dab323a3012745b1929ae9c..d832b6f57960c51cd42578d6398f586a9028bc4f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_898.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle
index 094d64fd5cc15c062e1c9bf26f9235d9517c3538..60c6a834f15bdb4a543704f01696ec53c64f493f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/nupw-bcl-bts1120.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] tests/wp_bts/nupw-bcl-bts1120.i:54: Warning:
[cfg] Forget exits clause of node <blkIn-stmt:26>
[wp] tests/wp_bts/nupw-bcl-bts1120.i:54: Warning:
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
index f573edafe8d54e38b786507fc9900efc9d02cf1f..4a3a4384db14cfb12387b0265f04c6a284b3954f 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte -warn-unsigned-overflow [...]
[kernel] Parsing tests/wp_gallery/binary-multiplication-without-overflow.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function BinaryMultiplication
[wp] Goal typed_lemma_ax1_lack : not tried
[wp] Goal typed_lemma_sizeof_ok_ok : trivial
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle
index 129465cef770b75b8586fd5e8ed73e23198a3561..58d59aef85258fe52c3a1d4b176d66dd618f57cf 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_gallery/binary-multiplication.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function BinaryMultiplication
[wp] Goal typed_lemma_ax1_lack : not tried
[wp] Goal typed_lemma_ax2_lack : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle
index b4f4caaaf02b52cb3b93f4e6c14e4c309f6fa375..e0c5b20b99e274c837850814d215b2f00fee3c5e 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_gallery/find.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function find
[rte] annotating function find_ptr
[rte] annotating function iter_ptr
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle
index 388a5387f67843dbacafd4aad8d4615860dbde18..cdf72d9135a17beec35a1d60cacb9a081f9d7175 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_gallery/frama_c_exo1_solved.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function exo1
[wp] Goal typed_exo1_ensures : not tried
[wp] Goal typed_exo1_ensures_2 : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle
index 01cfab82cf38c1afd040a1dda9d285e2ab0317ab..daf1e9d366bd36406edf6a848378db5cfd4ed352 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte -no-warn-signed-overflow [...]
[kernel] Parsing tests/wp_gallery/frama_c_exo2_solved.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function max_subarray
[wp] Goal typed_max_subarray_ensures : not tried
[wp] Goal typed_max_subarray_ensures_2 : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
index 5976d3b8cb9811ec5402165abf9eb8e73875f2b5..e21f8f5fe4bc97954c318b6c4531baf28e311bc2 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.old.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function equal_elements
[wp] Goal typed_ref_equal_elements_ensures : not tried
[wp] Goal typed_ref_equal_elements_ensures_2 : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
index ea1e78b5835af86328e5457e6ef00796a8e72fa0..0a5004c676571d4ea94cd0cf4e06b37217771f29 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.old.v2.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function equal_elements
[wp] Goal typed_ref_equal_elements_ensures_v1_good : not tried
[wp] Goal typed_ref_equal_elements_ensures_v2_good : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle
index d19091020e7771f01268a28a7d9a158e21d88c20..21850665dd122865783a31dd2f3cc8a23dfb02cc 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.simplified.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function pair
[wp] Goal typed_pair_complete_has_pair_no_pair : trivial
[wp] Goal typed_pair_disjoint_has_pair_no_pair : trivial
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
index 064dce264b9e7e20ae5c3d9799927e9b346ed87c..a73f6deff1e986ca843364662c85eba648bb5c54 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_gallery/frama_c_hashtbl_solved.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function add
[rte] annotating function eq_string
[rte] annotating function hash
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle
index 52b5a0ec02f3a5baff3c2969562156e94d7035b8..128fa9a9dd685b98a91179a3554847a921d39b21 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_gallery/loop-statement.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Goal typed_lemma_Lb : not tried
[wp] Goal typed_loop_statement_ensures_Scond : not tried
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle
index 4b800e901739371d60c357fb1a792f1a9e5ed4b0..832baab84eb61db255327ed172594084b92caa0c 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_hoare/alias_assigns_hypotheses.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function comprehension_alias
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle
index 4eb7ef191811f19d3d46467aa3603eaaa6c668cb..3da623e24931019ca8f1a8fbdc64132f1611c015 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_hoare/alias_assigns_hypotheses.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function comprehension_alias
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/byref.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/byref.0.res.oracle
index 9ec8bc14a7f9fe4e4ede6808f53fa99a9aa0731d..f9c6a96edce7dd37271023e690bf5433412604b6 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/byref.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/byref.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_hoare/byref.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle
index 051a94929b453b37ea0317b9496dcb85fd2c334c..54ad8489278e68186e342fc1157d755cd613d62f 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/byref.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_hoare/byref.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
index bb48a4672be4861c972fbcf9b7ba124c21dd3329..d2646994c22e0a1dbada00d2f6169e04da38ab0e 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
@@ -23,7 +23,6 @@ Function call_two_ref: { r0 tmp tmp_0 __retres }
Function g: { *pg tmp }
Function array_in_struct_param: { sf }
.................................................
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function array_in_struct_param
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
index 09b623d4dfd9a92abc5729a7cad65ff5be38728d..61bf6b67367b214b40e53f5d9d9e9fff16e4a0fe 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' -wp-no-let [...]
[kernel] Parsing tests/wp_hoare/dispatch_var2.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function call_global
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle
index 181d3c1dad2dbe0491b867861f33163305f06fa5..44ae58e7b74ba0fb1e7c7ef27a28f0155be239f7 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_hoare/dispatch_var2.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function call_global
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/isHoare.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/isHoare.res.oracle
index bfbd22dfea9ede3a172f60b032f320deffe4ed9d..31b64ff33371aa2341a89848adec14774f4cec9d 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/isHoare.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/isHoare.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_hoare/isHoare.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function cmp_invalid_addr_as_int
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
index bfb7581b49d7b30852c5599e9368a5d64eb0a6e1..9875c8c8f6706fc59099d8de937fd5c9e2a0d06a 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_hoare/logicarr.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/logicref.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/logicref.res.oracle
index 093b63521e624272f9819a2f9ce9b86db0052f59..0eb822224664ad3e2e81465f27005edaadb02a90 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/logicref.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/logicref.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_hoare/logicref.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function fvrange_n
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle
index e789d39c37d259a3fc4e6803904857355ab6ce39..3d20b3ef6be8edcf0fae09ea401482f89d8faa9f 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle
@@ -10,7 +10,6 @@ Function fsimple_array: { &t __retres }
Function ftwo_star: { d __retres }
Function fvpositive: { b }
.................................................
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function fsimple
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
index 3eef87eaec34b72a92be8b571d96c65ae88bad9e..c6bec6fef0728d4b3598e5ec6ae9d881cbec4150 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_hoare/reference.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function call_f2
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
index 6759eb2c636f866a1eea5da5ef5e124684bd1c0b..6be3aa72874003dc78af525fd268a665aad32185 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_hoare/reference_and_struct.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function call_array_in_struct_param
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
index 98a1e48694b763f6083689d7cfcd3031ed4e789d..2801c12e3a4d356ed5996b851196fd7ed9a0015f 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_hoare/reference_array.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function add_1_5
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
index e71891e1ea8c3057377014b7b78a5fb09e1cff69..2c5447e5d1d9013e345c34ecb12cebb4310f5712 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
@@ -12,7 +12,6 @@ Function call_f2: { tt tmp __retres }
Function f3: { p3[] k }
Function call_f3: { tp tmp }
.................................................
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function call_f1
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
index 884cf8a6f5c6c9df4525cded0ec8fc444841f112..59c0568ee15ab1f2f1a4475f688e303403a07b4b 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_hoare/refguards.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle
index 64ce1c0a27564d7e608fa737f9a2a34baaf37eae..9a4cc9410828748161c0e18f9d4f8515b1f360ea 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/abs.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function abs
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/asm.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/asm.res.oracle
index 250316f99ababe8ff0682c771fc78d39006f344b..0f8a43912a0cc578bfd602dbfe6432b3a3911553 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/asm.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/asm.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/asm.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle
index e56158295b1cdb7d71133f15a396221cf4c508d0..1296b169a5ddc881354e6e23094e3e9b0164a1e5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/bit_test.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function check1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle
index c80bbdfdc621cb262f494654e932dfd5f413cd53..fd6a26d1a47e1e500fb53783e6de294dceaf19ab 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-no-let [...]
[kernel] Parsing tests/wp_plugin/bool.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function band_bool with behavior false
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/call.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/call.res.oracle
index 62179a864c565fca093d10951859a2d2f2bb25e8..5199a49d5ed126e04c5d30fa6fbdf2726c4fab72 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/call.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/call.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/call.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.0.res.oracle
index 887dec881576e06ecd6e8da28ebdabba3c076345..6f58be4f1af5a946f6687e5a557255da6b6eb5bd 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/cint.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.0.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_plugin/cint.i:22: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function signed_bitwise
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.1.res.oracle
index 55a848888ce7a3063bdf829a2956194c3de03aa2..59b50c4132f5a58a210f4d72d5caef95df6a6b96 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/cint.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.1.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_plugin/cint.i:22: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function signed_bitwise
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.2.res.oracle
index c0c5ae7b8c0ce9ec3e83b4a6f2b0c680d12376f2..514e872a60043bdf0a7938905fa9fbbdebfa030b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/cint.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.2.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_plugin/cint.i:22: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function signed_bitwise
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle
index b169564f3f3df677b24cf3f5e545dae534503a67..3aaad8d66c9b1eeefb620fb7bb9f568538e6afba 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_plugin/cint.i:22: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function signed_bitwise
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.4.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.4.res.oracle
index f8b8993817804ee19d6b412d7a610e34bb951503..6530278cbb976598154e0d8dc198ca868fbb12e1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/cint.4.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.4.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_plugin/cint.i:22: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function signed_bitwise
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.5.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.5.res.oracle
index bb09f85e02cb893f5d9ebadfada28384266bd488..064a3b6849118946b732e22b0bd412a0e07b5ee6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/cint.5.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.5.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_plugin/cint.i:22: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function signed_bitwise
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
index 67dda1bd3fcfe40e62b094e3d07c9cda20424268..232d0259c30a3aec71ca0610cdc0af2b68750042 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/combined.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/convert.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/convert.res.oracle
index e322ec1a1e8f4d57752de4bf47dc42db7d917aa4..a05054d57a9a98b37b8307d412ef6ae99757ca51 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/convert.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/convert.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/convert.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Global
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
index a77cbc87bece917435a096dca1398e735a1896d6..2df09a43e2a673bf3e6e8921b8fd05865126d17a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/copy.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function copy
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed.0.res.oracle
index 4f81eda9072a018dd87cb2a73fc93e3c93f55773..0e195c8fcd205635db50093d6a98b9e2cda3d842 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/doomed.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/doomed.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function bar
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle
index 96ea7f28a84972eb67c04bc99bf2ed7e3ceb34c4..07bf46ceb48fa2196aac1041d66a314f86781b30 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/doomed.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function bar
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed_axioms.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed_axioms.res.oracle
index 66b4587a6b7f562ec25be5fd70a303a9af3a5cfb..da669bd36ebf0b30082de682bb0d52b17a6faec3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/doomed_axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed_axioms.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/doomed_axioms.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function foo
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed_loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed_loop.res.oracle
index 665deb24842bdf01369c31d978870e1f34cbfdf4..97103136af1d61d0f9dc62a842e18b5184bc026c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/doomed_loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed_loop.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/doomed_loop.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function foo
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle
index 169321402876d20386d7dd09216dd79310308dda..53bfdc8c969e99993428bf4e063da2a0978394bd 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/doomed_unroll.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/doomed_unroll.i:15: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
index 6e4b15fb4d0a29aad67e97dc0a87dcddf8d33714..e71c6e9ae9aea0d46a37b93de7f0bd295d0e1fb5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -10,7 +10,6 @@
[wp] tests/wp_plugin/dynamic.i:87: Calls h1
[wp] tests/wp_plugin/dynamic.i:100: Calls unreachable_g
[wp:calls] Dynamic call(s): 6.
-[wp] Loading driver 'share/wp.driver'
[wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior
[wp] Warning: Missing RTE guards
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
index 61fd74dd9d815d5a2a045af77e1385a8a47dfeaf..c3ed1e741d463a42a6f13570e273586242789306 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/fallback.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
index 818a355e2d15663d3e04db5fc8769c4944a19d84..d987807fecd4c5359e3a5c1fecdcf86b1f1df7f9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/flash.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
index 312f0897fc58e194cdbbefd4148c717786b6cf1c..31d6bb17966eb81c3efddb017b847781a52d9709 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/flash.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] tests/wp_plugin/flash-ergo.driver:2: Warning:
Redefinition of logic INDEX_init
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle
index 4e5d804718ecf4e93795cd35284e41a6b37edc2e..c1cd5c4035a144f84d1d282586471b9664aa036b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/flash.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle
index f193a1188d9c4316d1ed482ea3b61d2409b14336..d7358dce80b3d94ff5c052884965adccd6c8d92b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_driver.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/float_driver.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 20 goals scheduled
[wp:print-generated]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle
index 85e995df2796c0b54545c3d7c1c66198eb899050..4a8215d591e6f88e181b04cb50a6518f789fad8e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_format.res.oracle
@@ -4,7 +4,6 @@
Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function output
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_model.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_model.0.res.oracle
index a711e372d35c558c31793e43e593b585c74d4731..00f3e8dab4c76c330a7c167e974e51d8c8078a9f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_model.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_model.0.res.oracle
@@ -6,7 +6,6 @@
Floating-point constant 2.1 is not represented exactly. Will use 0x1.0cccccccccccdp1.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_model.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_model.1.res.oracle
index 55eefc41f89dc07ca8ef43882bed889ce252e363..7fbd6b3ca7bdb5449c6a81d4457b4acc712d3681 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_model.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_model.1.res.oracle
@@ -6,7 +6,6 @@
Floating-point constant 2.1 is not represented exactly. Will use 0x1.0cccccccccccdp1.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle
index 7e9d87ee00d3dd9b55bebc69d8dca822bcc85c19..39e9f3d83596b5d28e157b5556f5c0450b7badb0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle
@@ -4,7 +4,6 @@
Floating-point constant 1e-5 is not represented exactly. Will use 0x1.4f8b588e368f1p-17.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function dequal
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
index 4249f034461a465c794b76fe03bd9cf26e1fa735..acae1296cda548c49122e49e55befe3e44cd1d16 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
@@ -4,7 +4,6 @@
Floating-point constant 1e-5 is not represented exactly. Will use 0x1.4f8b588e368f1p-17.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function dequal
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle
index 3ef9251b463a17273f447723b675e76ea8aaf660..b48c65edf9e1ad6aa5e63ca9ca24a01d79f5bece 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/frame.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function alias
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/ground_real.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/ground_real.res.oracle
index ca03a014002a019fe3f06c6d7df1784c9312230d..1777e7e419823d03a7333505f6b74efa093807fc 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/ground_real.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/ground_real.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/ground_real.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Global
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
index e9c5272c0cdca9ab2197a3eedc111a93dd229da1..56fce1fae014c63f99ea466d2d9e3981f3f7ea77 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/inductive.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 2 goals scheduled
[wp:print-generated]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle
index dcdf495be1735ff0bb52b336f437ad08c3bf7eba..46f3cde2efb264d10baff2ace945c9c5420c50ec 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/init_const.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function fA
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle
index 3fcaa7780cb793ba02ac972a510be04169f3473f..1b028ec86bae7521af2821488cc935e87f17bae6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/init_const_guard.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/init_extern.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/init_extern.res.oracle
index 25a6346f68a786c06d4f2519dea4a3783118bd0e..4fb7c09c0aa6b08007c34a255858fbfd3b5ca5a9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/init_extern.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/init_extern.res.oracle
@@ -2,7 +2,6 @@
[kernel] Parsing tests/wp_plugin/init_extern.i (no preprocessing)
[kernel] Parsing tests/wp_plugin/init_linker.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/init_valid.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/init_valid.res.oracle
index c816306f8dfa030a9b13ecb7b3f75924b3ff959b..c630d5f5437f03e7d42293b302cdca2568cb3bee 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/init_valid.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/init_valid.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/init_valid.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function validA
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle
index 402be8d8ac5c7095d9994c3ce980543ce67da025..296121a1db1ff800e6f48a6fc03fce1cba2d5620 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/initarr.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle
index 9f80dffaa4d14bf53dbc7dcf512eb9a6331d9cb8..1ac8bbc1f3f459984a7a6b40e72e777fbc165f77 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/injector.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle
index 7b4df2e87f0cc1ffd85fabb51bab664caa53999a..fb1d1f3185b5bf46c75c4b4fe15662149d1b093c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/invertible.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp_plugin/invertible.i:17: Warning:
No code nor implicit assigns clause for function main, generating default assigns from the prototype
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
index 9dd899de5f15ff0d23edd240f05b69e72668c3f6..42f63d8aedbeb628172cc98d3ac216fdde2e2b4e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/loop.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function init
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/loopcurrent.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loopcurrent.res.oracle
index b477c37199d8f28da5dc2efc674670cde8b5d82f..a562cec21c990ee024f6d5a25157be8e176e53e9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/loopcurrent.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/loopcurrent.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/loopcurrent.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/loopcurrent.i:12: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/loopentry.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loopentry.res.oracle
index 991c9e2a2de44403278260c77aaa0ea3bcf0b432..fad72a0a7693a1a1d22c79a43cfe2858e82d774a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/loopentry.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/loopentry.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/loopentry.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/loopentry.i:12: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/loopextra.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loopextra.res.oracle
index a01b081f52511f2932f410f40aedec9dec52731a..ba2abdd43f81268c465ed20737613b5b7eb69c3f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/loopextra.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/loopextra.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/loopextra.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/loopextra.i:6: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/mask.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/mask.res.oracle
index 93ca42d9b44d684819608d755f462af193455015..ee4cd2e5dd9e372305e6ff4acc2a01582e583bb8 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/mask.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/mask.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/mask.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function compute
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle
index 8faae9123de65263f8a1c05d7223a290584d9654..738cdb2ffba8c36d383642c39e2778c8bd518fd3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Global
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
index b0884297aa8fac4251acf6f6080b971962d49504..743c3bfc6a9d9b1c3becd821353a341a51ea2ce3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_plugin/model.i:10: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
---------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle
index 134cf5cfbb8c57d81ee16894ba4537b84276e946..78a2178dc9531c58407c5c11cde605ea4fbcfd5e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle
@@ -1,6 +1,5 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/nowp.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] No proof obligations
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
index 13e8d343c16cb3559600976958b8ec8014719ead..565ac6b571e7eea4ba8381807c1b66aa60b66c55 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/nth.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Axiomatic 'Nth'
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle
index d314b7d06ef44618e72c98a0e90b6eb50d2f31b2..5392e0e5e2bbbebc8a843d784fa3e16fb565cbda 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/overarray.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f1_ok
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
index c0547370f6fd1fd42458c7e2d7542f96ea29c8b0..a3bcc315fdac6c66cfa7881ddf59d613adc25e89 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/overassign.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f1_ok
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/params.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/params.res.oracle
index 06390f953027618fcb5e31859d50f89d565d1ffd..b61273a928c127ddb95c816feb979e425f967971 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/params.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/params.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/params.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Global
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/plet.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/plet.res.oracle
index 8b4eb23ef7f431f7d47dd07aadaa8bf3f9631f5b..6dafe4cc77a16fbc972deabce8e93a237da882f5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/plet.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/plet.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/plet.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Axiomatic 'Test'
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
index ec3540368c3c5c7d195fb1ee82d527553e30fc70..0697c55a730d66e76ef9f11d90bfc7c1664240ff 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/prenex.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function diag
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
index 1ece42d9dc380401bdc2379bcb8760d9f2397786..02280de6dca96be0cbd3c7204c43b7f3599919be 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/repeat.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/repeat.c:47: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle
index 7eb7d1df64d15f0802d3c205dd74814362f05313..979f8d1dcd4039fe328b62722013317352985167 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_plugin/rte.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp:rte] function job: generate rte for memory access
[wp:rte] function job: generate rte for division by zero
[wp:rte] function job: generate rte for signed overflow
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle
index 3136da68bb235fb56970a9d05c9f02b05d682be7..14242727aae2d7a8ca563f10313a0ad855189af5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte -no-warn-signed-overflow [...]
[kernel] Parsing tests/wp_plugin/rte.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp:rte] function job: generate rte for memory access
[wp:rte] function job: generate rte for division by zero
[wp:rte] function job: generate rte for invalid bool value
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle
index ec0f537db15872e38aaeca0f1dee10c1a13c2932..a19a1e491e60eb7ebdfb54fedfaddfd717ad9623 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte -warn-unsigned-overflow [...]
[kernel] Parsing tests/wp_plugin/rte.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp:rte] function job: generate rte for memory access
[wp:rte] function job: generate rte for division by zero
[wp:rte] function job: generate rte for signed overflow
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle
index d5189e5215a283b655aa75b3a1ae42fa67f16bcb..0e988b3631124ef9c85bdb13ad170abe2e1b3461 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte -wp-model 'Typed (Nat)' [...]
[kernel] Parsing tests/wp_plugin/rte.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp:rte] function job: generate rte for memory access
[wp:rte] function job: generate rte for division by zero
[wp:rte] function job: generate rte for signed overflow
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle
index 7a1f8d5436279e560433b649dcea25b9b81b151c..e9d3ee4047ace47e692ce22e6e5aec6980a4b7c1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte -wp-model 'Typed (Nat)' -warn-unsigned-overflow [...]
[kernel] Parsing tests/wp_plugin/rte.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp:rte] function job: generate rte for memory access
[wp:rte] function job: generate rte for division by zero
[wp:rte] function job: generate rte for signed overflow
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle
index b8d50097f75d58ded23f025ff8962702cc2147a4..6d174fd9f0f15990c40b726e345b56112384a719 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Nat)' [...]
[kernel] Parsing tests/wp_plugin/rte.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp:rte] function job: missing rte for memory access
[wp:rte] function job: missing rte for division by zero
[wp:rte] function job: missing rte for signed overflow
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle
index b4f10b265197441ab9ed7eba8f949324d76cf0a5..0a3228cc97c8794d2bbea41005d478b4e47111ca 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte -wp-model 'Typed (Nat)' [...]
[kernel] Parsing tests/wp_plugin/rte.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: -wp-rte can annotate memory access because -rte-mem is not set
[wp:rte] function job: generate rte for division by zero
[wp:rte] function job: generate rte for signed overflow
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
index c42d51cfe76b8525c86496365e5960a04d766a7c..fdfb80b6c398acb479a2221181fa65057e0b48bf 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
[kernel] Parsing tests/wp_plugin/sep.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f1_none
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
index 897f3be73baecb92a0425a1729eb6b8671598dfb..62b9c9001fa65dc0a6ae6d537f6b888a6043b3b8 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
[kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function loops
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle
index 9b3f58137ab19c66fa595e002fc86b4c5e998843..124de2a508dcfec3122dac00f791189e6a0e4d25 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] [CFG] Goal f_exits : Valid (Unreachable)
[wp] [CFG] Goal g_exits : Valid (Unreachable)
[wp] [CFG] Goal g_assigns : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
index 42a767b4657d31d0c2611266d24a15f4b230a1b1..aa233aaddc79ff44a7e2d47e4989bc411e4ac984 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/string_c.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
Goal Post-condition 'copied_contents' in 'memcpy':
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/struct.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/struct.res.oracle
index bd7e4d2e01d5c9d3d0a7d5334b50cfc886d483fa..b0a83c5583c91e74870bd714cbed93b9b98d107a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/struct.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/struct.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/struct.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/subset.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/subset.res.oracle
index 29cc3bb629733ce01d9585801f991c7d1035b558..31e97c1709501c89d62e193d7ca7071c1b030434 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/subset.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/subset.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/subset.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function mem
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle
index d18122a712f8e78a6502ae1f5bcb0f239208985d..fde06aafdfce56ba5edb411f57ea36f78d4cec28 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/subset_fopen.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/subset_fopen.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle
index beb2d13df622002818e1d3fd6020647182c3160f..6cad2d7458db74974f8f50369941a9117d488574 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/trig.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function foo
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
index 45858c34dea99fd999b7895364f420838278f42c..60291308af6ae635ff1c00dd98d81a973bf7cae4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/unfold_assigns.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function ASSIGN_NO_UNFOLD_KO
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
index ab37e2fb1b55d3d83eb32d7489ddfed5c22c2ef7..f681ec0f92309c15f8c0dc760963fec77f356d88 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/unfold_assigns.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function ASSIGN_NO_UNFOLD_KO
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
index 05fc31fd1c18b2deac8ba6a94f1586ae0218dd75..6dc9e4477f0be20ab5a90cccc8fdb9b063f53698 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/unroll.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/unroll.i:20: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.0.res.oracle
index 77915655ed3f715c679a25dded7de594d39c9008..0d6d70086ee9080222b0f1646488290e39cbfea4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/unsafe-arrays.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.1.res.oracle
index 24ef4545877e56ab19cc0aefcc5469f7506c5886..d68704a19a61005ff259a3e364ed8c797c75a84c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unsafe-arrays.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/unsafe-arrays.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/unsafe-arrays.i:13: User Error:
Invalid infinite range (shiftfield_F1_f p_0)+(..)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
index 8f8e6a453d9cb4d2e03ce0fdbad93c78c450de4d..8f0c8d4ce8a3ca974c104502d4572ad66bf635a6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job_assigns
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
index 129e94d6af2a3561d291ac217db596b83db08246..8f7b2282f202b7a6ab2c4fb7f9faa450a8594c32 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-no-volatile [...]
[kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/volatile.i:15: Warning:
unsafe volatile access to (term) l-value
diff --git a/src/plugins/wp/tests/wp_store/oracle/array.res.oracle b/src/plugins/wp/tests/wp_store/oracle/array.res.oracle
index 70648cc14cdc8c290289caa867c7ec2bbb738ae8..cf476ad115dcb52548e6b69484c218d9305aab60 100644
--- a/src/plugins/wp/tests/wp_store/oracle/array.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle/array.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_store/array.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function g
diff --git a/src/plugins/wp/tests/wp_store/oracle/natural.res.oracle b/src/plugins/wp/tests/wp_store/oracle/natural.res.oracle
index 3f1d57dc0cb1b878483dbab1ee516abd86930c8b..fc4518d506c71444b4bb382c2a55129ab0718b35 100644
--- a/src/plugins/wp/tests/wp_store/oracle/natural.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle/natural.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_store/natural.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle b/src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle
index d98e119512c223fbd86aaec2fd70e3056e798b97..0850a3c16edfbe868b78b028cfbd5ed0857e2137 100644
--- a/src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_store/nonaliasing.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle b/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle
index 5b15a883bf957c1ab05e2a58869516dac0766312..175f393e79efeb2cd0264d214300239688680d5a 100644
--- a/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_store/struct.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
index e6de0501d53a2b2f1a10599ec0affcfe32491e76..1cb5b23e556d9e985e712eca70660864d7d9e896 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_tip/chunk_printing.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function main
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_tip/oracle/tac_split_quantifiers.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/tac_split_quantifiers.res.oracle
index 31f7225f21a5627b2d54c7d44bec4ec3c44c15f5..a43b8e6759f42e9e7daabf709612bb09a148cb92 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/tac_split_quantifiers.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/tac_split_quantifiers.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_tip/tac_split_quantifiers.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function split
diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
index b461930a19aa459d0662ae84c9cd12d3f9b39050..6911b7211955e6ec8512f8a04d6ade0cbc60baae 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_typed/array_initialized.c:13: Warning:
Too many initializers for array g
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main1
diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
index a4351662142b509704e9b463ffa67a88ac831c3c..91c35e494c27dfb6e16519f1d684da5651aa073c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_typed/array_initialized.c:13: Warning:
Too many initializers for array g
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main1
diff --git a/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle
index 2aff985d9a40767d203ee47244258205fc5b949f..fd7ab0c35a657ff5ba6547c8b6a7f35acc4f0b05 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/avar.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp_typed/avar.i:4: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle
index 42142a26a799c0867aea47745ca9bb82d722190b..79830d2882daec567a83127aace0e428d09a4f14 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/avar.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp_typed/avar.i:4: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle/bug_9.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/bug_9.0.res.oracle
index 6955c7e9f335dc943c0b34ee75a4f9c977e73bef..78f07a377734982e94506b88e77fcb910794fef7 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/bug_9.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/bug_9.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/bug_9.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_typed/oracle/bug_9.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/bug_9.1.res.oracle
index d1a9c2edc88afab1780b170df6f210b29c2a459d..4b6dba37d8e627e797ca1951231df79da442eb8f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/bug_9.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/bug_9.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/bug_9.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
index 5de789f115cfba370b3934f5956180e03715b223..175f532ae7f266fc4435711706f0ba8423e25574 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/cast_fits.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_typed/cast_fits.i:13: Warning:
Cast with incompatible pointers types (source: __anonstruct_L2_2*)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
index 965f27bfd7d18e284692ac2d1aa47c1f9c980ea0..0db2247f414f8cc14620db7ea3c67cd24eba1594 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/cast_fits.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_typed/cast_fits.i:13: Warning:
Cast with incompatible pointers types (source: __anonstruct_L2_2*)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
index 1e91b9fe01bb8adc7ee48b04cd3545dfdf445224..ff1c02a4ba546326c78ca6b5c1bc43955534ced6 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/frame.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function compound
diff --git a/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
index 3cc68cc1beffef594728925049e0ea006134bb47..93b726016189c4ba2b68bacb30ae8ca2fddfcbd2 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/frame.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function compound
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
index 573cc01ba43d17f65607f14cae279f5e60061c93..c00b06312b62e50529b76e36b62185d8eeb09d9b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/mvar.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp_typed/mvar.i:14: Warning:
No code nor implicit assigns clause for function Write, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
index a4c11cbaf131aee41f5bd8d0b1e71a2d790d259f..fef31f965305408e602c2e3191f7fea8c84510e2 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/mvar.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp_typed/mvar.i:14: Warning:
No code nor implicit assigns clause for function Write, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle
index 9fea0aa32cc281b4a02601332ac2c163c9881497..4d36bdaa42ccdc53dd00de1d58d254528811f40f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/shift_lemma.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle
index 4a80ee7c1bedda2b60a821b3a4c77e6726bbed6d..4b06e83a95830e9b28587ead79f408a849417783 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/shift_lemma.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
index 1de296f9e9a5e7d2f57b95348450d7176eb00eed..5fcad89c14121824e5887d46d04dad71d38806bb 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/struct_array_type.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
---------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
index dc5985c4828c9882061431a06104de87c484cfd6..d2e3f2a9cd72abe8c290a08496c943a44251a532 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_alloc.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
index 3716b8fceb32bf2565e3b264e65a2550bc1cc8f0..115e7900443a3b47594946cdc03820b159258291 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/unit_alloc.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
index c73cb0f2080f590d229a037fdd20c46ad134e7b5..6bddd899e5d968db9988a8569ae23c1ecafcadfd 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_bitwise.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Global
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
index 8db4499af6806ad9b746669a46546d33ca023c3e..2b7c8292fd54200b551baba35eb0363df4096b14 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_call.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp_typed/unit_call.i:7: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
index 4d1955acf5164fb3f870e5352cb5103777330203..2fe4a4489865ce4a2bff1a42a3ea9d3fda75232e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/unit_call.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp_typed/unit_call.i:7: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle
index dfda7aa3f9a879aec4c378acbacc3faaa83f8ec5..280d1b5db6a8a50fb4bec3c575ffe2945408c13c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_cast.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_typed/unit_cast.i:4: Warning:
Cast with incompatible pointers types (source: sint32*) (target: sint8*)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle
index bb48de46dd639db6c134a314aeb6dff50675b4b9..84e952f60190a0894e1608f693524f8f221ef31b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/unit_cast.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_typed/unit_cast.i:4: Warning:
Cast with incompatible pointers types (source: sint32*) (target: sint8*)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_cst.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_cst.0.res.oracle
index c96410cf87b70cf9838c74b65a07c0f87724d117..f220848799ec78a5c6a29168d305db2f7347e0f8 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_cst.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_cst.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_cst.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_cst.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_cst.1.res.oracle
index 2dc8392a426d484ab6a52db69c1b399087a9c7d0..ac27acaa0ddda8702954a63f3a1de2a28765810c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_cst.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_cst.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/unit_cst.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_float.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_float.res.oracle
index bb4bf9336170c2c82945560d731b1e437dd835dd..157f2dd9361584760669482fd204b616304881e9 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_float.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_float.res.oracle
@@ -4,7 +4,6 @@
Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle
index 8dee3ca102c5e09c71768a6a6bcb62f33b98ae52..8c6dba5f1eb0f760cf13f4f9033e52ea88b62c73 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_hard.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle
index 92ab010a2b72171180ade7aa0a8728fad75fc586..dc71a1a475c539600e6c24eedb48fab7b55c26b2 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/unit_hard.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.0.res.oracle
index 7388a4baf8038dd5763d2490d070e18f3ee240fd..508a664970f6135939d4b6e100f817a5ddf071d8 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_ite.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function check
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle
index 43877a403428fbd5a0e8f4b71f516edf1102e3aa..c0eec98834070f47edced3f7b7288673ae2a08bc 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_ite.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/unit_ite.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function check
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.0.res.oracle
index c1c14a0c6470b457e4acd28cafa21e1281d98c23..f610bd6ab0f9f4e7c9c591aca024d38bdafe0449 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_labels.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function duplet
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
index e11c326de6046af69f226191e7c644dcfe7c39d3..98b60be4d4acc85fc0c73725a7e1ca124159ed51 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/unit_labels.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function duplet
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.0.res.oracle
index 6be54b4bb0957640bab00f4e5403d2427b542ef8..7c21a18a61a696a9dd81a12baedef66041010c81 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_lemma.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Global
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.1.res.oracle
index e3fed83ab4c5249d91d6d8ff9994264b282ebf57..8d72724d212dfebee9921b23f9a8f5d4a74ca81e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_lemma.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/unit_lemma.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Global
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_local.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_local.0.res.oracle
index e81bad545d076c6fb587da7846856a050e5be47d..b79c6356f022c4b300687766ac2961b7bf048ea1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_local.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_local.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_local.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function bar
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_local.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_local.1.res.oracle
index ca652b49c38ec3d95c0e7c50b854e457574442ae..f756360a105429747f220bf7b75df3e8d637a435 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_local.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_local.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Raw)' [...]
[kernel] Parsing tests/wp_typed/unit_local.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function bar
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.0.res.oracle
index 3ef9cfde40405fdc904df5294e5c88e50756f2e4..5a1fdea5b33712a284f6c810143b991192fc0640 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_loopscope.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_typed/unit_loopscope.i:14: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle
index 62ec7355781e8b95e3a43a8d9f9c5a6bf5c14416..9cd81cf810713b1a3524c268452769cbb34bcf1c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_loopscope.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/unit_loopscope.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_typed/unit_loopscope.i:14: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle
index b744d1ea2ded3c291eba6d3aeae6cc1455a3e0da..f3cb015dea5def8ab6a430cab921475060bcfab5 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_matrix.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function make
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle
index 8a07fab05017a844ede2f8130e13da5bb3a67e37..c0f6bc8b083b00abd8b760766313095961da71ff 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/unit_matrix.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function make
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_string.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_string.0.res.oracle
index e131924404aa5101bd6ddc8ebbe5104e19530c33..09bf183361456eb884755b6f672fa5ed3444d56a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_string.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_string.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_string.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_string.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_string.1.res.oracle
index b129820adfb64f78fd855d6a6ea0de6257dca5e4..33e37139a199e32a66d72f8398733bafe8f88bce 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_string.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_string.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/unit_string.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle
index 9d00a4ee69ac21812c65aafdb9ff2004341c50de..fd636bbb09f5ba89b5108a7ce87a4e990a7a5b87 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/unit_tset.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function complex
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle
index 68e873a5b9f611b6b0f31db383bae2a11ea00536..7af88b3ded647e1a034133916ef6f2aa0e9e03c0 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/unit_tset.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function complex
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
index 056fdd1bee8306e0ff4705859d8a47b00b93ccb0..4e4f0bbf55a16a97adedf3c2357f132c3e3b91f2 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/user_bitwise.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function rl1
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.1.res.oracle
index 90e88cdc057bf70998b27791e828239a3c92f6f4..8bb1f805315dbb8cf84ccfee810bfc0b1843b2f2 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.1.res.oracle
@@ -1,6 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/user_bitwise.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] No proof obligations
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
index 6d48fd7458959b16b42f491c3d96de5430bcf2cd..08ed2413253191c6d0e05590fbf877cfbd7cdf0b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/user_collect.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function caller
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
index b5584066b9c0b50d900d56a88a69db04ebd2d0cf..af4d14ff9c3f55f1a8c354b4777b3e80817a9bec 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/user_collect.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function caller
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 6b9c8bf453da08220491e819d59107dc5086c126..57d9150a815562d82288549a231d7a4054e0c40c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] [CFG] Goal init_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index df4678a075211d21332f83a6794872de14c25899..2b7c224c04f509bfa2365292aedb2e50f4dc976a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] [CFG] Goal init_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle
index 01aafec9e3066d2298b52509e34f6821d41e5392..b49ad5f8dddc52f47a74259da71cc92795e32b34 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/user_injector.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle
index 46d05c94af57bfcc2afd20cb9ef2a1c31051db65..3df342a583be2d88bfd6665c0468e1a40becb410 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/user_rec.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Global
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle
index e8561738bcd6641cdd98021ce41a451ef9366891..14d0ebde9e942251adc93092bccf56baacc99dfe 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/user_rec.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Global
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle
index 758429573e32d2523927750a36cebd84cf13d7fb..f6ac9a650aea8ed15b1ca16eb05f2209f1930beb 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/user_string.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function strlen
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle
index d99aaaf937e73f39368935427477e925ff1a4818..b0256f00b0c4d77b72ad77ee1e2fd7ab3bb14df3 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/user_string.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function strlen
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle
index 1bb42be2636e30dee886ed48cfec3afe4d592828..ed045c6b7826dd899433716233552a553451921a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/user_swap.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
index 14d31113393f8816ae5b331d75b3d956ff740101..abbc64b85dacff64fa8d779ed0d10ab167bc9959 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/user_swap.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function main
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle
index 218d938c66f64884fdc40885b3e6ef021d92727e..3e32676531171339c4abaa8fc6cc16846c252ecc 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_usage/caveat.i:41: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function explicit
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
index bf777e68401c99ed8446d62431e6325dc8d653ac..b4a9f732ab57d81a13ed8b594f0a2c991ce7980e 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
@@ -11,7 +11,6 @@ Function implicit: { a *r p q }
Function explicit: { a *r p q }
Function observer: { a *r p q }
.................................................
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function explicit
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
index bb429c2780e818d4258f6d962ba75c908c0cf143..c4439057d741e22283cc74f24ba42ade076657f5 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
[kernel] Parsing tests/wp_usage/caveat2.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_usage/caveat2.i:22: Warning: Undefined array-size (sint32[])
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
index 200b214f0ccfe0b3cc9a7e5f43a23baa60d71afa..d15c7f73b49722c9b671268208fb84518250c69e 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
[kernel] Parsing tests/wp_usage/caveat_range.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function reset
diff --git a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
index a812acef1d1948e7e3a67f01b09fdb1b9b3dd2a8..253cb2dea90b13cb88c0b0167a7ba38061fe0693 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
@@ -39,7 +39,6 @@ Function calling_spec:
Function cup:
{ val *ref &addr array[] &addr_value val_ref array_ref[] value_array }
.................................................
-[wp] Loading driver 'share/wp.driver'
[wp] [CFG] Goal by_addr_in_code_annotation_requires : Valid (Unreachable)
[wp] [CFG] Goal by_reference_in_code_annotation_no_exit_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle
index b17b67ed8d683d0f1b95b1f4f70708b3f546dac0..4d1ca598e10b8a792fe8628a767944ef2c5f2477 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_usage/core.i:11: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_usage/core.i:24: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle
index 68fa444153836b8e1e3dcc5c31e55ab07d584fb4..337bce578f76fa1cfe3acb42bcecbd05b790507f 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_usage/core.i:11: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_usage/core.i:24: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle
index 4535eb5a1311ead4b8eddb9afb7875566b7fb828..6bb95463d0ee683c1a109b51e4217f2d70d8a482 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Raw)' [...]
[kernel] Parsing tests/wp_usage/global.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function foo
diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle
index 504e20e6bd6202c3bf8cfb5b05d9ee181c31efb3..0243fc9b1786ecd5d354be89f6212db6e707dc29 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/global.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed' [...]
[kernel] Parsing tests/wp_usage/global.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function foo
diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
index 4e060164a41b0c55d214b73b0ec8c7410eb0c6be..6d03c92ee56c2b284a167e6eb2a17091cf840e08 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_usage/global.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function foo
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle
index c089fb5d1fb06deefe5d4e7ab48e56ea4e0cd0ed..2ed983d3f5f127812a72052978820e43f8fc87ae 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_usage/issue-189-bis.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function memcpy_alias_vars
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
index bcd929e7df7322951c973426a3b068a4063d1873..71a2cdaccb60d2b018b7d2eaa18b5ce4cbc57b8c 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_usage/issue-189-bis.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
Goal Post-condition 'memcpy,ok' in 'memcpy_context_vars':
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189.0.res.oracle
index b4b1200e289821553a629e8f91d16aca25d4e142..4751ddf0b3fcf7f3884aaab3c3f154dbb485cf11 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189.0.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_usage/issue-189.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle
index 5e33a1a8de186123c1dcd3b9c71a72a600263d41..4b1378e938499df2a55c817f8db964445ad42230 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle
@@ -7,7 +7,6 @@
Init: { }
Function f: { *ptr src idx }
.................................................
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_usage/issue-189.i:17: Warning:
forbidden write to variable 'src' considered in an isolated context.
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
index 557f81f473c853f5b4cca4c3df2c77aa113ed96f..0b9c5b7d7e604f10f869d9801c20aba6bed6f7ea 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
@@ -7,7 +7,6 @@
Init: { }
Function f: { *ptr src idx }
.................................................
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle
index 45812dbfaba6534cad25c4b6c9da7f8e7d899e83..1328bbed17febcccd1e69b411df3b394601a1664 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle
@@ -15,6 +15,5 @@ Function declared_equals_x: { x p }
Function defined_equals_x: { x p }
Function recursive_usage: { x y b }
.................................................
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] No proof obligations
diff --git a/src/plugins/wp/tests/wp_usage/oracle/save_load.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/save_load.1.res.oracle
index b335b1e24b1103980e749a710f5bfe71d08d4190..d951b156c9db55025e7330956907cb6ac58d599d 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/save_load.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/save_load.1.res.oracle
@@ -1,6 +1,5 @@
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Function f
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_usage/oracle/save_load.sav.res b/src/plugins/wp/tests/wp_usage/oracle/save_load.sav.res
index 565f6392f5a79b923d1594b58879f692af9a8c59..5271ccf0c21234ee97e3b1d72c5c6138629e2f50 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/save_load.sav.res
+++ b/src/plugins/wp/tests/wp_usage/oracle/save_load.sav.res
@@ -1,6 +1,5 @@
[kernel] Parsing tests/wp_usage/save_load.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function f
diff --git a/src/plugins/wp/tests/wp_usage/oracle/valinit.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/valinit.res.oracle
index e7916ad165955c8d41bfb2cd9194a9069f4227cc..d35aef5194bd805fad29893e022944be6393fb76 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/valinit.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/valinit.res.oracle
@@ -9,6 +9,5 @@ Function f:
{ &ly0 lz0 lx1 &ly1 lz1 lq0 lq1 lp1 &la0 la1 ls0 &lv0 lw0 ls1 ls2 ls3 ls4 ls5
ls6 }
.................................................
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] No proof obligations
diff --git a/tests/misc/version.i b/tests/misc/version.i
index 3a762af550b5fb818f962ec7d88d225747f95e50..2b739ebbd83e2b125fd1e0c738864c54c1df21c7 100644
--- a/tests/misc/version.i
+++ b/tests/misc/version.i
@@ -1,4 +1,4 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -no-autoload-plugins
*/