diff --git a/src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle
index 783f051c009e91c40916a4857448372bc694ba58..0f4c53717a141099c6061c88405bc8945dfb5abd 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/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
[wp] 15 goals scheduled
[wp] [Qed] Goal typed_loop_continue_loop_invariant_preserved : Valid
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle
index 7d5f6951348e86bcefdbef72c44612958994fcc2..946892056883cd25919365593b66425129f5abe8 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/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
[wp] [Alt-Ergo] Goal typed_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
index 6c7bce3b389f8a2b7860baa692789814b6bffcd3..c396c4f4d7b63c91166e35804f8f51354e78de20 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/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_qualif/stmtcompiler_test_rela.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle
index 6b7b63c6d937a80b5c18ef93eeb31910d5426c6e..85e1744ce2042bb31ce0c09fb458e8a778278825 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/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
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_empty_assert : Valid
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
index 83812560087c4aa860f4631b1c3afc3c5c801d95..8fb43bd64b1b3aa4b102d3b4fac41559d491f382 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-timeout 1 [...]
[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_qualif/wp_behav.1.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
index 70bb96ddf2477029c86956d4cd69eae07efe382c..5d374947a3c5b1bd0c93ca6bebb380b8d10df724 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[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_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
index f27ec49d1b76b21fa56b659de40a911b560d62f2..2da6874c320d29930e5aad1b37fdab14f1728ce8 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[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
[kernel] tests/wp/wp_call_pre.c:53: Warning:
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle
index b91abd82765fc05e5e7fbe118aed7a4198bf2490..11c277d30e4c47bef5d923f654725aeda0399f00 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/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] [Alt-Ergo] Goal typed_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
index 505785f5e07cc548e827cb8fe06964b64567298f..e630f56e9a5a7ace83a2ecb62aec2d7cd30a65fc 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
@@ -9,7 +9,6 @@
[rte] annotating function spec_if_cond
[rte] annotating function spec_if_not_cond
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] 25 goals scheduled
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko1 : Unsuccess
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko2 : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle
index 54afe789f7401e45161e0acdb40d9ba1b26c41e2..7f14ed8bcd3e729b54b79658add3bb4d944a617f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.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
[wp] 24 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ASSOC_land_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle
index 8164480855d10ab65821a833fe4a2e948355e0b0..414816fbfb37797ae157187361886b952bf51dda 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[kernel] Parsing tests/wp_acsl/arith.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_cast_sgn_usgn_ensures_qed_ko_KO : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle
index 5ec6a5228a3cd7e392da615936157e928f9ccf0a..09587f786aa777e3aa09854a3f2c8dc5fc94ac13 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_jobA_assigns_exit : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
index b2c5f9a9db3f18275eb72bff62e0519326fb2767..4179df2cf6fd8edcbcb8ca036938c5d3cd3e4b56 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 42 goals scheduled
[wp] [Alt-Ergo] Goal typed_array_check_CHECK : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
index 45f96059729f403bf623e724e9e3b002964abac5..bca9df7601cd35aae9305795c5b5cf4bff74949d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 22 goals scheduled
[wp] [Alt-Ergo] Goal typed_array_check_CHECK : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memtyped.res.oracle
index da65ee4ddd2bfffa0a8b410458696f43d072bb8a..f95259fd6149cb787685439b165c8a3120456651 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 9 goals scheduled
[wp] [Alt-Ergo] Goal typed_array_check_FAIL : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memvar.res.oracle
index d43006f651cbab443155805de39a03a2ad7b042d..f7b59bf049bd1f27aaa6c3f7477e04b92b54476d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_array_check_FAIL : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
index a2e6ef5f8fb10702b95b325bc38065fbed816b49..180d946c3170c9be3b7dfdaa9a4df4820f951158 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_job_ensures_N : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle
index 12d57a19994c19e1752f5f0e499f6270d2970d22..3cbb5dfd2f11d8fd8feb15bf5e57bb40c917e3a8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.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
[wp] 17 goals scheduled
[wp] [Qed] Goal typed_call_assigns_all_assigns_exit_part1 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle
index d1cface46cfd4030462b77ed7885c624776d5ed8..18f62e7ca9b9d00fabe5574939745779e8c99cec 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[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
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_call_assigns_t1_assigns_exit : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle
index 2f3e2cbcff8f30f4f441ef12eee791c834f2ace6..f2b749cff0c1d4178cd95a5bb4e17051664932a8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 10 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_P_todo : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
index 365c8b069cab811184cebb19b0cf514909a33d35..a8fdef13518b119b2286cdcee6d108108ea227e0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
index fe9cf947ab420526afde486234dc6a35235c00c0..be66e97ea6ad2bddd1fb2fb3b937e6c0951c441f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 29 goals scheduled
[wp] [Qed] Goal typed_band_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle
index 722cd23bada5690be0e1e98def00b5986f6da59d..df621b7dc0c486eb9d2d42f2c6941751c8cd9653 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 5 goals scheduled
[wp] [Qed] Goal typed_job1_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle
index c366fd7097fd7ee890f69f1d2627ce9ecc6d726b..41e658859356999332ae7131da7c0504d1a344c0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 10 goals scheduled
[wp] [Qed] Goal typed_f_ensures_Pt : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/boolean.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/boolean.res.oracle
index 9df0dc2a56038df5b6357bcc942089b311adeb89..339f025ca519ea7f68aef813cc884a842def83ae 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/boolean.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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] [Alt-Ergo] Goal typed_u8_is_continue_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
index b4d2560332c3367fd94cbf59b7e677e8be87dd0a..76d4cc6f9ddb98747bf335c3dd82f12c1ec50b75 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 5 [...]
[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_check_c1 : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
index 992ef461134cea13948c5dedbddc13f9a9586ca7..48e98d4fa14c783c2f68c1b0a33ea97593912457 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 39 goals scheduled
[wp] [Alt-Ergo] Goal typed_function_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
index c503421c8a958092c2d9bd7e08643dac8c075331..01ceab39f726f162ae53c9bbc5f7d7be11fc1cef 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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] Warning: native support for coq is deprecated, use tip instead
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle
index 80fb3297716e38d68086c61059ada03e9d6381c9..9d414c889b3bb3207f9ce5869c66bbaa0c70e18f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.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'
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_InfN_not_finite : Valid
[wp] [Alt-Ergo] Goal typed_lemma_InfP_not_finite : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
index bef955a1d640a7e2b4ab9af3633501ca1b5301ee..e49465837218c5419ceae5e14c75d99ed2b0babf 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.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'
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
[wp] 3 goals scheduled
[wp] [Alt-Ergo (native)] Goal typed_lemma_InfN_not_finite : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
index f0c942664c189643200669817d97a9b96cd651f0..4da1cb298a6881cbb3a8943597b4f8ecdad3de68 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.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'
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 3 goals scheduled
[wp] [Coq] Goal typed_lemma_InfN_not_finite : Saved script
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle
index b6583d3f4c6a466b4fb40a446ac02a1f289ffa84..6f5af142a49b2d515937796f08d2fb2f3d51e1fe 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Real)' [...]
[kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_real_lemma_InfN_not_finite : Valid
[wp] [Qed] Goal typed_real_lemma_InfP_not_finite : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
index 979b8b88f24de686b3269c1c829b0bf3c69cf033..9ecfe8363f1cdff07c5577f231aed7513c9adf00 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/cnf.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 43 goals scheduled
[wp:cnf] CNF=P_A /\ P_A1 /\ P_A2
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle
index e9fd5565a05fff14d503d81b5214be2d05e00dbb..8aa8444599fedd28182aef2628080b91ad06681a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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'
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_lemma_cons : Valid
[wp] [Qed] Goal typed_lemma_diff : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle
index 711ee91f78a6c24e79eb927a9efda21d173c0324..94777d12beffa59d8b5b76ed6f77bc2e4b7fb764 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.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
[wp] 22 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_d0_div_pos_pos : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
index 711ee91f78a6c24e79eb927a9efda21d173c0324..94777d12beffa59d8b5b76ed6f77bc2e4b7fb764 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.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
[wp] 22 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_d0_div_pos_pos : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
index b798c16bdb6bc2b59169d585e06bf09ab3a7b7d3..65c66c6e2b9d8eb7cfe6f226277d15564e207144 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[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
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_d7_div_0_x_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
index 7718ca4b67d4ec3eb13fac67b914fe1b9201dacd..1f2b15cef67cb8058051884f76366f81771e4800 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 42 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_p0 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle
index da11be9212d4d290de284dbfa46cf79f3d630faf..da0936200fd220b116561c80332d57bcd091f63b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_simple_array_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle
index cb949a9f9545c5163da4efda55c2ac57205e9b0b..484d3489bb0e59e2bcdad1acd13dd15d78276e1b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.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
[wp] 19 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_finite_32_64 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle
index 08e524f9e5ad5fc53f396d2a7df478d33f6e2778..37aaf32ef37285871060a657e05dc53df980ec39 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Real)' [...]
[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
[wp] 19 goals scheduled
[wp] [Qed] Goal typed_real_lemma_finite_32_64 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle
index bc8717807fd0d5bfde96f27734717207d76c39db..a5148398dc49ac2d163ebf312c3891f6f01807ec 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle
@@ -4,7 +4,6 @@
Floating-point constant 0.1f is not represented exactly. Will use 0x1.99999a0000000p-4.
(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
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_double_convertible_check : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle
index d5aaa7c1240344acd52290366c4a370cf83c6c69..538b5fb67c2e328febca6d2fbe935d934dde6b0c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.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
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_ref_f_loop_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
index 4b3a0044393faa02a60d3f95120b5a17991d3a11..f34b9052819a59cc9fbaf75fec6c23f9b8379308 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-timeout 1 [...]
[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
[wp] 17 goals scheduled
[wp] [Alt-Ergo] Goal typed_check_lemma_C_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle
index 39d383ddb17868508b08b0c47a490d79c50ecacc..1d332c3eba2f75eb4907e0cfbeff3a314b09d366 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_bar_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
index 222fe3b90403ab5186f4c3212dc8a1808a4ef491..880080271e2c5cd391bb557894a1b906aef43a6b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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_qualif/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
index 1fc7282684fabcb88b04bd94e84983e2209e1941..b396aef3b543d85d0aaf92e4d9d7cb596dbc7be0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[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
[wp] 24 goals scheduled
[wp] [Qed] Goal typed_fa1_ensures_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
index b790e8063540490ffa7c7565dc919b0fae209af7..853a40b3b238555f8881d827cd75486cd7fbec92 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[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
[wp] 18 goals scheduled
[wp] [Alt-Ergo] Goal typed_fa1_ensures_qed_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle
index d53071687811c413fbd4f51ff936bcebb02460eb..3cf52a8c9857dd1125d0a39b33d93223c0bbccbd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.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
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_ensures_P : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
index 53fe740ee7bb040a142f98f1af9bc780f40f16a8..11647c01b3df9fbfe42ee0f3c1b6ba4a787cb00b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 28 goals scheduled
[wp] [Alt-Ergo] Goal typed_formal_assert_provable : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
index ea40fb15e882b9468480b994c6da3818d571bd08..fa2acc12292c85ee69c240a5795f611dfc93f72f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 54 goals scheduled
[wp] [Qed] Goal typed_globals_check_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle
index cf80df81df28ed71dbfd6179d39a6c80d6e9e836..8bf8b806834460be113b2e184c35831f88f0e3ad 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_bug_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle
index 600fdf9a79bf6be04ab2a6f2959a82199c5e350f..e4c9550dc034c193d936035c2d76d20a7b552be6 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 19 goals scheduled
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle
index 43a22d025e26733246823853ffd6f34479980aec..f71b1ba16e121a7d7ceb9e0f4a0461b6aa8aaf37 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.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
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_g_assert_qed_ok_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle
index 6481802874a5ee384f099fc9cff435e5d6c1c4b4..fa9e50b10c43a4e1a1fd30d2be9088b20fe2faf4 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_assert_qed_ko_oracle_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
index 4f622671cdd1a80fe80834e171d582f737a8eb23..7c60acbc6bc552e898b693a4c1dff4beba722107 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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_qualif/looplabels.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle
index 492eb9634e02a5de82d75e9f75556fa0a65dfa1b..c7494eb3cc7153f07bca64930c983b2c19743d6c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_copy_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle
index c1a5e39bed0436f4bc7f0b7dda00ddf3f3d3b62e..1f8e9e4734906168f09d6bb3896f221f95211933 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_valid_non_null : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
index e84a81d12463b0848c3ced81c696018af2e7c9ea..b078d29e16536e7b77f3c3bab70fe92865f4a775 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[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_qualif/pointer.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
index 89712b41fe44ba795beedd5c8ff74aada4bbd6ae..a902f3f43d88764dfdbbdf7b2001e00d89aa7d43 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.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_qualif/post_result.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle
index e45ff82098c22fb28f57acffc6f86cc9fcbec1ce..d2eb8110c9572bed694b5fc19c23611c22e92687 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[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
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_correct_assert_OK : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle
index ecfa8fc993b3a8ac1a995dd25bf4cebcab0d226c..b27efefadcdec02581efc8bc21738d88dca0b834 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.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
[wp] 52 goals scheduled
[wp] [Qed] Goal typed_bitwise_ensures_r_precedence_and_xor : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle
index 614ab5823135cfbd7a55bd7fd46986e759545d50..16f68c44ff1103550d1ef4717329ba069b96c1e1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.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
[wp] 37 goals scheduled
[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_l_precedence_xor_and : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle
index c6b10dca91fe2ad85c93d5e62e1fe17319d85ced..4d389265cd8cfe3e45d227c229e032c109d86e81 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_test_ensures_P1_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle
index 6444362e5e27c13a024bd8614eb9f008aa06e9d6..9befe574b90fbf4b38a3b69e13fbd0b75468134c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.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
[wp] 7 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle
index 4d228ae7143e4d240f29aafffcfc7618adf7083e..11234264105999b92326127758f4ef34bfb4efbc 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[kernel] Parsing tests/wp_acsl/reads.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_modifies_x_ensures_qed_ko_G_KO : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle
index be665b9cca19398eac29db96cd1c29d149437d9b..aafa831a5d6a86746fef022bccf843e81e16bd6e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.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
[wp] 11 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_M1_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle
index 6cf9ed0803c41b4a71a709be66ec53f1bd7a8465..9ee1634559a2f85d09871a1b2067cc62165789fc 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[kernel] Parsing tests/wp_acsl/record.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_KP5_qed_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
index 2f04de9548a29027bb99c38b83bda1f2218378e7..7db00e97afe6aebfc022b51f22d7aebc7a7e823e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 18 goals scheduled
[wp] [Alt-Ergo] Goal typed_check_acsl_check_ok_C1_absurd_is_cint : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle
index 1e3debd836303f7253d635f15b49a21a346a7900..5eebd01bb772c8c769aad75003426bde3ce45e22 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert_A : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle
index bc32b522fd6c20392a5e46e940e61fd69be127bd..3b8c905ab63c750db0beaea8c971bb48aa3f7200 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.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
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_caveat_f_ensures_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle
index 692720f957a3fb4851d401a52fdd8a418ace2058..f43f461d6c19f94662e891f022c78bad8b526551 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Caveat)' -wp-steps 50 [...]
[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
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_caveat_f_ensures_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle
index 6277a80bafac2040ddbd17a73a3d67febdf2117e..bad7bc16a7c6f386454f91feeaed9372c22b7c5b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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'
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_lemma_UNION_DESCR : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle
index 9b59b6bac5cbeb58aacf9c1ba5e82a9e06cd990f..d891a56629221496f7672b2df57900c1cf543c29 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle
index 986a53101347925a5f3f8d6be7f833570067dfbe..6cd53f6a5bbe80f3012e01a633118bcdac18a013 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle
index f4ce0c5e62321a946f91d8dfa1999a086dfe835b..d886facd8a83386e139679b749c597720893203f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_rotate_left_ensures_bit_zero : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle
index ebd003d69d448bf8f2ea836a8c0a326bd170b200..6d9d902295debff8da4f9c576a73dc4a62c9c02e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/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
[wp] 15 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_f_1 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle
index 3eb172046e582d56554da52046ce258384ca862f..022b0364fa9ee3d9b289bfb3c241136c2e77bb6b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle
index a9b8d3dfbf95ac0b271f92b83355c0e69c91a841..0368f3b6126af38d9c7dc865d96336e7677090bd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle
index 665ff4aed3b2d3bde5d07b65bebea1e0975c4908..2dd56ced0525d32c285202bcaa24340617a20c2c 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_A : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
index af4c7b91ddde82f67ceb766112f5d614d75692ff..fbd210f679cb91ec29196a1b2f0e5f4b01f8f764 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_f3_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
index c5515d3585a14c0612808fb0a41e166a3140ef24..7f1e9b6e40fe2f7f02428d4290e889a9fc0c5d1b 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_bts/bts779.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function f
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_assert : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle
index 81c8416d16fa9cc15b002e06f197ea2b90cb992f..07263eaba248a77e6041f55a890d6f20ca8d897a 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_ref_main_ensures_I0 : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle
index 03a9507ea8164f81b9a8754bf234bfdf23c7df0a..8d3d1c250bfcf2ce2a168b360d6dd34898d11e1f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[kernel] Parsing tests/wp_bts/bts986.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_assert_A : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle
index 5a020f66ee15f500ca4b306d8c19558a61fbe81f..2cdd4e30969e83cd3bcbaaaa19602507ea67c65f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Real)' [...]
[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
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle
index abcda8d369d768828e71481a8ba74ed4b21686fc..e3b5535c1cb8a5f5e3557c9a4fe0ef85b2566b19 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[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
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_f_assert_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
index bf325fc4ff10e2061af50113485fc79a7b5b41a7..3472cd3cdfd26d8ad9265ed4e98207fe7a0e12fb 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 10 goals scheduled
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle
index 84c5b56ed462a1d9dd9ebb007fc6ac74b2987c6d..0b3c861aaa90fba8d43eb45dc097a8c531e129a4 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 13 goals scheduled
[wp] [Qed] Goal typed_local_loop_invariant_preserved : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle
index 8f62c5605c854c1e152b2bf68e57a954a670b56a..5d88cb99d2cc007af88b732ec74b9808ac99452b 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_compute_bizarre_Bizarre_ensures_TRANS : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle
index 5d175d94ffb0c144848044e01ea79e7d07726b41..4b070090eaa9f81b91cddfdb7c1827c22dcce062 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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_qualif/bts_1601.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle
index 7efb8386c5fb64310ffdde108116eadb36aaa950..86708cc7d79dc64c967451ea2382b2cc185d3eb5 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
index ebe06ce52f4bf7f8adad0f4454e1b0f5ca738179..31ff857069fd4bcad307a94feb4622cc816f18de 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_global_frame_ensures_sep_iff_ref : Unsuccess
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
index 7e368e5770ac7fb351fc4e57df579e1e7f809cc6..efbd5c95df37d1cf94c26e4381967f45fba7dfa3 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_ref_global_frame_ensures_sep_iff_ref : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle
index 058efe3f4e9bbaa5cc8e2b915c0e488596667b08..c47673e6b51df770410f04e7619b358ecea293f0 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_call_assert : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle
index bfcb01c492df22e9d7a750db82d299ee4de2515c..6f837f71940fa5aaa41c56c688dcd642832c139f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_main_ensures_Eval_P : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle
index afb849952b4a2ce73cc71497cf071e0b709ae5a6..c02dc9c178f3388a2f3c6212d3f540aabdb1a1db 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_job_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle
index 75f2f1ffe2071220b336af525af0ee88edf4bf51..99642408d02d9bb3678f5267181dfb4e16a0d6bd 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-timeout 1 [...]
[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
index 332bc081e7b4a91d0a25fc9745a7707148d7e385..ffb3913bc3829c2336a99250827f72c490e1ca85 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-timeout 1 [...]
[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
[wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
index 50cddea1b703876cc9d4b83bc02a9f43f0eca368..daef8736024e638253e9724c9732a577d90cb7df 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle
index 7c15d302575a2787a8d5b4fcfbc5b1f35d9a26fd..abf5b9692634744f0f1b390c33f4920e344ebc89 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 8 goals scheduled
[wp] [Qed] Goal typed_f_ensures_var_divded : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle
index 6fda3dfb53cdbe4d142f181cfcd95bde55934ad6..ea1d384da71ead051acf621bac6241aa441336bc 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_ZERO : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
index e1937ad2d564359816d4d03bcc49474a3b53ab07..be5d63c71f629ebf2cfc190d1532174e3f93b970 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_inconditional_exit_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle
index 485a5ed91f445fec2802b93aed25a1818a448a18..0f948292e59cef95e400626256c08b717ae197ff 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
index 0e57e63b9d92096579de23fb61f4ecdc47a27feb..c34591c0821fb4509b9c2ee41523e1306b521817 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_143.i (no 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] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle
index 485a5ed91f445fec2802b93aed25a1818a448a18..0f948292e59cef95e400626256c08b717ae197ff 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
index a4f2f3787a6ec3253bd62a7b86092493fc73a35f..c4d6c3bd19213d9856ba2a9860cd15d6f0370988 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_143.i (no 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] [Coq] Goal typed_lemma_ok_because_inconsistent : Default tactic
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle
index 6ab759c07bb389275ba7929463d7845c9067f1c5..19ffd064dfc2f54284c5d1c1ba830da766e51f95 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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'
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_broken : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
index d5e25e1edd51b8fae4459cf3e5683a831767202b..df5e033c97cf32024c587ccc4efe29ecd824e07b 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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'
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_foo : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle
index c23bd61bb48e42e8db14f2a7fa52829d737daaf5..c4d33cc9b69a9af5442f34759db1c02b3fd3aa32 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_f1_loop_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle
index b4c5c4f42866f939a7acfe6c1e19579c55c53d0a..437f33f00c3f348ac81f2cec3c4520c286180eae 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle
index 72ff7aaa1bdf490a9bfff9ae776ff4ffafb7aabb..f5c735d0395f2270a0b38e8c52423f4688eea914 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_add_assigns_part1 : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_711.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_711.res.oracle
index ebb6855f35d74c7a9195b5d5f9d6618841d84fa9..87633b0ea70e4a4143717cec91bbe1ceba92e119 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_711.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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'
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_A : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
index ed8d24a253a4e71985d065afaebccfcdc9098daf..2ab4a1454a9c1cf87dce7dc02bf19b648ae792ad 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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_qualif/issue_715_b.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
index 9f9bc155c5feeb1c347aec5a7d8c9c5c32cd9a73..694a10a84e816776f16530112304a39f25cb8716 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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_qualif/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
index 300d4c7ea1fe2d07d1a4a810572949bf17b21c8d..6fc62ce363bb63402e570f6ae0c8ab870bee5c61 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 40 goals scheduled
[wp] [Alt-Ergo] Goal typed_acquire_loop_invariant_RANGE_preserved : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle
index 338d948dadce37b4611ab359bb52de36e190c59e..455278246bd518ab7843f951f86963da8d6c9ae1 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_LoopCurrent_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle
index 9486ece4eccbf935e4da4957d98eb7d28619cef9..30935254772c056f74fa6ec471beff51f1e79d08 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_getMax_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
index 35895046c313f3c5b9afccb4df714ce09f77ecc0..cdf10ae70906c92f74e87debe17d04066af1e9c6 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_issue_check_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
index 1e55e4e4da4d50a375b1d5045388b3b665121725..c8ec6fc55f27e36a0907309c57a6d9ed3f859773 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_bar_assigns_part1 : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_898.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_898.res.oracle
index 7d9049804fb645d575944e4ce403903b3c3e6b8c..9e1e9bcdbead3094f0f8b7672cd5ea7de62f534d 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_898.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_job_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
index 272e07b8fe6b7f3f20d9efa62f062148aa8fcb80..164271bc40ab026c97fa2a3ab4579fcb40c49bda 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/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] [CFG] Goal unreachable_smt_with_contract_assigns : Valid (Unreachable)
[wp] [CFG] Goal unreachable_smt_with_contract_exits_ok : Valid (Unreachable)
[wp] [CFG] Goal unreachable_smt_with_contract_ensures_ok : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
index 0c30eb6cf12b6ad09707403db775ab3eea05fc4f..41402c7b8c2aef45ecafd2238c6896a462d04be1 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/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] 16 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ax1_lack : Unsuccess
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
index 92bfb254ae46eca98320c3de32493e1daf5d5130..c0a3091f89c5126ccf596644dbedb9dedd65dfbc 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/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] 17 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ax4_ok : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
index c73a41611eb1f2a78315fc603a476714cb052c57..f6155b9473b6f4f2fa67d5dacc2925606237e04a 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_gallery/find.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 41 goals scheduled
[wp] [Qed] Goal typed_find_complete_found_not_found : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
index 6fc6f3615765398b4464cfd1bb1c76e601378d88..e6750a21946341e1d5c8c9e4a0fc333232e87ed0 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_gallery/frama_c_exo1_solved.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Alt-Ergo] Goal typed_exo1_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
index bd27fc933298b8c30d36296a12b78436c804e32e..5af041259b1ca49c25e5305942a19e77e7752bdb 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_gallery/frama_c_exo2_solved.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 22 goals scheduled
[wp] [Alt-Ergo] Goal typed_max_subarray_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
index 6d3d8657fd91d93a265b801bdd6626843ef2563e..ee4bb865187f340d0937eed1cc9350efbd917959 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -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'
[wp] Warning: Missing RTE guards
[wp] 34 goals scheduled
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
index 0eb2143d7b45f66de9307487e31b33bd0db7469a..e7d12e16b297109fd7270130ec0b7f3d698bed88 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -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'
[wp] Warning: Missing RTE guards
[wp] 35 goals scheduled
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_ensures_v1_good : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
index af7f5f6418ea9b26d2ac9e28f26e2506c2a0aaa8..c3667e36d84126bec70f0aebec2a7d430c082e85 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.simplified.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 26 goals scheduled
[wp] [Qed] Goal typed_pair_complete_has_pair_no_pair : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
index 8e5320587c9157e2971dc28f9078d3d860dbfd28..3d56522f9e5dc65bcc2d8f7be60673406c2e8e01 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_gallery/frama_c_hashtbl_solved.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 102 goals scheduled
[wp] [Alt-Ergo] Goal typed_add_complete_full_nominal : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle
index 206278a5b0a23cd6942e67585a952e8c0aaf3c30..bebcd6d2a228371bf8142435eb8b888055e488e1 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/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] 15 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_Lb : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
index 35b2ee5a8b5f4aae3f5fded642fc8ad138edb9ad..cb72f2b3ee00828b6b13eb90b39e180c157ff726 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/alias_assigns_hypotheses.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
[wp] 30 goals scheduled
[wp] [Qed] Goal typed_comprehension_alias_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle
index 056f3917be7886b84ea979f282a51f6e457c3a76..24386e88747eca7dbf7c3b4f5bd12f818c5d5a1e 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/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
[wp] 12 goals scheduled
[wp] [Qed] Goal typed_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
index 0d4681981ee83417394762d0437fc01738433cc2..447bc62e87dbc502341cba6d50f4ed406ce19fad 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/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
[wp] 12 goals scheduled
[wp] [Qed] Goal typed_ref_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
index 179a92599507e1a11c4c79687ba0b471c8ef2c52..54ef16384aa6e7917a8ea59934f1e802709848a1 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_hoare/dispatch_var.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 78 goals scheduled
[wp] [Qed] Goal typed_ref_array_in_struct_param_ensures_Pload2 : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
index f2b9868fd88e56ba518ff919dae5f869d6f55307..54fb25c926cda9d7c86936fdb3dc64067610e846 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/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
[wp] 34 goals scheduled
[wp] [Qed] Goal typed_ref_call_global_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
index d23ba332da0642c03ac334a848c66f419b8ef0ea..6601e9e2d00ee0d618d8ed8046f4859ba603748f 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/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
[wp] 34 goals scheduled
[wp] [Qed] Goal typed_ref_call_global_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle
index dcf9b471da8aeb29ffed257e2a9288a50048c45c..04d5a4f2629e07014d67d846237693ab7173469d 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/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
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_ref_cmp_invalid_addr_as_int_ensures_ok : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle
index cd7e781214bef23a9c3d082a914160a6d2aa1999..efe1f7fdd1764a4ad45bbfb19fcdcd8323071f27 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_job_ensures_PTR : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle
index d2264fc7e594395b5aaf858d4dc2c24fb18c410f..1c127a17545a9535c8a1e6cecf08379654f649e9 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/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
[wp] 5 goals scheduled
[wp] [Qed] Goal typed_ref_fvrange_n_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle
index 44f733dcecfead44d7ced192fa7dd8d0f7e8460d..061f51954cab858b515c5e3320d909ba303ed652 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_hoare/logicref_simple.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
[wp] [Alt-Ergo] Goal typed_ref_fsimple_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
index e4be92ac66b9066968792697b0dbc7a0ae389d0a..009b3d2962514d6403f57a102d082206f7a0bb15 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/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
[wp] 23 goals scheduled
[wp] [Qed] Goal typed_ref_call_f2_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
index 757cef883b0f374d7c06ff29cc2aa21ac6efc954..e29464dd5553cb3b620485ad15435ce831bdad74 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/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
[wp] 32 goals scheduled
[wp] [Qed] Goal typed_ref_call_array_in_struct_param_ensures_Pload2 : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
index edfb3c339c7e85f6144acb1cb4b7bc67aee40920..2d2721f73017227cb40285453549226662009c09 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/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
[wp] 36 goals scheduled
[wp] [Alt-Ergo] Goal typed_ref_add_1_5_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle
index a53989661a59d05f01cb02906e4df9b7f55de9e3..b5390221da4d396ad6e3c0fdb1de95711c8dad3d 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_hoare/reference_array_simple.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_ref_call_f1_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
index beca524545cbe77d6cbb33b907b730d53176aab1..02a4bffe2c4d64132a21a44142ddcf9bf1b3f99f 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/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
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_ref_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle
index 676668f5c0a548d7a5163c8192bd30734112bb34..213ee06d29f83d84f773c31e96b4e084d01aa723 100644
--- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle
@@ -3,7 +3,6 @@
[kernel] Parsing tests/wp_manual/working_dir/swap.c (with preprocessing)
[kernel] Parsing tests/wp_manual/working_dir/swap1.h (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_swap_ensures_A : Valid
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle
index 7eeef9271651414998f73b1f345cec06219521f3..4f1030ab27018000d462c3def8e475fbbfc77d40 100644
--- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle
@@ -3,7 +3,6 @@
[kernel] Parsing tests/wp_manual/working_dir/swap.c (with preprocessing)
[kernel] Parsing tests/wp_manual/working_dir/swap2.h (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[rte] annotating function swap
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_swap_ensures_A : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
index 0a5c1608e7c642b2da40aa0a77192d68e4a61a96..fc8605283009333c1cc2ed29037b8ce30203b737 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/post_assigns.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function receive
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/post_valid.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/post_valid.res.oracle
index ebeea945b1a3dc5b1c48acf8b2a3d0c072a5f097..9848d7b4c8d5789b1bd7bc6dc08efa16612c0b68 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/post_valid.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/post_valid.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/post_valid.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_qualif/abs.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle
index 29ad79718d7c1dd66f2a8b8d1d436d85f1bf86ba..16adfa4946a202a912a9f1e69902616b1b347e1b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_abs_abs_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle
index 1065fc610ec6eae268e375b386487486ba1f1aea..3c71816dbbf88a9d7a7ab0c8471e5af0d0cc782f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.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
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
index 3a68e2ef5e192d127f43ecb6095b8fe05ed7426b..d5a8298ccca7d9cfe5363da017189ff878149463 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.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
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
[wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle
index 9548820aa57c3418c739327fe3d4bb8af36260c5..344e6b078479a4d7fdc25ab603de7bec24424f63 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_main_assert_OK : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle
index f6a082b42cc33bbd5b6ac2c421762b4aea213966..fef95834e2e117d45fffb152ca684dc76202a36b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_bit_test_check1_ensures_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle
index 3d4c24ffb4a1281d54bbf887af8f711de7b79796..d23de5bf36c08ebb9d0caf73240db5bb164d5d3b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 7 goals scheduled
[wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle
index 0f454d8c9dc6153468057651322ce1b0a6ea1469..c58a574b23eb0ec75c989e921af89d71396dd902 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.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'
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ceil : Valid
[wp] [Alt-Ergo] Goal typed_lemma_floor : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
index 451f9a657698b78e17984621caeef40ab1c6c1ce..e920dbe12565b8c038bde60962d817e0c4b4a18f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.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'
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
[wp] 2 goals scheduled
[wp] [Alt-Ergo (native)] Goal typed_lemma_ceil : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle
index 8c4637944dbf66e70083b0f2ca6d91317ba60f37..097475c27feafea1e41d76ecac880a822f1df06e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 11 goals scheduled
[wp] [Alt-Ergo] Goal typed_copy_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
index a3d176c2b04ee980b4bf2cd926d98d1028fec38a..541ee8719f95fc7b63f2c9c6dfbcaa4d9ad3bd43 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.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
[wp] 7 goals scheduled
[wp] [Passed] Smoke-test typed_bar_wp_smoke_default_requires
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
index f11a3888e1dc6f587beb931fa8677fb11eb4758d..dfc863b89cdfe6e7648fedbe5d393fb95c5b2704 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 10 goals scheduled
[wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_loop_s2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.0.res.oracle
index 31663282840a94f1fb070f1b7ab275f6390fd1cd..0f1ab89f30e93e02d96f35b7782b3773bee6ce01 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/doomed_call.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Qed] Goal typed_f1_ok_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
index 3d349ae889761bc345e1e830e832772d04c61ccd..1ccce739712018e9b9453a8d2a8e1ee668904622 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/doomed_call.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 33 goals scheduled
[wp] [Passed] Smoke-test typed_call_exit_ok_wp_smoke_dead_call_s2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
index 51c6311db51f101a18e4018c350aa16d9998e2de..972512d6665bff2ccf87f9d61b6a0f53228d8088 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-split [...]
[kernel] Parsing tests/wp_plugin/doomed_call.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 36 goals scheduled
[wp] [Passed] Smoke-test typed_call_exit_ok_wp_smoke_dead_call_s2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
index 0b7ac571bbb5104117da2b1a5abd17b46c31fc15..b256a09e43c74003d6e3bc7a5b1c4f3abe89b236 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/doomed_dead.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 46 goals scheduled
[wp] [Passed] Smoke-test typed_f1_ok_wp_smoke_dead_code_s3
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
index b5c0258a177a6fd3979a13a3bd589bf4671bb599..0b4390c4e11c64231036c6c89c01b16fc65c1cdd 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-split [...]
[kernel] Parsing tests/wp_plugin/doomed_dead.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 48 goals scheduled
[wp] [Passed] Smoke-test typed_f1_ok_wp_smoke_dead_code_s3
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
index c1ea877c9baf297a06bc5012eb462963ac2e0561..6cbe64cf0f16c20eda7b2d0d71a9d00e58286748 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 8 goals scheduled
[wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_loop_s2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
index 9daa85dfb61bef09c36d23fdc45a15e24df9dfb8..4a65820f41cec1a70848725c4ebd2f33b3c24581 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/doomed_report_ko.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_loop_s2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
index 2b80ca79ba3e82219a7e914e785dea7f3c5e3610..c578928320d9953ffa47747f9d26dfaa40927d9f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/doomed_report_ok.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Passed] Smoke-test typed_foo_wp_smoke_dead_loop_s2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
index bcd42d15cb2eeff852f0551d2c583c32f4569787..9f20f169f87366f5aa10f1dd022d84d9c87629fe 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
index a0f09e08be3c8acf22540e19f8ea9cf9d7298c7b..2561d69246cd7d32640e47700c1b3e7660874f55 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/dynamic.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior
[wp] Warning: Missing RTE guards
[wp] 51 goals scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot b/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot
index adc97b189dd30ed107c620cded36762ba14ef83f..7c51f93dabee8afae76d1222d9c817b1053df9ab 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot
@@ -35,6 +35,7 @@ digraph f {
N100 [ color=green , label="Assume f_ensures_3" ] ;
N100 -> N099 ;
N101 [ color=red , label="Assigns f_assigns" ] ;
+ N101 -> N100 [ style=dotted ] ;
N102 [ label="" , shape=circle ] ;
N102 -> N101 ;
N102 -> N100 ;
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
index 4b005c11a31b2e9dbfab45e3ecebf574424538f2..c78a7cf65a38f32339cb534a45aaced02ad60dcf 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.0.0'
[wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle
index 219472265d9f7873bae6ecca18fc86ea6f27eba6..0d5f90a7526755a6d15610e4881c08abf7e0e1a5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-timeout 1 [...]
[kernel] Parsing tests/wp_plugin/flash.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_job_ensures_Events : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle
index 70adda9301671f9105136c51565e7e6a3af9f7cf..a01eeba9e85753bb3728a8b18e52179de2ff3f36 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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_qualif/flash.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle
index 847a02d9f75f5561d640415e507be62799b9e404..a87892007eea5a1214f99161ef4e1b9826bafe7d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_flash_job_ensures_Events : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
index beac21fa7b5ad7a5d2144f9eac99391570ce6afe..5ba66e74babbcfc208688d5a4e9b0989e089004b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.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
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
index fd00d9ebd5b3572c8a1acd500ba6df167dcf7384..0423017c2be17ac025fcf70e73491281b769971f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.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
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
[wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
index 5974584a73c3314ee7219f84e732d7bbe21260be..fcad25a085a2ccc51c4d9b3896c25c7fca9504f2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_output_ensures_KO : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle
index 96493d8e91a25c306aa1363426dc4155e4007edb..265dcf746300cd6547717198ab1ec49ae4e343e5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_real_dequal_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle
index 497f15c885f64541d1d18180a84fb4e2e658dea3..a42394bed4b944faad652b0f70e55d095ca69ae7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_dequal_ensures : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle
index 47c2b9e78e3107c3e32468219e46de76bc8cae23..fb7fe23261680138c94159f6ea04c9ac25f339e3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_alias_ensures_KO : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle
index 9a35ec5ad1c74a93c5bc6f68d35c8b7dbb0a0fdc..a875c26ce74f00b05ef3fded034d1de490509a9c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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'
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_R : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle
index 4c1700d30e3a246fcd6405fdad46b5f2dcea8453..6d7143512ed48ff7e046732495c4230c531fc48a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-timeout 240 [...]
[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] [Coq] Goal typed_lemma_offset : Saved script
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle
index cdc1cc3b7c5193f7139c2c959d34ccf09ff88ada..4389c814aec8df535f7d9bbd12b2b51036f6c7e6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_fA_ensures_KO : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle
index 21ceab5595dc8b8671c4c700d44d75a2b39f1914..2a606446dc508ff2c1ee4c64f75ce2f7a75e7097 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 7 goals scheduled
[wp] [Qed] Goal typed_f_ensures_Const : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle
index a998137dcc1af1438ca62c0353296865f0ee3117..bbc0f9b17382cdbafbeb6f5a9aa9279ce478c6dc 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_f_ensures_OK : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle
index 2ad8b7259698ff0772c2439f7309148ba0aba033..3f9234d02bd81a465147e9d05117667f9dfe9cbd 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_validA_assert_OK : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle
index 1654af3ba936a2a8b340f13e4970ebc01c3dcd89..1607fa2719344a9f53471ea5e443d5e3d319ea6d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_job_ensures_SEP : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
index af35f6b8507e96fce68044a83cac500c84814833..65ebd21fce6811c9b33ea504d9ae8136a7f6d9aa 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.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
[wp] 13 goals scheduled
[wp] [Qed] Goal typed_f_call_g_requires : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle
index 273409a9bcabf0ce12e0eb3e455a9d4c89714d40..8730d221d2969eca9b2a83336a5d944037f6874e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[kernel] Parsing tests/wp_plugin/injector.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ko_ensures_qed_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle
index 33f5a9859865d89af15b0b70727997753ba2d148..602235b4e1772332174a1428afa250766274b4de 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 9 goals scheduled
[wp] [Alt-Ergo] Goal typed_init_ensures_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle
index 60ddf9009c6893786a7ed8b4d15627fde5437c5e..75c868bd36ae05e9b8149506fe3d16a45176c363 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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_qualif/loopentry.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle
index 93b40345adbe00724c694ba553239dac785743b1..f62dda1b35eefa46aabdfd4180461127302e5bd7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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_qualif/loopextra.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle
index 32ed32900d4795e92adf0f51e067b0be4e80c7d0..111bb4a02c06d23a33d6407e49cf7337e132400d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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_qualif/mask.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle
index fab459f7a10eec2d4250a89b09651f7250977f6e..a212cb8779f94f82742d16dac4a0a92d846a3f36 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_compute_ensures_A : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.0.res.oracle
index 82888040205afdcb8ba0206e3b6007c7fb8925c4..4af858324c195a679739ad390d26d65cb4403141 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.0.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-timeout 100 -wp-steps 1500 [...]
[kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 30 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_abs_neg : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
index a3c9e94c53e0e0d69ef81c937eff0a97aad86f9e..40753d2a146f38c6a7492f72afbf13ab99e03d60 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-timeout 100 -wp-steps 1500 [...]
[kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
[wp] 30 goals scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
index 6dd9859b66923ba3291bb6433d7017c18ef0d153..ffc737646cc3751ece484585b3668b9546fa4a87 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
[kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_sin_asin : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
index 5b07b133292e5f331f03ec150346b916870de08f..81ba2360317d22e51aed43fc0ec3e3e828560c6f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
[kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
[wp] 9 goals scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
index 45defe11c252e1fdb22342768b34b459e48ce881..becab8e8f0695bc02585f6dfc232d1e84394aede 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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_qualif/nosession.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle
index 21dad7a45d6492664cfd7d5c8ecd4aed040ddadf..d56af67a5072ba45bb43314c4e3ca5658524abf1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/nosession.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Failed] Goal typed_f_ensures
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
index 28d3b1aac6194de68decb3aad592930d7d05c1d2..f11f92c390ec20461736d7afffab1019345708a9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
@@ -1,7 +1,6 @@
# 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] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
index f7ef9322a9954f7c26eddbf37d08b84cefee4354..1647eed4e12f9eec5d91b1c473c1899f1700a55d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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'
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_access_16_16_ok : Valid
[wp] [Alt-Ergo] Goal typed_lemma_access_4_4_ok : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle
index a78f9d23cc2c17a9cd6d0711871c8fb2a775b1eb..6daeab38c98f63ca1fdf216a7f789be8d86d92c5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 12 goals scheduled
[wp] [Qed] Goal typed_f1_ok_assigns_exit : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
index 5222a717ce69ab4c9583dd47bf8802e0cb09858c..5bfb2cf3e3404fc852f21bd6bce54e9d187991a5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 12 goals scheduled
[wp] [Qed] Goal typed_f1_ok_assigns_exit : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle
index 66f2e22013fdd80456a4ba59946ccd0f5b1d73f4..f5af22f701424ef220ab28a18bdebd44c36410d2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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'
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_lem : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle
index a8a6e9e1f363a439258d75c0e9940283db1d04dc..30017bf15b078ab2665348dee450cf16b66fde5e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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'
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_GOAL : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
index 0aace62366d2513ed6483844d03655afc05308b6..5f2225e888c8039688ad6f032109704023a8750c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/post_assigns.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
[wp] [Qed] Goal typed_receive_ensures : Valid
@@ -16,5 +15,9 @@
receive 5 - 5 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'receive':
- /*@ behavior typed: requires \separated(&size,message+(..)); */
+ /*@
+ behavior typed:
+ requires \separated(message + (..), &size);
+ requires \separated(message + (0 .. \at(size,Post)), &size);
+ */
void receive(int n, char *message);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_valid.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_valid.res.oracle
index 7452d12d8c6da0842e324a144b09e6e816139803..42883461442bf7cfe6e8ca58e5a3912baf397bed 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_valid.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/post_valid.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/post_valid.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_job_ensures_LOCAL : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle
index 522d782c44a4cdbf2521e37f0a221b09d177d3f4..dcaa1de220c10583f6f3ba7868cc1a14e86d7bea 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 12 goals scheduled
[wp] [Alt-Ergo] Goal typed_diag_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/region_to_coq.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/region_to_coq.res.oracle
index e9138f7b492a1b4692401846228aec556b99e6b1..90915c00cf2005f3e6fc62a0cb21910cb94531b2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/region_to_coq.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/region_to_coq.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/region_to_coq.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 4 goals scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
index b622a45a0f7a2daa0c28f30d33096e4fde0e5d6c..2580c0129be69f18f65f38d88a7180eeb7b2c4cb 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
@@ -12,7 +12,6 @@
[eva:final-states] Values at end of function main:
__retres ∈ [-2147483647..2147483647]
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_Eva_signed_overflow : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle
index 28ac3e50e6eb882bd71fa02d0ae891664acad61b..d2e67a0b560403806ef2cdcc386d535ab3da3e40 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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_qualif/rte.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
index 71c6b6ffc4b9973d35fa83da51dfb5a06aa3d003..b15eec1d8c0f3329246d434eb8f8f479d12f622e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.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'
[rte] annotating function job
[rte] annotating function job2
[rte] annotating function job3
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
index 64612393030a62a4f4e7b0dc92fcdfd20e0c8e48..2be801f58b0d34109b22d22ebdca6ac9d25d6ea4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.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
[wp] 39 goals scheduled
[wp] [Qed] Goal typed_caveat_loops_ensures_ok_first : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
index 8905c23c28d16382cc830f9f7616a7718869d0e6..ad0100e7a0de24b7fc5c49b1038180f283fa669e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.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
[wp] 34 goals scheduled
[wp] [Qed] Goal typed_caveat_loops_ensures_ok_first : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
index b58e86cce5e522462e5d2c639c8cc7b8bee0eb27..9f08e04867c88212456b5f19fc1a3f40e7ba00e8 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Caveat)' -wp-steps 50 [...]
[kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
index d9273f9a996b1e35e80c61643caab9f1c2a5a547..7bd29dc92c3ddefcccd049aa53e76f6482b79a4f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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_qualif/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
index 0c67db7db8712f0b13c7fbee20f2db940b1fae8e..e5ecf9b5e00d8593bc806889fba90904b71c6b37 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-timeout 120 -wp-steps 2500 [...]
[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
[wp] 44 goals scheduled
[wp] [Alt-Ergo] Goal typed_memcpy_ensures_copied_contents : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle
index 37e0be540b7f5b0a9689248b70d9c3840513c0b3..43fba563315355d7ca0addf14cea396b9273d25a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 18 goals scheduled
[wp] [Qed] Goal typed_f_ensures_qed_ok_E0 : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle
index f42dd19bc62938f7011f367998a9305ee490715a..15e36ca17c4b10d669412b57f0051f386e9cff61 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle
@@ -3,7 +3,6 @@
[kernel] tests/wp_plugin/struct_hack.i:46: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/struct_hack.i:37: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle
index 1330ec957e608d3a72c926aee310b26b97312b32..8fc2d073364afea561fc261a9a71f6f72fd199f7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_mem_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
index bc26d1ed0e5e1ba13b5e989e26d3429f275c549c..7f76d80b00a10d94eb30f412df38843d33541efa 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 5 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_assert_Ok_A : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
index a4bc55ce426f46f0f19a9c08a38a529ac8b438f4..59455952143a4d400e7a94030a7fa6c446b544ff 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_S : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
index e847532a8b0af675af2c134b0a994bf4df024999..1acc6c2f67194ac1cacb71df228693a3ff42ad02 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/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_qualif/unsafe-arrays.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle
index 2d2d4a2621c736e1c92541672122ef490fdb0170..6944a089a5680677ce9f2faad5a2eb6608eb7665 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.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] 3 goals scheduled
[wp] [Qed] Goal typed_f_ensures_ARRAYS : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
index 1901df8a161a2fe48d947ec5cbe3977a2e6292e2..4dc2d8b6cabcc2b77ac16615387e15dadd33c4a1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/unsigned.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] 1 goal scheduled
[wp] [Script] Goal typed_lemma_U32 : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle
index ed869315385b0a55a80d94923101c8f805babcce..1af004f7352a7399067955d2a6f532ea402593f8 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/array1.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle
index 5e7de78ee60a2f5aa14cc1f5e319aab15f01ab5e..8a08fc002341f92fc59c3e0bddc74b46aafb47dd 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/array2.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle
index d46d52bdc2ca803b21d3faac80876001c715fc68..1344cd80f93131f3b3ce5b68df14775600fe5537 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/array3.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle
index b732e6a34d538630c79489e85d1256b3a126eeb3..cfd2596b0591d1bc89e1a30cb9ac27a197a52ea2 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/array4.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle
index 31f6983483faa6a1cf748b59de00f228305d5855..96c8bb9496dc74752ccd83b438b8cca2cc8f27b2 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/array5.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle
index 34d7eb2a98234201feba0ed0c8ac99eb43f27da4..e9b4be282bb2067de102441f7f84bf1a301329ad 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/array6.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle
index 0e0ad91c1638620ed0195d7987d0fa01003e73c6..014de0bbb3a906df837b21bab34a69366d353f29 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/array7.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle
index 13c02c6b2d165dd77354201d006bda6425925a7f..c045da519b1923ff0250a10be65fbb19fbbc44e0 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/array8.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle
index 0db49291906bd53d4198f688cb412a1d48eceeab..524115e64b4234b212eba54058f71db95542f2a2 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/fb_ADD.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle
index 372e798b6738aa13ac1808713975884123dac150..98b5221f1755b87c0d3552511f029bb8513c6a74 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/fb_SORT.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle
index af0aea662d2da09f00b8ce7532b0d23648a6771c..7cae27dc0bb5db0195e3dd039165b5036b2f9f7a 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/garbled.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle
index fe16dc545ec4bc400ffb2f52a45392edb2555020..851c520b6845a0e1090004ed8a87e04e687e6a37 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/index.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle
index d0a1dcf567acd74de8f3d99a2045742ec76ea668..bd22d004dbbb42d74264f5af2f37df6819875f8b 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/matrix.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle
index 4f31df7dff83aa35c0fa9c26f3428671d4a1b5b5..f420eeb6427fdbb1ca7a7764ee519a756296b0dd 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/structarray1.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle
index 94c1cbf18655420babfe0f2e5252d44574767bc2..47409954b5b88eb0c499797658218f760eecf9b3 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/structarray2.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle
index 0cee2a2b63172d9a9266c3f665cb4bd8bd3a43b3..1acebc060c044889880df8bffb9b73e6e12e0e65 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/structarray3.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle
index 70c1d992d17e288ca98283f4f7413b93496b1c8c..ec6b5a2de86270e3dbfc5304c83ce5621c8909fe 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/structarray4.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
index 258e09a4a6956547a87e73fee12edb2644aaea3c..f736619caac65deed1a4955a8fe1996603c0dc18 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_region/swap.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle
index 910812b95aae44bd63450b0f0f35c88f63b2b4df..9373264bf9dc25047ecf3a7e64b41b779f82cf97 100644
--- a/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/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
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_g_ensures_P_startof_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle
index e2f8762967c52bf9b9e15b728769a49967976843..8d3b99ea68772209a97b649d3349178c3734ce6a 100644
--- a/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_f_ensures_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle
index fd22abbbb9a85bfa113cd5dde2cd32a335f5b3d9..139e0d95e804f6aca5a9002bd87a629369a385fe 100644
--- a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.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
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ok_P : Valid
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle
index bb918fb79e29cbbe4a96120f338047648ec3dea1..8d1a5b9cac94b62e3b028920bf61cd6897007e1a 100644
--- a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-steps 50 [...]
[kernel] Parsing tests/wp_store/nonaliasing.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko_P_oracle_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle
index 461e3fcaa6f0677b0acb619c9cd725a27f15423f..344ab6e6f744147c2bd03515ad9604f97d99258c 100644
--- a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/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
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_f_assert_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
index 0de1e59793298ec333db9346817d211d42e40c25..1fc22002b222f9cfabf273f5b1796664c486a825 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/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
[wp] 5 goals scheduled
[wp] [Script] Goal typed_split_ensures_Goal_Exist_Or : Unsuccess
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle
index e2a176a72f5066032526fbf01dc4b811772595c7..0d1a283b5f82294ce2f798f83ea9eee83fa89231 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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
[wp] 5 goals scheduled
[wp] [Alt-Ergo] Goal typed_main1_assert : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle
index e2a176a72f5066032526fbf01dc4b811772595c7..0d1a283b5f82294ce2f798f83ea9eee83fa89231 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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
[wp] 5 goals scheduled
[wp] [Alt-Ergo] Goal typed_main1_assert : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle
index a9b513c05f613b1e8641964319ce2b9cd82f6bfb..878e590dd1e091c3fe6db642952a77cdd1b9b449 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.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_qualif/cast_fits.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
index b720cb1e0e29341083e776e8f22e0f55ee769177..e706b784a7a92b81e6fa7c16a7982f020fccfbe3 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.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_qualif/frame.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
index 2c002e7b1b168ce19f4d7a8d13be19971ffa0196..dbc2330142860c450016dadd3afe2cd9f5c8a828 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.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
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_compound_assert_SEP : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
index 2d667089f84a3524ab94f99ca2f3b3d1e87825a4..65452ad8fe8dcf8a886ab9f392404f71630df81b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.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_qualif/shift_lemma.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle
index e8a80395ed36a95a70a975d148592102ba683b4e..b09f19d9e21cd1d22ac3a67730dd7a5b487d9c55 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.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
[wp] 5 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_assert : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle
index 7513018dcd915582fee84ed0c4e927b408e536d9..a7963a1a6f95d866ce43bb242984b73428ac54c3 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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
[wp] [Alt-Ergo] Goal typed_f_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle
index 5e5b91dc94a4fae2c602610b76ab88d741c057a3..e3689c507d2476957466d03da0a6f7c251718493 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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
[wp] 7 goals scheduled
[wp] [Qed] Goal typed_f_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle
index 97a099bc62cdf9c56dfa9a739f1f92911f633b74..14f99e8e67f5e8a79c38b8083d09af44b03a87f6 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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
[wp] 7 goals scheduled
[wp] [Qed] Goal typed_ref_f_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle
index 03bc287592f8a1a34f36c76e9dd23e90f8aefc9d..aa4dc3db0593a87b6409b0fdd1abc3e462965ba5 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.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
[wp] 61 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_band_sint8 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle
index 9c4dc9afa22a0bdcb51edec61b4ef6ad14c02b0c..1c174b6ad2ab0132d97ea5ed07c86ec4b24e7fbb 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.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
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_band_int_assert_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
index e39935873a6909a3522ca8fece74af0a4fcdd270..e2091a07708432017ec2a5599e677cb06cab0721 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.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_qualif/unit_cast.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle
index 8d8d1eff5fc7b853214e148d778b4fefd45f81c1..c54e6f55894426414495d56cd63c0fe1a8b2e3c1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.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_qualif/unit_cst.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle
index 70fa445d32bc7524e1013b4f2f8c23943f876e64..503a254a25f00fd9ae064719d864b8f608a8b112 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.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
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_f_ensures_A : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle
index 6b5ca009e8dae54cdf0091adf167288ae2600dcf..df568124db56b58ad7625bfc83e1d823c194dc6b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_main_ensures_CST_F : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle
index 00ea955fe66bb4fdcfaeda35930d84395eb85608..71e047a463e1457643a7bfa8f70f0aaef0f6c362 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.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
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_main_requires_p_is_33FF : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle
index 0bc63584c9b7b6f5e2db2591d0f8788eb066b47e..0fc85faf32b648767159621cd29f07da187565d4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.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
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_check_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle
index 802c3513d531b3752211fedb5dd7632ed0773f49..a255ecbfec34a8abcb606596793671d050dd77f4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.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
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_duplet_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle
index 6015427dddcbc8c7d4bf286aa356f9bcc4db8599..820a581c2e10442ce536c96ce2ecf012b3e76ebd 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.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'
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_P23_KO : Unsuccess
[wp] [Alt-Ergo] Goal typed_lemma_P52 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle
index ffa7b49597ef31892bf907ada32423335317d6ad..ab1c9992d7b13d591c01ef247c9393d6345c9906 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_bar_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle
index 86474c5e363a3ff5b28822f9bcdf98546dc8fc3e..131788981a35a7359070c4d0f9203f342fedf489 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_raw_bar_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle
index 3b196114d45fb2824e9a38d13d779ee8e7bb388e..80e267199ec95e38e3342d58984e767e822caed7 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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_qualif/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
index 7e327b11a789f998a2e487876f530db99f3c476a..4417ddd127acc3f894426f6829b8d8b4766afaf2 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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_qualif/unit_matrix.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle
index 94ce30099a1c7a44562028f3e44c935851aa9ca7..f48df3d43f601321a6b715fc4a9d10273b2107bc 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.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
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_make_ensures_OK1 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle
index 43b55a82a22fb99517433a8b3b1e08b52e536a98..85998f3551920e8f3c059c0b434c9865eb6f39d0 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.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
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_assert_AB : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle
index 756da0b5ce2eb69ccf60a71ae0bdb6475c088085..d82295e1dc51bd6fc34b5804a09dfaa7414c4659 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.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
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_complex_call_job_requires : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle
index a29035c5b07da1f5385f084ee7b05afcc9bda57a..c210a11f4cccf2b5c541a9928046681fd56eef9b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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
[wp] 12 goals scheduled
[wp] [Qed] Goal typed_ref_rl1_ensures_b0 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle
index ae33efb03cb7afe2119a6a3853eff1d475303779..803894a6a5d9c534aebcc30db5e4d8a0a09b6902 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.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
[wp] Warning: No goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
index ccc488ddf66ba0894de55fa1e125ee62d5df358a..5e4efa11a65af41c09fe5fb907fbb742af6879a2 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.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
[wp] 32 goals scheduled
[wp] [Qed] Goal typed_caller_ensures_K : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
index a3eb99d52425aa2e0bc0c57c0f46a4793004a0ca..0ba543bbd4f02751a8696043616c85eb8a81ad65 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
index 3a97274559283cd00d6f3e0ee43bc9a0bea53be0..757500ea677bef03e3f14f519399211fb0656b4a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.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_qualif/user_init.2.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
index 21d17e27f81061c3125263f7bd5eb704e588d172..ef421c4c8085f87a16384d2910243dfe788934ff 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.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_qualif/user_injector.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
index d75c812e6016ece281ac9bee3c866b51327a8d24..20fdb332cff1128c6e165033300ad73bfea348fc 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.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
[wp] 20 goals scheduled
[wp] [Qed] Goal typed_job_ensures_SEQ : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
index 90efeb24fce244e7b1ee0f3737bd04c7b52db2cb..93b4fb88899dc8766046ac491738f5ce0f679df6 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
@@ -1,7 +1,6 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[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
[wp] 16 goals scheduled
[wp] [Qed] Goal typed_ref_job_ensures_SEQ : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle
index fdc05455b8d85a43d87f1cf9ca2c169e587af022..16e16726067efbf2c05555f8174b25a438697575 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.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
[wp] 18 goals scheduled
[wp] [Alt-Ergo] Goal typed_F1_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle
index 3b813077d9b1e91220984926ea680f4bb31d9149..48d205c0e686833aab93bed4760f2e6b2b96399a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.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
[wp] 13 goals scheduled
[wp] [Qed] Goal typed_strlen_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle
index dd19834fbb20e2b934e559200d0f6a0865845dd0..17290739f7cfe29999b4cff7f2bb7431b8646644 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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
[wp] 7 goals scheduled
[wp] [Qed] Goal typed_main_assert : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
index 8b1b07121dc4efe7aa92926dbdef60e5f0045f88..258b04e2719b1fa3a8f7cf6bae19c18e06cec255 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/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
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_ref_main_assert : Valid
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
index f8365548e57855815969a4bd76ad8f8ad873dac6..6c1a2b8821961dcbaf564314c55b39872a1ef6bc 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/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[])
[wp] 9 goals scheduled
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
index d985f8cbec7862bbf1d917c194ff5c9b438f2403..050004166a73ac6f66a23eadb0131b5b510a598c 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/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
[wp] 12 goals scheduled
[wp] [Alt-Ergo] Goal typed_caveat_reset_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle
index 1c5952f1a020e452ad9d284b3805e867d99a9321..1aa3a66475c495f732460268228af5de005e9a00 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/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
[wp] 30 goals scheduled
[wp] [Alt-Ergo] Goal typed_memcpy_alias_vars_ensures_memcpy : Valid
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
index 045de5e319baca32f2f7292da1d6006f318b52f0..c2679dccf0ddd1ca3dbebec9e4eb51a652063629 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/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
[wp] 10 goals scheduled
[wp] [Alt-Ergo] Goal typed_memcpy_context_vars_ensures_memcpy_ok : Valid