diff --git a/Makefile b/Makefile
index a001d3f0bc972c1d78583701114cc92e812740ea..dd01490e9a8fa14468e82ec499a12ca2f0bf5e61 100644
--- a/Makefile
+++ b/Makefile
@@ -182,7 +182,7 @@ TESTS=builtins callgraph cil constant_propagation dynamic float idct impact jcdb
# todo: adds aorai (2 configs + Aorai_test library)
# todo: no test found for studia ?
-# todo: adds wp (at least 2 configs)
+# todo: adds wp (config qualif)
PLUGIN_TESTS= dive instantiate loop_analysis markdown-report nonterm report server variadic wp
tests: config.sed
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 478b7b10b1e81104a4f763da28abe69b307cb34c..6883d9ff47b14241d62896e3a1b147d82aa80ba1 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,2 +1,3 @@
-CMD: @frama-c@ -wp -wp-par 1 -wp-share ../../../share -wp-msg-key shell -wp-report %{dep:../../qualif.report} -wp-session @PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
+PLUGIN: wp,rtegen
+CMD: @frama-c@ -wp -wp-par 1 -wp-share ../../../share -wp-msg-key shell -wp-report %{dep:../../qualif.report} -wp-session @PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay -wp-coq-timeout 120
OPT:
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 813798a56de622e0c795b05199b7ad14e250e025..4ad9b8f44006538bccb9b0979e47619f3786edfd 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp/cfg_loop.i (no preprocessing)
+[kernel] Parsing cfg_loop.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 15 goals scheduled
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 946892056883cd25919365593b66425129f5abe8..a074e6a554d0526106c6babaf00199c0a2e27f60 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle
@@ -1,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp/sharing.c (with preprocessing)
+[kernel] Parsing sharing.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 6e1e0c0d7c30baad20ca78800a4bacd2573751f7..a8d80dc000e5bda53fb10784403c102a359e3431 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
@@ -1,12 +1,12 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp/stmtcompiler_test.i (no preprocessing)
-[kernel] tests/wp/stmtcompiler_test.i:136: Warning:
+[kernel] Parsing stmtcompiler_test.i (no preprocessing)
+[kernel] stmtcompiler_test.i:136: Warning:
Body of function if_assert falls-through. Adding a return statement
[wp] Running WP plugin...
-[kernel] tests/wp/stmtcompiler_test.i:145: Warning:
+[kernel] 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
-[wp] tests/wp/stmtcompiler_test.i:81: Warning:
+[wp] stmtcompiler_test.i:81: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 27 goals scheduled
[wp] [Qed] Goal typed_empty_assert : Valid
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 85e1744ce2042bb31ce0c09fb458e8a778278825..4f68808ea91ad2345835bb3d2d0ff669c6740f8e 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp/stmtcompiler_test_rela.i (no preprocessing)
+[kernel] Parsing stmtcompiler_test_rela.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 faa679c96697f66156e01511131f9dc0cf867911..123cb832adaf6401a521714729a1279af3d54d2f 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,16 +1,16 @@
# frama-c -wp -wp-timeout 1 [...]
-[kernel] Parsing tests/wp/wp_behav.c (with preprocessing)
+[kernel] Parsing wp_behav.c (with preprocessing)
[wp] Running WP plugin...
-[wp] tests/wp/wp_behav.c:172: Warning:
+[wp] wp_behav.c:172: Warning:
Ignored specification 'for b1' (generalize to all behavior)
[wp] Warning: Missing RTE guards
-[wp] tests/wp/wp_behav.c:69: Warning:
+[wp] wp_behav.c:69: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp/wp_behav.c:81: Warning:
+[wp] wp_behav.c:81: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp/wp_behav.c:154: Warning:
+[wp] wp_behav.c:154: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp/wp_behav.c:176: Warning:
+[wp] wp_behav.c:176: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 38 goals scheduled
[wp] [Qed] Goal typed_f_ensures_qed_ok : Valid
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 5d374947a3c5b1bd0c93ca6bebb380b8d10df724..836c313e00d90fac1893bdd9c1eed58a13dceb77 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,10 +1,10 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp/wp_behav.c (with preprocessing)
+[kernel] Parsing wp_behav.c (with preprocessing)
[wp] Running WP plugin...
-[wp] tests/wp/wp_behav.c:172: Warning:
+[wp] wp_behav.c:172: Warning:
Ignored specification 'for b1' (generalize to all behavior)
[wp] Warning: Missing RTE guards
-[wp] tests/wp/wp_behav.c:69: Warning:
+[wp] wp_behav.c:69: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess
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 bad25e7802e2219b75ae036e67603294e2d6093e..d31f94ae8d4700ba131202a6ae4182a5482f0e7d 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,9 +1,9 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
+[kernel] Parsing wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
-[kernel] tests/wp/wp_call_pre.c:53: Warning:
+[kernel] 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:
+[kernel] wp_call_pre.c:53: Warning:
No code nor implicit assigns clause for function g, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
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 11c277d30e4c47bef5d923f654725aeda0399f00..e7aa87478b247bc40f94dc6f74e791962542c1b1 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp/wp_eqb.i (no preprocessing)
+[kernel] Parsing wp_eqb.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 90bb89816b2808947e23ae7a45f9a42897429a66..4ec3f9cebefe1412636c13f4f3adf36b15e2168a 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
@@ -1,5 +1,5 @@
# frama-c -wp -wp-model 'Hoare' [...]
-[kernel] Parsing tests/wp/wp_strategy.c (with preprocessing)
+[kernel] Parsing wp_strategy.c (with preprocessing)
[rte] annotating function bts0513
[rte] annotating function bts0513_bis
[rte] annotating function default_behaviors
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 7f14ed8bcd3e729b54b79658add3bb4d944a617f..6421bb6a22828470e479d8dd7c145274443ac35c 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/arith.i (no preprocessing)
+[kernel] Parsing arith.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 24 goals scheduled
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 414816fbfb37797ae157187361886b952bf51dda..ccc1c83ed99a3b580dc057912ad8b90d703aafbe 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/arith.i (no preprocessing)
+[kernel] Parsing arith.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 09587f786aa777e3aa09854a3f2c8dc5fc94ac13..e7fabb1851d15e8cfb508e8029c1e8b48803b78e 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/assign_array.i (no preprocessing)
+[kernel] Parsing assign_array.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 660872093ac27a7d2ae67acedee77f2b66c6c471..29ca6a4c21b1de651eb30168e912c03ca60ff46f 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/assigned_initialized_memtyped.i (no preprocessing)
+[kernel] Parsing assigned_initialized_memtyped.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 42 goals scheduled
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 bdd6cac2653343ae848ca9b820fc69dc15e8fdd7..9c9d392ccecf2f325ea4374995072d43f1469412 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,5 +1,5 @@
# frama-c -wp -wp-timeout 20 [...]
-[kernel] Parsing tests/wp_acsl/assigned_initialized_memvar.i (no preprocessing)
+[kernel] Parsing assigned_initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 22 goals scheduled
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 183c0c59b683a4e8f1257724c2d6ea67dbd8ef8a..4b34e4e7ebcb7efc0ac26e3c7dbdb8bcf9ab681a 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/assigned_not_initialized_memtyped.i (no preprocessing)
+[kernel] Parsing assigned_not_initialized_memtyped.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
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 e5a1208fc8f44c52782c44786da7d621138f1091..b7400e96ca7ba7e7217c02594773c5a933d0fb07 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/assigned_not_initialized_memvar.i (no preprocessing)
+[kernel] Parsing assigned_not_initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 180d946c3170c9be3b7dfdaa9a4df4820f951158..6ff8f9301d1d85b27ce41eb4b805330ad34a3ace 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/assigns_path.i (no preprocessing)
+[kernel] Parsing assigns_path.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
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 3cbb5dfd2f11d8fd8feb15bf5e57bb40c917e3a8..be1fcea95acc03cf80739f72f39b5459b1f1b573 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing)
+[kernel] Parsing assigns_range.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 17 goals scheduled
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 18f62e7ca9b9d00fabe5574939745779e8c99cec..8e75f33c163bec81a97a521235e88802d6cb0fb0 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing)
+[kernel] Parsing assigns_range.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 f2b749cff0c1d4178cd95a5bb4e17051664932a8..2e6f0226f8a12472f706245ff3e3869ddbd0c56e 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/axioms.i (no preprocessing)
+[kernel] Parsing axioms.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
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 05b7c9c11f25194d55795c9aba8475fecd23d1f0..44e1c94ba9b445c2f5c0fd91ea61425b6f08e2ce 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/base_offset.i (no preprocessing)
+[kernel] Parsing base_offset.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
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 a91b7a0149b5b87b9fc08bf7b402236915adc151..2f2067dfc3acf32d666bfb4b7f35cec421e34555 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/bitwise.i (no preprocessing)
+[kernel] Parsing bitwise.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 29 goals scheduled
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 df621b7dc0c486eb9d2d42f2c6941751c8cd9653..dc9160a870fb9155dbadc859527ff67bf4b5e25a 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/bitwise2.i (no preprocessing)
+[kernel] Parsing bitwise2.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
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 41e658859356999332ae7131da7c0504d1a344c0..ea8709779a5e0bf15215a4d68c22354079d53c54 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/block_length.i (no preprocessing)
+[kernel] Parsing block_length.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
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 339f025ca519ea7f68aef813cc884a842def83ae..48e6e69aca4ed70a5692c9ecd53b1a3e494104d2 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/boolean.i (no preprocessing)
+[kernel] Parsing boolean.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 af1378e391d547f67fe53f59135d2195168a5767..7eda18784520c66d36ec7a399e0fddfff0c119e5 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,5 +1,5 @@
# frama-c -wp -wp-steps 5 [...]
-[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[kernel] Parsing checks.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 48e98d4fa14c783c2f68c1b0a33ea97593912457..43511c2b77fd5ae6a1d2ec621ca57cdc23409e04 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,5 +1,5 @@
# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/wp_acsl/chunk_typing.i (no preprocessing)
+[kernel] Parsing chunk_typing.i (no preprocessing)
[wp] Running WP plugin...
[rte] annotating function function
[wp] 39 goals scheduled
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 01ceab39f726f162ae53c9bbc5f7d7be11fc1cef..d076d76ed0ca7aae9c361b7cb65df1b03f11b9d5 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,5 +1,5 @@
# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/wp_acsl/chunk_typing_usable.i (no preprocessing)
+[kernel] Parsing chunk_typing_usable.i (no preprocessing)
[wp] Running WP plugin...
[rte] annotating function usable_axiom
[rte] annotating function usable_lemma
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 9d414c889b3bb3207f9ce5869c66bbaa0c70e18f..e5e152aa2a04ff1bede601bd2e3421a525454857 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
+[kernel] Parsing classify_float.c (with preprocessing)
[wp] Running WP plugin...
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_InfN_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 e49465837218c5419ceae5e14c75d99ed2b0babf..efbf0e0a5e995775beccb153f9ac586f1301faaf 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
+[kernel] Parsing classify_float.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
[wp] 3 goals scheduled
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 4da1cb298a6881cbb3a8943597b4f8ecdad3de68..8d89bf6103e89d700c551ea565d3cd4a814e3d35 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
+[kernel] Parsing classify_float.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 3 goals scheduled
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 6f5af142a49b2d515937796f08d2fb2f3d51e1fe..d56892bed73e2320f69ba98f7d23a947f7420d22 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Real)' [...]
-[kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
+[kernel] Parsing classify_float.c (with preprocessing)
[wp] Running WP plugin...
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_real_lemma_InfN_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 9ecfe8363f1cdff07c5577f231aed7513c9adf00..2631afd542b6b5197226f2607be8d02d1cc62924 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/cnf.i (no preprocessing)
+[kernel] Parsing cnf.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 43 goals scheduled
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 8aa8444599fedd28182aef2628080b91ad06681a..eaecc9714e5ef60cbfe904bd326123fe72286f06 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/ctor.i (no preprocessing)
+[kernel] Parsing ctor.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_lemma_cons : 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 94777d12beffa59d8b5b76ed6f77bc2e4b7fb764..8abf0f34df3833ccd8b45a7a4795c257e36caf79 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing)
+[kernel] Parsing div_mod.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 22 goals scheduled
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 94777d12beffa59d8b5b76ed6f77bc2e4b7fb764..8abf0f34df3833ccd8b45a7a4795c257e36caf79 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing)
+[kernel] Parsing div_mod.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 22 goals scheduled
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 65c66c6e2b9d8eb7cfe6f226277d15564e207144..e0f1fa19f1b2ca5add3cb07aec6d4d17418ee34f 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing)
+[kernel] Parsing div_mod.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 1f2b15cef67cb8058051884f76366f81771e4800..163a87864020a0982270857646d1c1ec28485f86 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/e_imply.i (no preprocessing)
+[kernel] Parsing e_imply.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 42 goals scheduled
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 950c758b70c5295e2c48394f5367085488c07c9f..bc4d3a27e1ab9472678c174bfe8de71c30aeb782 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/equal.i (no preprocessing)
+[kernel] Parsing equal.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 0bf8482694768045a032e0ddceb752fb2a1dac83..9ba561787d4363705f699a4bbf7d66904347b94d 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
+[kernel] Parsing float_compare.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 19 goals scheduled
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 27675ba0b6830fff79c02e047b5d86136f7f0eee..6d1b078148d214dda6191ef7305dd289612bf2cf 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Real)' [...]
-[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
+[kernel] Parsing float_compare.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 19 goals scheduled
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 ff8fe2744f860a45392f3658b1e2e6f238fb2b38..3362c14fd999c78b98c47fd0092ed312656a929e 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
@@ -1,6 +1,6 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/float_const.i (no preprocessing)
-[kernel:parser:decimal-float] tests/wp_acsl/float_const.i:10: Warning:
+[kernel] Parsing float_const.i (no preprocessing)
+[kernel:parser:decimal-float] float_const.i:10: Warning:
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...
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 538b5fb67c2e328febca6d2fbe935d934dde6b0c..232ed2e60fe4c4e062a926f5d54da01c8be2081e 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_acsl/funvar_inv.i (no preprocessing)
+[kernel] Parsing funvar_inv.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 ee38ba7972748686bc43809b5174f8930279ea0e..f4f1b7e3145348d3a8fc2b2439484bc2665911ef 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,5 +1,5 @@
# frama-c -wp -wp-timeout 1 [...]
-[kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
+[kernel] Parsing generalized_checks.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 17 goals scheduled
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 1d332c3eba2f75eb4907e0cfbeff3a314b09d366..7be552269882b567eb1a1ed89d37702f6bce538e 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/implicit_enum_cast.i (no preprocessing)
+[kernel] Parsing implicit_enum_cast.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
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 e48f553e2947fc9590f4931437b4a48767d92ff5..42a2712a517b8653a8eae106b9c7e3627cfef0a3 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,7 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/init_label.i (no preprocessing)
+[kernel] Parsing init_label.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] tests/wp_acsl/init_label.i:27: Warning:
+[kernel] 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
[wp] 4 goals scheduled
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 d6bc501d6c9ad682aa1542e85bb31d2df4ed5cf6..dfbed47d774fe1c59df24cc9401d9b1b73f2d8b5 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing)
+[kernel] Parsing init_value.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 24 goals scheduled
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 3d74eca2ac3488de79a65c2b32cf9e21149e3922..96e1fe244e48536ea968a1085f29dc49e93b6a47 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing)
+[kernel] Parsing init_value.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 18 goals scheduled
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 3cf52a8c9857dd1125d0a39b33d93223c0bbccbd..4d2e5f794dd90e24924c508cff7486d695bf3596 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/init_value_mem.i (no preprocessing)
+[kernel] Parsing init_value_mem.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 88684268b9cb445cdfdf9909b4e607ac18a0664f..34e09776f72a843757b71f7289eb5fbffb500180 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/initialized_memtyped.i (no preprocessing)
+[kernel] Parsing initialized_memtyped.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 28 goals scheduled
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 fa2acc12292c85ee69c240a5795f611dfc93f72f..ffb39abe02fbbeb4bc00411787388fdbbae6dd11 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/initialized_memvar.i (no preprocessing)
+[kernel] Parsing initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 54 goals scheduled
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 8bf8b806834460be113b2e184c35831f88f0e3ad..b1ebccde2482e665fc235ffeb0b66287da33fba4 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/intbool.i (no preprocessing)
+[kernel] Parsing intbool.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 089501d0a3a6713dce8e372db5c147a9a61e7bbb..3fd3eaad360bf9ca28836bc6a48972e311306a94 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,8 +1,8 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/invalid_pointer.c (with preprocessing)
+[kernel] Parsing invalid_pointer.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/invalid_pointer.c:21: Warning: void object
+[wp] invalid_pointer.c:21: Warning: void object
[wp] 19 goals scheduled
[wp] [Qed] Goal typed_memvar_check_M1 : Valid
[wp] [Qed] Goal typed_memvar_check_P0 : Valid
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 f71b1ba16e121a7d7ceb9e0f4a0461b6aa8aaf37..f4a753164c5e337581ce386628c9746960c44d6b 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/label_escape.i (no preprocessing)
+[kernel] Parsing label_escape.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 fa9e50b10c43a4e1a1fd30d2be9088b20fe2faf4..9ed64cb24ee4e9cebd1e7a99cd84d900152ee953 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/label_escape.i (no preprocessing)
+[kernel] Parsing label_escape.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 7c60acbc6bc552e898b693a4c1dff4beba722107..0fabb9c099152b4e092f96eb5bf0d1c504c7b96d 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,37 +1,37 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/logic.i (no preprocessing)
+[kernel] Parsing logic.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/logic.i:65: Warning:
+[wp] logic.i:65: Warning:
Cast with incompatible pointers types (source: __anonstruct_Buint_4*)
(target: uint32*)
-[wp] tests/wp_acsl/logic.i:49: Warning:
+[wp] logic.i:49: Warning:
Logic cast from struct (Tint2) not implemented yet
-[wp] tests/wp_acsl/logic.i:50: Warning:
+[wp] logic.i:50: Warning:
Logic cast from struct (Point) not implemented yet
-[wp] tests/wp_acsl/logic.i:51: Warning:
+[wp] logic.i:51: Warning:
Logic cast to struct (Point) from (int [2]) not implemented yet
-[wp] tests/wp_acsl/logic.i:52: Warning:
+[wp] logic.i:52: Warning:
Logic cast from struct (Point) not implemented yet
-[wp] tests/wp_acsl/logic.i:53: Warning:
+[wp] logic.i:53: Warning:
Logic cast from struct (Tint2) not implemented yet
-[wp] tests/wp_acsl/logic.i:54: Warning:
+[wp] logic.i:54: Warning:
Logic cast from struct (Buint) not implemented yet
-[wp] tests/wp_acsl/logic.i:55: Warning:
+[wp] logic.i:55: Warning:
Logic cast to struct (Buint) from (unsigned int) not implemented yet
-[wp] tests/wp_acsl/logic.i:56: Warning:
+[wp] logic.i:56: Warning:
Logic cast from struct (Tint6) not implemented yet
-[wp] tests/wp_acsl/logic.i:57: Warning:
+[wp] logic.i:57: Warning:
Logic cast to sized array (Triangle) from (int [6]) not implemented yet
-[wp] tests/wp_acsl/logic.i:58: Warning:
+[wp] logic.i:58: Warning:
Logic cast from struct (Tint6) not implemented yet
-[wp] tests/wp_acsl/logic.i:59: Warning:
+[wp] logic.i:59: Warning:
Logic cast from struct (Tint6) not implemented yet
-[wp] tests/wp_acsl/logic.i:60: Warning:
+[wp] logic.i:60: Warning:
Logic cast to sized array (int [2]) from (int [6]) not implemented yet
-[wp] tests/wp_acsl/logic.i:61: Warning:
+[wp] logic.i:61: Warning:
Logic cast from struct (Tint6) not implemented yet
-[wp] tests/wp_acsl/logic.i:62: Warning:
+[wp] logic.i:62: Warning:
Logic cast to struct (Tint2) from (int [6]) not implemented yet
[wp] 21 goals scheduled
[wp] [Alt-Ergo] Goal typed_h_ensures : Valid
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 c7494eb3cc7153f07bca64930c983b2c19743d6c..3c5f14b5586a8915b0302faf8a82f7b3a8d4adb5 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/looplabels.i (no preprocessing)
+[kernel] Parsing looplabels.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/memvar_chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/memvar_chunk_typing.res.oracle
index b6dab655323e029a174df65e0e9f50255dd4c94e..dc3afd8b0ce07f369430144e68badc8fc0fc7846 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/memvar_chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/memvar_chunk_typing.res.oracle
@@ -1,5 +1,5 @@
# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/wp_acsl/memvar_chunk_typing.i (no preprocessing)
+[kernel] Parsing memvar_chunk_typing.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_L : 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 1f8e9e4734906168f09d6bb3896f221f95211933..57936c31ef4ff21b2f5800f326d7b848adb6a753 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/null.c (with preprocessing)
+[kernel] Parsing null.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 9e0fd3122c659339481553df508465ea91fdba64..2e058d9e213b9fbb7f9a383b49cbd192d627a512 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,10 +1,10 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_acsl/pointer.i (no preprocessing)
+[kernel] Parsing pointer.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/pointer.i:50: Warning:
+[wp] pointer.i:50: Warning:
Uncomparable locations p_0 and mem:t.(0)
-[wp] tests/wp_acsl/pointer.i:49: Warning:
+[wp] pointer.i:49: Warning:
Uncomparable locations p_0 and mem:t.(0)
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_ref_array_ensures_Lt : Valid
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 5e0172dd87d30107441b9959cdf9c1f5460443b4..ac454864f98e4bfaae0ae87e2d0ded1f71f30a0f 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,10 +1,10 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/pointer.i (no preprocessing)
+[kernel] Parsing pointer.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/pointer.i:50: Warning:
+[wp] pointer.i:50: Warning:
Uncomparable locations p_0 and mem:t.(0)
-[wp] tests/wp_acsl/pointer.i:49: Warning:
+[wp] pointer.i:49: Warning:
Uncomparable locations p_0 and mem:t.(0)
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_array_ensures_Lt : Valid
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 d2eb8110c9572bed694b5fc19c23611c22e92687..0b383ccbb583d6ac42377fb950341f02d0d112cd 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/post_result.i (no preprocessing)
+[kernel] Parsing post_result.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 24278f6c3aaaaf689932142d4c270d79f18cc1a7..7fcb2ffab9dd9e54cbf13724180b80c5c625cfa6 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
@@ -1,40 +1,40 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/precedence.i (no preprocessing)
-[kernel:annot-error] tests/wp_acsl/precedence.i:90: Warning:
+[kernel] Parsing precedence.i (no preprocessing)
+[kernel:annot-error] precedence.i:90: Warning:
unexpected token ';'
-[kernel:annot-error] tests/wp_acsl/precedence.i:135: Warning:
+[kernel:annot-error] precedence.i:135: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:134: Warning:
+[kernel:annot-error] precedence.i:134: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:133: Warning:
+[kernel:annot-error] precedence.i:133: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:132: Warning:
+[kernel:annot-error] precedence.i:132: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:130: Warning:
+[kernel:annot-error] precedence.i:130: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:129: Warning:
+[kernel:annot-error] precedence.i:129: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:128: Warning:
+[kernel:annot-error] precedence.i:128: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:127: Warning:
+[kernel:annot-error] precedence.i:127: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:125: Warning:
+[kernel:annot-error] precedence.i:125: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:124: Warning:
+[kernel:annot-error] precedence.i:124: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:123: Warning:
+[kernel:annot-error] precedence.i:123: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:122: Warning:
+[kernel:annot-error] precedence.i:122: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:120: Warning:
+[kernel:annot-error] precedence.i:120: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:119: Warning:
+[kernel:annot-error] precedence.i:119: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:118: Warning:
+[kernel:annot-error] precedence.i:118: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:175: Warning:
+[kernel:annot-error] precedence.i:175: Warning:
R is not a logic variable. Ignoring code annotation
-[kernel:annot-error] tests/wp_acsl/precedence.i:176: Warning:
+[kernel:annot-error] precedence.i:176: Warning:
P is not a logic variable. Ignoring code annotation
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
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 1aa717f83fed226738c1ce9aaeaabf722f6e8206..d08db8de9fe6ddc3efa9ff9365897e40ce0ab081 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
@@ -1,40 +1,40 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/precedence.i (no preprocessing)
-[kernel:annot-error] tests/wp_acsl/precedence.i:90: Warning:
+[kernel] Parsing precedence.i (no preprocessing)
+[kernel:annot-error] precedence.i:90: Warning:
unexpected token ';'
-[kernel:annot-error] tests/wp_acsl/precedence.i:135: Warning:
+[kernel:annot-error] precedence.i:135: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:134: Warning:
+[kernel:annot-error] precedence.i:134: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:133: Warning:
+[kernel:annot-error] precedence.i:133: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:132: Warning:
+[kernel:annot-error] precedence.i:132: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:130: Warning:
+[kernel:annot-error] precedence.i:130: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:129: Warning:
+[kernel:annot-error] precedence.i:129: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:128: Warning:
+[kernel:annot-error] precedence.i:128: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:127: Warning:
+[kernel:annot-error] precedence.i:127: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:125: Warning:
+[kernel:annot-error] precedence.i:125: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:124: Warning:
+[kernel:annot-error] precedence.i:124: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:123: Warning:
+[kernel:annot-error] precedence.i:123: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:122: Warning:
+[kernel:annot-error] precedence.i:122: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:120: Warning:
+[kernel:annot-error] precedence.i:120: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:119: Warning:
+[kernel:annot-error] precedence.i:119: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:118: Warning:
+[kernel:annot-error] precedence.i:118: Warning:
Inconsistent relation chain.
-[kernel:annot-error] tests/wp_acsl/precedence.i:175: Warning:
+[kernel:annot-error] precedence.i:175: Warning:
R is not a logic variable. Ignoring code annotation
-[kernel:annot-error] tests/wp_acsl/precedence.i:176: Warning:
+[kernel:annot-error] precedence.i:176: Warning:
P is not a logic variable. Ignoring code annotation
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
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 4d389265cd8cfe3e45d227c229e032c109d86e81..ec9aaa9da5506e11f915ce26ee3e742e765a6e7b 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/range.i (no preprocessing)
+[kernel] Parsing range.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 119c06c6c1dfbb48898ce45bc196e5c3689084ff..5bc26fcefecb866a006e2850db6ce1f649a85a91 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/reads.i (no preprocessing)
+[kernel] Parsing reads.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
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 213fdec4cb23e08311a46680cd43fd429fcbdb8b..d7762f73d156acb1bea76d496eb4735f52abaedc 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/reads.i (no preprocessing)
+[kernel] Parsing reads.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 aafa831a5d6a86746fef022bccf843e81e16bd6e..a12022bdc954d0f5bff0dd617e5344363f9262b9 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/record.i (no preprocessing)
+[kernel] Parsing record.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 11 goals scheduled
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 9ee1634559a2f85d09871a1b2067cc62165789fc..cf42c84adc358cc5999d2fd4a05c69b925dcf2c5 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/record.i (no preprocessing)
+[kernel] Parsing record.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 514d6f40bcb0115e003f31c0188db30b84330fa2..64ff3d3d62f73f7e7ec8b87b02db286009cea7b1 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/simpl_is_type.i (no preprocessing)
+[kernel] Parsing simpl_is_type.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 18 goals scheduled
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 5eebd01bb772c8c769aad75003426bde3ce45e22..22981e0025789ca58fb3fe1e9623ba132e06792c 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/sizeof.i (no preprocessing)
+[kernel] Parsing sizeof.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 3b8c905ab63c750db0beaea8c971bb48aa3f7200..1efc688a87a3276648750b06a2369201334f4a17 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
-[kernel] Parsing tests/wp_acsl/struct_use_case.i (no preprocessing)
+[kernel] Parsing struct_use_case.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 f43f461d6c19f94662e891f022c78bad8b526551..8ac28e497ac9db37cdcd00644687e0b506a0165b 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Caveat)' -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/struct_use_case.i (no preprocessing)
+[kernel] Parsing struct_use_case.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 bad7bc16a7c6f386454f91feeaed9372c22b7c5b..678ead75a09a52d12646a33a60c522dc7c4244ba 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/tset.i (no preprocessing)
+[kernel] Parsing tset.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 4 goals scheduled
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 d891a56629221496f7672b2df57900c1cf543c29..171329197f0bf0153a41a8feb09a2678a937b917 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/type_guard.i (no preprocessing)
+[kernel] Parsing type_guard.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 6cd53f6a5bbe80f3012e01a633118bcdac18a013..f3b30166b51ffed151281f6379b41bd59841076d 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/type_guard.i (no preprocessing)
+[kernel] Parsing type_guard.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 e1fcca70b0a74d4ec83cc56da21c38db1866d05f..7d027492563279fb94f5533303ea358ff345a679 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/unit_bit_test.c (with preprocessing)
+[kernel] Parsing unit_bit_test.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 6d9d902295debff8da4f9c576a73dc4a62c9c02e..2d38dce71597782d91ac2a3ece7bac586ef927f7 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/unit_bool.i (no preprocessing)
+[kernel] Parsing unit_bool.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 15 goals scheduled
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 022b0364fa9ee3d9b289bfb3c241136c2e77bb6b..421d5032376351d5ec926a3e903fd0e1f1f18a08 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/user_def_type_guard.i (no preprocessing)
+[kernel] Parsing user_def_type_guard.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 0368f3b6126af38d9c7dc865d96336e7677090bd..0b69f7daf855c680a12fa4ba643a777ea613255b 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/user_def_type_guard.i (no preprocessing)
+[kernel] Parsing user_def_type_guard.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 15fb0108e378694f738e976e4a1618109cb9519f..249f9cac609a8301b06a5c04218c2bad41fa85d4 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/bts0708.i (no preprocessing)
+[kernel] Parsing bts0708.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 fbd210f679cb91ec29196a1b2f0e5f4b01f8f764..dc3a0c6f89ddaa6b7aa7aac81cabd82ad0549f6e 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/bts0843.i (no preprocessing)
+[kernel] Parsing bts0843.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 7f1e9b6e40fe2f7f02428d4290e889a9fc0c5d1b..dbb98c6df14292b6b3f805888a739fec56d47ac8 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,5 +1,5 @@
# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/wp_bts/bts779.i (no preprocessing)
+[kernel] Parsing bts779.i (no preprocessing)
[wp] Running WP plugin...
[rte] annotating function f
[wp] 2 goals scheduled
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 07263eaba248a77e6041f55a890d6f20ca8d897a..2554eb4273100d2abe3dcee96add314211fd3636 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_bts/bts788.i (no preprocessing)
+[kernel] Parsing bts788.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 8d3d1c250bfcf2ce2a168b360d6dd34898d11e1f..0ef4130fb85ebf15d969fdf3552a4109366d47bd 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_bts/bts986.i (no preprocessing)
+[kernel] Parsing bts986.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 2cdd4e30969e83cd3bcbaaaa19602507ea67c65f..d9a23912c0146b7c40b02c375c68271fcab0e186 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Real)' [...]
-[kernel] Parsing tests/wp_bts/bts_1174.i (no preprocessing)
+[kernel] Parsing bts_1174.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Warning: native support for coq is deprecated, use tip instead
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 e3b5535c1cb8a5f5e3557c9a4fe0ef85b2566b19..e8fdfc5b1a2df94f96ccd14a406c6c401b759072 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_bts/bts_1176.i (no preprocessing)
+[kernel] Parsing bts_1176.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 0d96c29ae0cfc5a4764a83ebf72d2b57b8f48240..5072e7c6182b7fce459e1727cd69ba7b7bb4f8b5 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,5 +1,5 @@
# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/wp_bts/bts_1360.i (no preprocessing)
+[kernel] Parsing bts_1360.i (no preprocessing)
[wp] Running WP plugin...
[rte] annotating function foo_correct
[rte] annotating function foo_wrong
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 c34b04935c1d1bddbbe582eea0d3fc8cfdc4f5ae..53303432f91d102e7a2331fab3a36a581581a6b5 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/bts_1462.i (no preprocessing)
+[kernel] Parsing bts_1462.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 13 goals scheduled
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 5d88cb99d2cc007af88b732ec74b9808ac99452b..326de6e3cf4e153c73ec6ea2ea27d607a4a750fe 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/bts_1586.i (no preprocessing)
+[kernel] Parsing bts_1586.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 4b070090eaa9f81b91cddfdb7c1827c22dcce062..5e2c4f9562f58ea4734d7278913377ae3c04a605 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,10 +1,10 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/bts_1588.i (no preprocessing)
+[kernel] Parsing bts_1588.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_bts/bts_1588.i:19: Warning:
+[wp] bts_1588.i:19: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_bts/bts_1588.i:5: Warning:
+[wp] bts_1588.i:5: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_f_loop_invariant_l1_2_preserved : Valid
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 86708cc7d79dc64c967451ea2382b2cc185d3eb5..c27e58cfd85bd5426ab168004469c17a71c4bdea 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/bts_1601.c (with preprocessing)
+[kernel] Parsing bts_1601.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
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 91203bd8a7c316be36b9377c010047ff59f965b9..2ad49d15f3ed765b5c4792651b80ffbb172ba298 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/bts_1828.i (no preprocessing)
+[kernel] Parsing bts_1828.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 e5edde37e9b7b942c93989d95bb6fd04d5118460..45b60a0df05e954f7480d87da0f46c7d4871663a 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_bts/bts_1828.i (no preprocessing)
+[kernel] Parsing bts_1828.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 c47673e6b51df770410f04e7619b358ecea293f0..a407bf2ca06447efd20ca4067f5bc38ad11527bf 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/bts_2040.i (no preprocessing)
+[kernel] Parsing bts_2040.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 6f837f71940fa5aaa41c56c688dcd642832c139f..cb6c2c3d0f1d294c989e3f5e7b1bdbb54b1448c9 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/bts_2079.i (no preprocessing)
+[kernel] Parsing bts_2079.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 c02dc9c178f3388a2f3c6212d3f540aabdb1a1db..786136c4a21485711dd42dec053c7474c8a363b8 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/bts_2159.i (no preprocessing)
+[kernel] Parsing bts_2159.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 99642408d02d9bb3678f5267181dfb4e16a0d6bd..7aee840f3b3d3be6a1047e55e3e71bba815d19b8 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,5 +1,5 @@
# frama-c -wp -wp-timeout 1 [...]
-[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
+[kernel] Parsing bts_2471.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 ffb3913bc3829c2336a99250827f72c490e1ca85..725a63572bd50abb6c1cebeaca9117219a74b625 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,5 +1,5 @@
# frama-c -wp -wp-timeout 1 [...]
-[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
+[kernel] Parsing bts_2471.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
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 daef8736024e638253e9724c9732a577d90cb7df..8d031ef0aec0346a1b754a010c2e9c610ff308a1 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
+[kernel] Parsing bts_2471.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Warning: native support for coq is deprecated, use tip instead
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 abf5b9692634744f0f1b390c33f4920e344ebc89..6f05d1615c3d1f0f863289bba00e0a343393c545 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/ergo_typecheck.i (no preprocessing)
+[kernel] Parsing ergo_typecheck.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
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 ea1d384da71ead051acf621bac6241aa441336bc..41b0c6bc7835644f9b8938f263fcbecadfd9f94e 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue-364.i (no preprocessing)
+[kernel] Parsing issue-364.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 be5d63c71f629ebf2cfc190d1532174e3f93b970..8792b49802b3cb43fb62f9aa8f5de49c55f4a7da 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue-684-exit.c (with preprocessing)
+[kernel] Parsing issue-684-exit.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 9d615ddd682dd47aa3bb673b79d3b40cb090cb74..ae88c968f4f93ede1636f0bfdd4f27dd1e5ab0ab 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
+[kernel] Parsing issue_143.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
[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 08841f4f3a5743e7882829ae4b5b2530c704ef60..dbc3692bd3d94259a85fbabd4eb7eac19af49ccf 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
+[kernel] Parsing issue_143.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 2 goals scheduled
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 9d615ddd682dd47aa3bb673b79d3b40cb090cb74..ae88c968f4f93ede1636f0bfdd4f27dd1e5ab0ab 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
+[kernel] Parsing issue_143.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
[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 376255d0dcbdd0874f047745de334d291a25548a..0d5c8468befb51d60e927cd08d092d4b7af892f0 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
+[kernel] Parsing issue_143.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 2 goals scheduled
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 19ffd064dfc2f54284c5d1c1ba830da766e51f95..ca918c67e926f344dd1ea6e2125fadeba4a239df 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_198.i (no preprocessing)
+[kernel] Parsing issue_198.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_broken : Valid
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 df5e033c97cf32024c587ccc4efe29ecd824e07b..819ed2e218dfbf3b559aa8893c5cbbd79c2e0ef8 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_447.i (no preprocessing)
+[kernel] Parsing issue_447.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_foo : Valid
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 c4d33cc9b69a9af5442f34759db1c02b3fd3aa32..193391696738af597851faf822d15c08a2f2dbfa 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_453.i (no preprocessing)
+[kernel] Parsing issue_453.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 437f33f00c3f348ac81f2cec3c4520c286180eae..ac23b5b748d3a6326e159cd81afd0b05f1526109 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_494.i (no preprocessing)
+[kernel] Parsing issue_494.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 f5c735d0395f2270a0b38e8c52423f4688eea914..75201f17f4253955d31304aa96b4f2bb1d55c9d6 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_508.c (with preprocessing)
+[kernel] Parsing issue_508.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 87633b0ea70e4a4143717cec91bbe1ceba92e119..9a296ca593e37d3a3e1a906b786d309493539cd0 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_711.i (no preprocessing)
+[kernel] Parsing issue_711.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_A : Valid
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 2ab4a1454a9c1cf87dce7dc02bf19b648ae792ad..f9c7a0b47638cfc0373ca3b1803d653525530564 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,7 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_715_a.i (no preprocessing)
+[kernel] Parsing issue_715_a.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] tests/wp_bts/issue_715_a.i:6: Warning:
+[kernel] 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
[wp] 1 goal scheduled
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 694a10a84e816776f16530112304a39f25cb8716..301704e67cdee613d0b2f45c0df9fcfb9c68aa6b 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,7 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_715_b.i (no preprocessing)
+[kernel] Parsing issue_715_b.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] tests/wp_bts/issue_715_b.i:9: Warning:
+[kernel] 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
[wp] 2 goals scheduled
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 6fc62ce363bb63402e570f6ae0c8ab870bee5c61..69f63c6e1c94ed8159119284c2bcf135b224b07b 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_751.i (no preprocessing)
+[kernel] Parsing issue_751.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 40 goals scheduled
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 455278246bd518ab7843f951f86963da8d6c9ae1..586d8294e154d026c8798b1e6ba4df57bfe647c5 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_801.i (no preprocessing)
+[kernel] Parsing issue_801.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 30935254772c056f74fa6ec471beff51f1e79d08..bfa4234e9e17408482bb240c9acbad5dd6fe1927 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_81.i (no preprocessing)
+[kernel] Parsing issue_81.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 2b809a025c2ffac3da40e70fc650e26459984b06..da5dce9d62d3921e0ae191b335a7114011932519 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_825.i (no preprocessing)
+[kernel] Parsing issue_825.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
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 64c3d264d8c78c5fc4f60fd53162e685061f1d06..4d1f471075924c29add33d5fee2570c17dd90fa0 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_837.c (with preprocessing)
+[kernel] Parsing issue_837.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
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 9e1e9bcdbead3094f0f8b7672cd5ea7de62f534d..ca195b3e2f08d3891f1fd5e3632c36952e906c4b 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_898.i (no preprocessing)
+[kernel] Parsing issue_898.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 164271bc40ab026c97fa2a3ab4579fcb40c49bda..d443e190ef6891366afe204ac1d9d4476191f699 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/nupw-bcl-bts1120.i (no preprocessing)
+[kernel] Parsing nupw-bcl-bts1120.i (no preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal unreachable_smt_with_contract_assigns : Valid (Unreachable)
[wp] [CFG] Goal unreachable_smt_with_contract_exits_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 2bf3e0ea994f79997ec9562c77d3408aac591fd3..8b3b8ce8f5b18a8b19ab37dd367fb7231c48f8bf 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,5 +1,5 @@
# frama-c -wp -wp-rte -wp-timeout 20 -warn-unsigned-overflow [...]
-[kernel] Parsing tests/wp_gallery/binary-multiplication-without-overflow.c (with preprocessing)
+[kernel] Parsing binary-multiplication-without-overflow.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function BinaryMultiplication
[wp] 16 goals scheduled
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 c0a3091f89c5126ccf596644dbedb9dedd65dfbc..374c185811eccbf13ab99836f863fcb6f43c8ccb 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,5 +1,5 @@
# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/wp_gallery/binary-multiplication.c (with preprocessing)
+[kernel] Parsing binary-multiplication.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function BinaryMultiplication
[wp] 17 goals scheduled
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 a081d0c388b7caff1c718d895bacd308dfeaf6aa..0760f8c1ed9a053d7dae27231140e001e240e7e1 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_gallery/find.i (no preprocessing)
+[kernel] Parsing find.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 41 goals scheduled
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 06ee2377636c52ca390ad6ed61e81275c8185c01..4b982f51859e9264450636ff771075ff5d74795a 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_gallery/frama_c_exo1_solved.c (with preprocessing)
+[kernel] Parsing frama_c_exo1_solved.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
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 1780ec5c89a9b45027afa30b5a132043047e4271..d3b25a868125a1e2dafa3c01cd819c5ab0bcf968 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_gallery/frama_c_exo2_solved.c (with preprocessing)
+[kernel] Parsing frama_c_exo2_solved.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 22 goals scheduled
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 e75ffe7ec64e8d454c01d3b2497ea7e10bd7e9c7..5795b95d8a27537135312148524f359331267906 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.old.c (with preprocessing)
+[kernel] Parsing frama_c_exo3_solved.old.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 34 goals scheduled
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 7672a505bc9fa5d57e9cd506b0e0b2ed7d01591d..fcd4c52bc00f465c3b346ae0522c976c431174c2 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.old.v2.c (with preprocessing)
+[kernel] Parsing frama_c_exo3_solved.old.v2.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 35 goals scheduled
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 72409b7f36cfd6816e0e20df25e04071390908b1..e2cf934a567dc28914fecb97236a1751f6fcb264 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.simplified.c (with preprocessing)
+[kernel] Parsing frama_c_exo3_solved.simplified.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 26 goals scheduled
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 b9066d9921a764ee6e240b742d1f8f5c6387d265..c99172a223bc3449ae605c420826261c541b5494 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_gallery/frama_c_hashtbl_solved.c (with preprocessing)
+[kernel] Parsing frama_c_hashtbl_solved.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 102 goals scheduled
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 a86dae9951bdf6be94cf4c1213e92c65b93591a9..940355bf8dd007765944c8173ebf5315bc89a1c0 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_gallery/loop-statement.c (with preprocessing)
+[kernel] Parsing loop-statement.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 15 goals scheduled
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 33a25d793ff22746cb810bbf039b5d65e0bc4bf5..0c71166950ca540ca3883d76687323b3922c87b7 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_hoare/alias_assigns_hypotheses.i (no preprocessing)
+[kernel] Parsing alias_assigns_hypotheses.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 30 goals scheduled
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 0b6ce2d0287b4891e9671afb5c1289c56e821b62..2ee1cf41475b640699aca87e439366afbb78bd4e 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_hoare/byref.i (no preprocessing)
+[kernel] Parsing byref.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 12 goals scheduled
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 48e1936e19564287ad810f53ddca2ccc7767dc19..5018eadab7ed616992e0fd97ed6126ab57ae8ff0 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_hoare/byref.i (no preprocessing)
+[kernel] Parsing byref.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 12 goals scheduled
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 d97c3812bd67b8c5da17e69e66ce4c1cbed3317e..300ffa2c96e9ee6fa5cb61203ad60527f9bd84e7 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_hoare/dispatch_var.i (no preprocessing)
+[kernel] Parsing dispatch_var.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 78 goals scheduled
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 b5878139820eb2eed4ceb79df18a6690a4635426..774ebc54b577f113869aaa54fe88b5a0dcc11562 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' -wp-no-let [...]
-[kernel] Parsing tests/wp_hoare/dispatch_var2.i (no preprocessing)
+[kernel] Parsing dispatch_var2.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 34 goals scheduled
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 7a50ede52eb9de48083e80185e8fbe5291b9697e..250357cf24abbb54d002fa65c4133e06806591ce 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_hoare/dispatch_var2.i (no preprocessing)
+[kernel] Parsing dispatch_var2.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 34 goals scheduled
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 04d5a4f2629e07014d67d846237693ab7173469d..eca3be2dd3bef570d1700b6a5f80b6ac517cd46d 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_hoare/isHoare.i (no preprocessing)
+[kernel] Parsing isHoare.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 efe1f7fdd1764a4ad45bbfb19fcdcd8323071f27..03796d3e4160058e1fd1f5cf57b0ba22a0d72ba1 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_hoare/logicarr.i (no preprocessing)
+[kernel] Parsing logicarr.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 1c127a17545a9535c8a1e6cecf08379654f649e9..273fdfb6090ad3424decc6d4a5f26d03e758c915 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_hoare/logicref.i (no preprocessing)
+[kernel] Parsing logicref.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
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 061f51954cab858b515c5e3320d909ba303ed652..fab483750f3c179f129747d79a9e2b03f4a81bd7 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_hoare/logicref_simple.i (no preprocessing)
+[kernel] Parsing logicref_simple.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
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 81897c8db12744ff443786b8e730f7f1adcccc89..4a8b2e9e2322b9816a7a543a874848f6d982add1 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_hoare/reference.i (no preprocessing)
+[kernel] Parsing reference.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 23 goals scheduled
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 9da7484d4d2dbe1ef5e6c0d68b4f796d572e69ac..65ceafb33562951bf33d8bf8374e23a2ff959905 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_hoare/reference_and_struct.i (no preprocessing)
+[kernel] Parsing reference_and_struct.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 32 goals scheduled
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 5fa325b91701864750b7557fa6443415d74dbdb9..aa93fe826b9ac6ae17d74bb5ffbb779ec5243b58 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_hoare/reference_array.i (no preprocessing)
+[kernel] Parsing reference_array.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 36 goals scheduled
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 b5390221da4d396ad6e3c0fdb1de95711c8dad3d..f0b5d3dee657e31d31380c14e06cb635ef756f5c 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_hoare/reference_array_simple.i (no preprocessing)
+[kernel] Parsing reference_array_simple.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 02a4bffe2c4d64132a21a44142ddcf9bf1b3f99f..0dcc419ece02133ae2f9e587a23ce79b480c48ad 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_hoare/refguards.i (no preprocessing)
+[kernel] Parsing refguards.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
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 213ee06d29f83d84f773c31e96b4e084d01aa723..9cf58bd601e8188d778074453af0f355bec5028c 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
@@ -1,7 +1,7 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_manual/manual.i (no preprocessing)
-[kernel] Parsing tests/wp_manual/working_dir/swap.c (with preprocessing)
-[kernel] Parsing tests/wp_manual/working_dir/swap1.h (with preprocessing)
+[kernel] Parsing manual.i (no preprocessing)
+[kernel] Parsing working_dir/swap.c (with preprocessing)
+[kernel] Parsing working_dir/swap1.h (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 4f1030ab27018000d462c3def8e475fbbfc77d40..fb13236dbf626facd576c4934ec557d2b0285c38 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
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/wp_manual/manual.i (no preprocessing)
-[kernel] Parsing tests/wp_manual/working_dir/swap.c (with preprocessing)
-[kernel] Parsing tests/wp_manual/working_dir/swap2.h (with preprocessing)
+[kernel] Parsing manual.i (no preprocessing)
+[kernel] Parsing working_dir/swap.c (with preprocessing)
+[kernel] Parsing working_dir/swap2.h (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function swap
[wp] 8 goals scheduled
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle
index 16973c988dfa103fb3ffbe0141d213bc689cee51..15ac0f70d86c802229aaf2fdac0953b775713f3f 100644
--- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle
@@ -14,15 +14,15 @@
by Wp.typed.
[ Valid ] Post-condition 'B'
by Wp.typed.
-[ Valid ] Assigns (file tests/wp_manual/working_dir/swap2.h, line 4)
+[ Valid ] Assigns (file working_dir/swap2.h, line 4)
by Wp.typed.
-[ Valid ] Assertion 'rte,mem_access' (file tests/wp_manual/working_dir/swap.c, line 3)
+[ Valid ] Assertion 'rte,mem_access' (file working_dir/swap.c, line 3)
by Wp.typed.
-[ Valid ] Assertion 'rte,mem_access' (file tests/wp_manual/working_dir/swap.c, line 4)
+[ Valid ] Assertion 'rte,mem_access' (file working_dir/swap.c, line 4)
by Wp.typed.
-[ Valid ] Assertion 'rte,mem_access' (file tests/wp_manual/working_dir/swap.c, line 4)
+[ Valid ] Assertion 'rte,mem_access' (file working_dir/swap.c, line 4)
by Wp.typed.
-[ Valid ] Assertion 'rte,mem_access' (file tests/wp_manual/working_dir/swap.c, line 5)
+[ Valid ] Assertion 'rte,mem_access' (file working_dir/swap.c, line 5)
by Wp.typed.
[ Valid ] Default behavior
by Frama-C kernel.
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 16adfa4946a202a912a9f1e69902616b1b347e1b..de73a52c63e3026ab576bcadbd8737f22aa5f7cf 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/abs.i (no preprocessing)
+[kernel] Parsing abs.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 3c71816dbbf88a9d7a7ab0c8471e5af0d0cc782f..146552b7f55e6cec0927dd4ce0cc23678597b4dc 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/abs.i (no preprocessing)
+[kernel] Parsing abs.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Warning: native support for coq is deprecated, use tip instead
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 d5a8298ccca7d9cfe5363da017189ff878149463..34c366ca1cffba4cf705fc0c994faccac7529d81 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/abs.i (no preprocessing)
+[kernel] Parsing abs.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
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 344e6b078479a4d7fdc25ab603de7bec24424f63..31c221bc3497394e30eadd663da85385fa0d0e02 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/asm.i (no preprocessing)
+[kernel] Parsing asm.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 fef95834e2e117d45fffb152ca684dc76202a36b..c99721def5a43854721730bff8f1d334cbff621a 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/bit_test.c (with preprocessing)
+[kernel] Parsing bit_test.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
index b908bc8578a9a582d5db8cd077546571368e4e06..38370a03818c44eb4fc4c81e1b7f1b0a4595af70 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
@@ -1,5 +1,5 @@
# frama-c -wp -wp-no-let -wp-timeout 45 -wp-steps 1500 [...]
-[kernel] Parsing tests/wp_plugin/bool.i (no preprocessing)
+[kernel] Parsing bool.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
@@ -14,8 +14,8 @@
[wp] Proved goals: 3 / 7
Qed: 2
Alt-Ergo 2.0.0: 1 (unsuccess: 4)
-[wp] Report in: 'tests/wp_plugin/oracle_qualif/bool.0.report.json'
-[wp] Report out: 'tests/wp_plugin/result_qualif/bool.0.report.json'
+[wp] Report in: 'oracle_qualif/bool.0.report.json'
+[wp] Report out: 'result_qualif/bool.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job - - 1 0.0%
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 dac2be58e75ca61486ac7ca1bf782c6ba092b8b7..d72ac023e65b130fa5628e08fe1ec5624d2aa47a 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,5 +1,5 @@
# frama-c -wp -wp-no-let [...]
-[kernel] Parsing tests/wp_plugin/bool.i (no preprocessing)
+[kernel] Parsing bool.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
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 c58a574b23eb0ec75c989e921af89d71396dd902..e0b8fc01010c34eed4093e0cc1c487eb78511a30 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/convert.i (no preprocessing)
+[kernel] Parsing convert.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ceil : 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 e920dbe12565b8c038bde60962d817e0c4b4a18f..7bd9172a0194f3c00e9b0a7735d563aa01a970fd 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/convert.i (no preprocessing)
+[kernel] Parsing convert.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
[wp] 2 goals scheduled
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 097475c27feafea1e41d76ecac880a822f1df06e..e0dfdd314121b4941bfe645786d7f0b45dcbc541 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/copy.i (no preprocessing)
+[kernel] Parsing copy.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 11 goals scheduled
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 06068093e7ee75e3358fe8d141511712ef6c71b0..668ba7d83d98a2ae14615230b83155c9a785da14 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,18 +1,18 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/doomed.i (no preprocessing)
+[kernel] Parsing doomed.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
[wp] [Passed] Smoke-test typed_foo_wp_smoke_default_requires
[wp] [Failed] Smoke-test typed_foo_wp_smoke_A_requires
Qed: Valid
-[wp] tests/wp_plugin/doomed.i:27: Warning: Failed smoke-test
+[wp] doomed.i:27: Warning: Failed smoke-test
[wp] [Passed] Smoke-test typed_foo_wp_smoke_B_requires
[wp] [Passed] Smoke-test typed_bar_wp_smoke_default_requires
[wp] [Qed] Goal typed_bar_ensures : Valid
[wp] [Failed] Smoke-test typed_buzz_wp_smoke_default_requires
Qed: Valid
-[wp] tests/wp_plugin/doomed.i:41: Warning: Failed smoke-test
+[wp] doomed.i:41: Warning: Failed smoke-test
[wp] [Qed] Goal typed_buzz_ensures : Valid
[wp] Proved goals: 5 / 7
Qed: 2 (failed: 2)
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 dfc863b89cdfe6e7648fedbe5d393fb95c5b2704..c455b41304a04c8cfad7160a008292ff77e6361d 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,17 +1,17 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/doomed_axioms.i (no preprocessing)
+[kernel] Parsing doomed_axioms.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_loop_s2
Alt-Ergo: Valid
-[wp] tests/wp_plugin/doomed_axioms.i:29: Warning: Failed smoke-test
+[wp] doomed_axioms.i:29: Warning: Failed smoke-test
[wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_code_s7
Alt-Ergo: Valid
-[wp] tests/wp_plugin/doomed_axioms.i:30: Warning: Failed smoke-test
+[wp] doomed_axioms.i:30: Warning: Failed smoke-test
[wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_code_s9
Alt-Ergo: Valid
-[wp] tests/wp_plugin/doomed_axioms.i:32: Warning: Failed smoke-test
+[wp] doomed_axioms.i:32: Warning: Failed smoke-test
[wp] [Alt-Ergo] Goal typed_foo_loop_invariant_A_preserved : Valid
[wp] [Alt-Ergo] Goal typed_foo_loop_invariant_A_established : Valid
[wp] [Alt-Ergo] Goal typed_foo_loop_invariant_B_preserved : Valid
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 b1a5c4a4fbc09fcce1b714599901ea1f0c29643e..771195e0c0a4c6c66b30306e919610a0fcf60892 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/doomed_call.i (no preprocessing)
+[kernel] Parsing doomed_call.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
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 130e2f527e0c702d8d61de7871768a960821ad7e..cddd70df9fbe89f47e90ffe7548bb7e8531ff9bb 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/doomed_call.i (no preprocessing)
+[kernel] Parsing doomed_call.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 33 goals scheduled
@@ -17,10 +17,10 @@
[wp] [Qed] Goal typed_f2_ok_exits : Valid
[wp] [Failed] Smoke-test typed_call_ko_wp_smoke_dead_call_s14
Qed: Valid
-[wp] tests/wp_plugin/doomed_call.i:68: Warning: Failed smoke-test
+[wp] doomed_call.i:68: Warning: Failed smoke-test
[wp] [Failed] Smoke-test typed_f3_ko_wp_smoke_dead_code_s15
Qed: Valid
-[wp] tests/wp_plugin/doomed_call.i:69: Warning: Failed smoke-test
+[wp] doomed_call.i:69: Warning: Failed smoke-test
[wp] [Qed] Goal typed_f3_ko_ensures : Valid
[wp] [Passed] Smoke-test typed_call_exit_ok_wp_smoke_dead_call_s18
[wp] [Qed] Goal typed_f3_ok_ensures : Valid
@@ -28,7 +28,7 @@
[wp] [Qed] Goal typed_f4_ok_ensures : Valid
[wp] [Failed] Smoke-test typed_call_ko_global_wp_smoke_dead_call_s26
Qed: Valid
-[wp] tests/wp_plugin/doomed_call.i:89: Warning: Failed smoke-test
+[wp] doomed_call.i:89: Warning: Failed smoke-test
[wp] [Qed] Goal typed_f4_ko_ensures : Valid
[wp] [Passed] Smoke-test typed_call_effect_wp_smoke_dead_call_s29
[wp] [Passed] Smoke-test typed_call_effect_wp_smoke_dead_call_s30
@@ -40,11 +40,11 @@
[wp] [Passed] Smoke-test typed_call_effect_wp_smoke_dead_call_s34
[wp] [Failed] Smoke-test typed_call_effect_wp_smoke_dead_call_s36
Qed: Valid
-[wp] tests/wp_plugin/doomed_call.i:121: Warning: Failed smoke-test
+[wp] doomed_call.i:121: Warning: Failed smoke-test
[wp] [Passed] Smoke-test typed_f5_ko_wp_smoke_dead_code_s35
[wp] [Failed] Smoke-test typed_f5_ko_wp_smoke_dead_code_s36
Qed: Valid
-[wp] tests/wp_plugin/doomed_call.i:121: Warning: Failed smoke-test
+[wp] doomed_call.i:121: Warning: Failed smoke-test
[wp] [Qed] Goal typed_f5_ko_ensures : Valid
[wp] Proved goals: 28 / 33
Qed: 10 (failed: 5)
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 cfbb11197d446202f248457926496f212dfb6492..23c3c026e3f0c30c825d0023ec10723aeef01ccf 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,5 +1,5 @@
# frama-c -wp -wp-split [...]
-[kernel] Parsing tests/wp_plugin/doomed_call.i (no preprocessing)
+[kernel] Parsing doomed_call.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 36 goals scheduled
@@ -20,10 +20,10 @@
[wp] [Qed] Goal typed_f2_ok_exits_part2 : Valid
[wp] [Failed] Smoke-test typed_call_ko_wp_smoke_dead_call_s14
Qed: Valid
-[wp] tests/wp_plugin/doomed_call.i:68: Warning: Failed smoke-test
+[wp] doomed_call.i:68: Warning: Failed smoke-test
[wp] [Failed] Smoke-test typed_f3_ko_wp_smoke_dead_code_s15
Qed: Valid
-[wp] tests/wp_plugin/doomed_call.i:69: Warning: Failed smoke-test
+[wp] doomed_call.i:69: Warning: Failed smoke-test
[wp] [Qed] Goal typed_f3_ko_ensures : Valid
[wp] [Passed] Smoke-test typed_call_exit_ok_wp_smoke_dead_call_s18
[wp] [Qed] Goal typed_f3_ok_ensures : Valid
@@ -31,7 +31,7 @@
[wp] [Qed] Goal typed_f4_ok_ensures : Valid
[wp] [Failed] Smoke-test typed_call_ko_global_wp_smoke_dead_call_s26
Qed: Valid
-[wp] tests/wp_plugin/doomed_call.i:89: Warning: Failed smoke-test
+[wp] doomed_call.i:89: Warning: Failed smoke-test
[wp] [Qed] Goal typed_f4_ko_ensures : Valid
[wp] [Passed] Smoke-test typed_call_effect_wp_smoke_dead_call_s29
[wp] [Passed] Smoke-test typed_call_effect_wp_smoke_dead_call_s30
@@ -43,11 +43,11 @@
[wp] [Passed] Smoke-test typed_call_effect_wp_smoke_dead_call_s34
[wp] [Failed] Smoke-test typed_call_effect_wp_smoke_dead_call_s36
Qed: Valid
-[wp] tests/wp_plugin/doomed_call.i:121: Warning: Failed smoke-test
+[wp] doomed_call.i:121: Warning: Failed smoke-test
[wp] [Passed] Smoke-test typed_f5_ko_wp_smoke_dead_code_s35
[wp] [Failed] Smoke-test typed_f5_ko_wp_smoke_dead_code_s36
Qed: Valid
-[wp] tests/wp_plugin/doomed_call.i:121: Warning: Failed smoke-test
+[wp] doomed_call.i:121: Warning: Failed smoke-test
[wp] [Qed] Goal typed_f5_ko_ensures : Valid
[wp] Proved goals: 31 / 36
Qed: 13 (failed: 5)
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 0b349526c40d14e9bc6ee38bd5e6574999977b81..4efceed332f18825d9ee2099f4d871ec5f08309d 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/doomed_dead.i (no preprocessing)
+[kernel] Parsing doomed_dead.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 46 goals scheduled
@@ -18,7 +18,7 @@
[wp] [Passed] Smoke-test typed_f2_ko_wp_smoke_dead_code_s22
[wp] [Failed] Smoke-test typed_f2_ko_wp_smoke_dead_code_s23
Qed: Valid
-[wp] tests/wp_plugin/doomed_dead.i:44: Warning: Failed smoke-test
+[wp] doomed_dead.i:44: Warning: Failed smoke-test
[wp] [Passed] Smoke-test typed_f2_ko_wp_smoke_dead_code_s26
[wp] [Qed] Goal typed_f2_ko_assigns_exit : Valid
[wp] [Qed] Goal typed_f2_ko_assigns_normal_part1 : Valid
@@ -46,7 +46,7 @@
[wp] [Passed] Smoke-test typed_f5_ko_wp_smoke_dead_code_s56
[wp] [Failed] Smoke-test typed_f5_ko_wp_smoke_dead_code_s61
Qed: Valid
-[wp] tests/wp_plugin/doomed_dead.i:90: Warning: Failed smoke-test
+[wp] doomed_dead.i:90: Warning: Failed smoke-test
[wp] [Passed] Smoke-test typed_f5_ko_wp_smoke_dead_code_s63
[wp] [Passed] Smoke-test typed_f5_ko_wp_smoke_dead_code_s65
[wp] [Qed] Goal typed_f5_ko_assigns_part1 : Valid
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 fd8fae824785bcd829b66d0b40756567adba02b3..2019d6f5586b56d663e273a36e046ce86e0c7863 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,5 +1,5 @@
# frama-c -wp -wp-split [...]
-[kernel] Parsing tests/wp_plugin/doomed_dead.i (no preprocessing)
+[kernel] Parsing doomed_dead.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 48 goals scheduled
@@ -20,7 +20,7 @@
[wp] [Passed] Smoke-test typed_f2_ko_wp_smoke_dead_code_s22
[wp] [Failed] Smoke-test typed_f2_ko_wp_smoke_dead_code_s23
Qed: Valid
-[wp] tests/wp_plugin/doomed_dead.i:44: Warning: Failed smoke-test
+[wp] doomed_dead.i:44: Warning: Failed smoke-test
[wp] [Passed] Smoke-test typed_f2_ko_wp_smoke_dead_code_s26
[wp] [Qed] Goal typed_f2_ko_assigns_exit : Valid
[wp] [Qed] Goal typed_f2_ko_assigns_normal_part1 : Valid
@@ -48,7 +48,7 @@
[wp] [Passed] Smoke-test typed_f5_ko_wp_smoke_dead_code_s56
[wp] [Failed] Smoke-test typed_f5_ko_wp_smoke_dead_code_s61
Qed: Valid
-[wp] tests/wp_plugin/doomed_dead.i:90: Warning: Failed smoke-test
+[wp] doomed_dead.i:90: Warning: Failed smoke-test
[wp] [Passed] Smoke-test typed_f5_ko_wp_smoke_dead_code_s63
[wp] [Passed] Smoke-test typed_f5_ko_wp_smoke_dead_code_s65
[wp] [Qed] Goal typed_f5_ko_assigns_part1 : Valid
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 6cbe64cf0f16c20eda7b2d0d71a9d00e58286748..ea9a729fb715cb28a1912160e9f6b2317f66f069 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,17 +1,17 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/doomed_loop.i (no preprocessing)
+[kernel] Parsing doomed_loop.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
[wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_loop_s2
Qed: Valid
-[wp] tests/wp_plugin/doomed_loop.i:22: Warning: Failed smoke-test
+[wp] doomed_loop.i:22: Warning: Failed smoke-test
[wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_code_s7
Qed: Valid
-[wp] tests/wp_plugin/doomed_loop.i:23: Warning: Failed smoke-test
+[wp] doomed_loop.i:23: Warning: Failed smoke-test
[wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_code_s9
Qed: Valid
-[wp] tests/wp_plugin/doomed_loop.i:25: Warning: Failed smoke-test
+[wp] doomed_loop.i:25: Warning: Failed smoke-test
[wp] [Qed] Goal typed_foo_loop_invariant_A_preserved : Valid
[wp] [Alt-Ergo] Goal typed_foo_loop_invariant_A_established : Unsuccess
[wp] [Qed] Goal typed_foo_loop_invariant_B_preserved : Valid
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 4a65820f41cec1a70848725c4ebd2f33b3c24581..fa0963a210ea29f16925424a20927d37447e7870 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,17 +1,17 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/doomed_report_ko.i (no preprocessing)
+[kernel] Parsing doomed_report_ko.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_loop_s2
Alt-Ergo: Valid
-[wp] tests/wp_plugin/doomed_report_ko.i:29: Warning: Failed smoke-test
+[wp] doomed_report_ko.i:29: Warning: Failed smoke-test
[wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_code_s7
Alt-Ergo: Valid
-[wp] tests/wp_plugin/doomed_report_ko.i:29: Warning: Failed smoke-test
+[wp] doomed_report_ko.i:29: Warning: Failed smoke-test
[wp] [Failed] Smoke-test typed_foo_wp_smoke_dead_code_s9
Alt-Ergo: Valid
-[wp] tests/wp_plugin/doomed_report_ko.i:30: Warning: Failed smoke-test
+[wp] doomed_report_ko.i:30: Warning: Failed smoke-test
[wp] [Alt-Ergo] Goal typed_foo_loop_invariant_A_preserved : Valid
[wp] [Alt-Ergo] Goal typed_foo_loop_invariant_A_established : Valid
[wp] [Alt-Ergo] Goal typed_foo_loop_invariant_B_preserved : Valid
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 c578928320d9953ffa47747f9d26dfaa40927d9f..51405b441152b126651c07267a53551872f1e15b 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/doomed_report_ok.i (no preprocessing)
+[kernel] Parsing doomed_report_ok.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
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 9f20f169f87366f5aa10f1dd022d84d9c87629fe..e01d87f027ba84420e851e196229ddeb4a9b06d5 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,8 +1,8 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/doomed_unroll.i (no preprocessing)
+[kernel] Parsing doomed_unroll.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/doomed_unroll.i:15: Warning:
+[wp] doomed_unroll.i:15: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 5 goals scheduled
[wp] [Passed] Smoke-test typed_foo_wp_smoke_dead_code_s27
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 9144906c8da84fbc097b34efdbe590b66f253b4a..478700185e2469d10361abcf660b596d465bae4a 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,7 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/dynamic.i (no preprocessing)
+[kernel] Parsing dynamic.i (no preprocessing)
[wp] Running WP plugin...
-[wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior
+[wp] dynamic.i:78: Warning: Missing 'calls' for default behavior
[wp] Warning: Missing RTE guards
[wp] 51 goals scheduled
[wp] [Alt-Ergo] Goal typed_call_call_point_f1_f2_s3 : Valid
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 4028fd0e199f2b378fe54f72025b011ae11391a8..933a85f90f260d3d1b192cb2dc1d68cd65528cbb 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/fallback.i (no preprocessing)
+[kernel] Parsing fallback.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.2.0'
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 0d5f90a7526755a6d15610e4881c08abf7e0e1a5..e7deb6e2aa5b7951bf9a5d3b822cf67c0f6483a7 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,5 +1,5 @@
# frama-c -wp -wp-timeout 1 [...]
-[kernel] Parsing tests/wp_plugin/flash.c (with preprocessing)
+[kernel] Parsing flash.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 a01eeba9e85753bb3728a8b18e52179de2ff3f36..867c987d611d88d6f979abe3e3a897ad3a72b4f7 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,7 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/flash.c (with preprocessing)
+[kernel] Parsing flash.c (with preprocessing)
[wp] Running WP plugin...
-[wp] tests/wp_plugin/flash-ergo.driver:2: Warning:
+[wp] flash-ergo.driver:2: Warning:
Redefinition of logic INDEX_init
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 a87892007eea5a1214f99161ef4e1b9826bafe7d..09997a7fac3dfc41bd52eb294988b1d2bdc12825 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/flash.c (with preprocessing)
+[kernel] Parsing flash.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 5ba66e74babbcfc208688d5a4e9b0989e089004b..035a7253a8796855be87d1e57b2c7182febefb46 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
@@ -1,6 +1,6 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing)
-[kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning:
+[kernel] Parsing float_format.i (no preprocessing)
+[kernel:parser:decimal-float] float_format.i:10: Warning:
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...
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 0423017c2be17ac025fcf70e73491281b769971f..0b38dce72acbbe0166038cebb9c17e7bb744cfdb 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
@@ -1,6 +1,6 @@
# frama-c -wp -wp-timeout 100 -wp-steps 5 [...]
-[kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing)
-[kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning:
+[kernel] Parsing float_format.i (no preprocessing)
+[kernel:parser:decimal-float] float_format.i:10: Warning:
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...
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 fcad25a085a2ccc51c4d9b3896c25c7fca9504f2..876b56b73ef0f3a6041262e3113ca6d40502a1f5 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
@@ -1,6 +1,6 @@
# frama-c -wp -wp-timeout 100 -wp-steps 5 [...]
-[kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing)
-[kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning:
+[kernel] Parsing float_format.i (no preprocessing)
+[kernel:parser:decimal-float] float_format.i:10: Warning:
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...
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 265dcf746300cd6547717198ab1ec49ae4e343e5..b9e76a083eb560a3bc135f93845116a3658d197d 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
@@ -1,6 +1,6 @@
# frama-c -wp -wp-model 'Typed (Real)' [...]
-[kernel] Parsing tests/wp_plugin/float_real.i (no preprocessing)
-[kernel:parser:decimal-float] tests/wp_plugin/float_real.i:19: Warning:
+[kernel] Parsing float_real.i (no preprocessing)
+[kernel:parser:decimal-float] float_real.i:19: Warning:
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...
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 a42394bed4b944faad652b0f70e55d095ca69ae7..c7bb7c5f6280115c612b0dffe752b25c86bfab86 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
@@ -1,6 +1,6 @@
# frama-c -wp -wp-model 'Typed' [...]
-[kernel] Parsing tests/wp_plugin/float_real.i (no preprocessing)
-[kernel:parser:decimal-float] tests/wp_plugin/float_real.i:19: Warning:
+[kernel] Parsing float_real.i (no preprocessing)
+[kernel:parser:decimal-float] float_real.i:19: Warning:
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...
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 1d9ae90802a9173944e7f6725c1a27e606548204..faf78acad99845e6306af553cc43d723cf310a6d 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/frame.i (no preprocessing)
+[kernel] Parsing frame.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 a875c26ce74f00b05ef3fded034d1de490509a9c..e5e1c28c161bafa6cb0e994670bbefe3c0a72903 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/ground_real.i (no preprocessing)
+[kernel] Parsing ground_real.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_R : Valid
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 6d7143512ed48ff7e046732495c4230c531fc48a..6ba6b85a7b863238c853add006c0bbf2c5705c78 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,5 +1,5 @@
# frama-c -wp -wp-timeout 240 [...]
-[kernel] Parsing tests/wp_plugin/inductive.c (with preprocessing)
+[kernel] Parsing inductive.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 2 goals scheduled
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 4389c814aec8df535f7d9bbd12b2b51036f6c7e6..a408ed5a7aa067ef03064d5f917b8e30a018d19b 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/init_const.i (no preprocessing)
+[kernel] Parsing init_const.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 2a606446dc508ff2c1ee4c64f75ce2f7a75e7097..b0c49e258b19b081dfd0612e079b878dbb83c7a9 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/init_const_guard.i (no preprocessing)
+[kernel] Parsing init_const_guard.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
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 bbc0f9b17382cdbafbeb6f5a9aa9279ce478c6dc..ff210a2b5b276422c9e290c5af3d3f1e5b849871 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
@@ -1,6 +1,6 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/init_extern.i (no preprocessing)
-[kernel] Parsing tests/wp_plugin/init_linker.i (no preprocessing)
+[kernel] Parsing init_extern.i (no preprocessing)
+[kernel] Parsing init_linker.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 3f9234d02bd81a465147e9d05117667f9dfe9cbd..c3a20d407b6fd093640b8277139376b7cd81575c 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/init_valid.i (no preprocessing)
+[kernel] Parsing init_valid.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 1607fa2719344a9f53471ea5e443d5e3d319ea6d..b6af203f6ca6d80fefbf7c3e2389ed8378a17437 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/initarr.i (no preprocessing)
+[kernel] Parsing initarr.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 65ebd21fce6811c9b33ea504d9ae8136a7f6d9aa..696770932552ba2ba7df2c45031bf32bb95e6b27 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/injector.c (with preprocessing)
+[kernel] Parsing injector.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 13 goals scheduled
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 8730d221d2969eca9b2a83336a5d944037f6874e..fd35b184958ea5f904ac8c82f2fc8344533e4364 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_plugin/injector.c (with preprocessing)
+[kernel] Parsing injector.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 602235b4e1772332174a1428afa250766274b4de..b489f684f7c054439e5aceabe60d4568bb4cb8a3 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/loop.i (no preprocessing)
+[kernel] Parsing loop.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
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 75c868bd36ae05e9b8149506fe3d16a45176c363..24b26ed0544638fb3c55cfed2deede38d7090c86 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,8 +1,8 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/loopcurrent.i (no preprocessing)
+[kernel] Parsing loopcurrent.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/loopcurrent.i:12: Warning:
+[wp] loopcurrent.i:12: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_f_loop_invariant_preserved : Valid
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 f62dda1b35eefa46aabdfd4180461127302e5bd7..3f503a108e3613ba690d37eda50e2865bae6394c 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,8 +1,8 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/loopentry.i (no preprocessing)
+[kernel] Parsing loopentry.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/loopentry.i:12: Warning:
+[wp] loopentry.i:12: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_f_loop_invariant_preserved : Valid
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 111bb4a02c06d23a33d6407e49cf7337e132400d..102c14a3aaa226d33b8a9b76c4dc8e9e961ad0ed 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,10 +1,10 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/loopextra.i (no preprocessing)
+[kernel] Parsing loopextra.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/loopextra.i:6: Warning:
+[wp] loopextra.i:6: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_plugin/loopextra.i:3: Warning:
+[wp] loopextra.i:3: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_f_assert : Valid
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 a212cb8779f94f82742d16dac4a0a92d846a3f36..9b679add50012a09be29523fa602cf37c76ca1d4 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/mask.i (no preprocessing)
+[kernel] Parsing mask.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 4af858324c195a679739ad390d26d65cb4403141..33c44e4df3707bd65474c02a3395dc12f07061e1 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,5 +1,5 @@
# frama-c -wp -wp-timeout 100 -wp-steps 1500 [...]
-[kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
+[kernel] Parsing math.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 30 goals scheduled
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 40753d2a146f38c6a7492f72afbf13ab99e03d60..773a5245836281bda1c4734cac463b776176e985 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,5 +1,5 @@
# frama-c -wp -wp-timeout 100 -wp-steps 1500 [...]
-[kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
+[kernel] Parsing math.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
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 ffc737646cc3751ece484585b3668b9546fa4a87..69ac94a86894ed67b60991613cedc80023e2b4ad 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,5 +1,5 @@
# frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
-[kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
+[kernel] Parsing math.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
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 81ba2360317d22e51aed43fc0ec3e3e828560c6f..d0872807ed58e412921ecbda4ffd377fb27c85eb 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,5 +1,5 @@
# frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
-[kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
+[kernel] Parsing math.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
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 9a0ca70837815110370de4bd01d9653916f4d785..ff97bc71c534b5b33638bfe120f1c0de928f8e66 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
@@ -1,6 +1,6 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/model.i (no preprocessing)
-[kernel] tests/wp_plugin/model.i:10: Warning:
+[kernel] Parsing model.i (no preprocessing)
+[kernel] model.i:10: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle
index 4feaeefdadad2ae6b7ed8f9b8380c50edb7f23d7..2ad3c977064ff6b9105e27b6d16ae0f5a06a713d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle
@@ -1,5 +1,5 @@
# frama-c -wp -wp-timeout 1 -wp-steps 10 [...]
-[kernel] Parsing tests/wp_plugin/no_step_limit.i (no preprocessing)
+[kernel] Parsing no_step_limit.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] [no-steps] Goal typed_lemma_truc : Unsuccess
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 d56af67a5072ba45bb43314c4e3ca5658524abf1..f62cd996de8b64cab69560ddc68c1824ccf25b79 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/nosession.i (no preprocessing)
+[kernel] Parsing nosession.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 f11f92c390ec20461736d7afffab1019345708a9..963e5d8a0998e8e674a65ef555d61a7186011d7f 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/nowp.c (with preprocessing)
+[kernel] Parsing nowp.c (with preprocessing)
[wp] Running WP plugin...
[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 57c1c46213f63ee45bec279856df93aee1788a85..68fe97d6e4fa3fa66f330d8a0def5a8eab97d2f6 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/nth.i (no preprocessing)
+[kernel] Parsing nth.i (no preprocessing)
[wp] Running WP plugin...
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_access_16_16_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 6daeab38c98f63ca1fdf216a7f789be8d86d92c5..a118a81cac6c68f57d7352ac336d6d7815623b90 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/overarray.i (no preprocessing)
+[kernel] Parsing overarray.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 12 goals scheduled
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 5bfb2cf3e3404fc852f21bd6bce54e9d187991a5..b80b06514e7c3ed2285c7f767c8f08197a98e437 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/overassign.i (no preprocessing)
+[kernel] Parsing overassign.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 12 goals scheduled
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 f5af22f701424ef220ab28a18bdebd44c36410d2..4422d76ee9d151b7a83f9a7d8d9f874eacda4b20 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/params.i (no preprocessing)
+[kernel] Parsing params.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_lem : Valid
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 30017bf15b078ab2665348dee450cf16b66fde5e..67fbb57a51e2d528a8077c99f214a51eeb993c17 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/plet.i (no preprocessing)
+[kernel] Parsing plet.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_GOAL : Valid
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 5f2225e888c8039688ad6f032109704023a8750c..125b85ed5174e692bdc852b36d027d86dbeb1143 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/post_assigns.i (no preprocessing)
+[kernel] Parsing post_assigns.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
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 42883461442bf7cfe6e8ca58e5a3912baf397bed..93440d98a87aabadd1e02f6cccc40363426b1502 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/post_valid.i (no preprocessing)
+[kernel] Parsing post_valid.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 dcaa1de220c10583f6f3ba7868cc1a14e86d7bea..2e2b36878d3e5f9274b92febfa5d9a2927f042f6 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/prenex.i (no preprocessing)
+[kernel] Parsing prenex.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 12 goals scheduled
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 90915c00cf2005f3e6fc62a0cb21910cb94531b2..724f423702b11d463ff5957c6ae6f936e1558ca3 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/region_to_coq.i (no preprocessing)
+[kernel] Parsing region_to_coq.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Warning: native support for coq is deprecated, use tip instead
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 2580c0129be69f18f65f38d88a7180eeb7b2c4cb..c961a5d468de1dc6bdf09be57972f87aef6dd2e0 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
@@ -1,11 +1,11 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/removed.i (no preprocessing)
+[kernel] Parsing removed.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/wp_plugin/removed.i:9: Warning:
+[eva:alarm] removed.i:9: Warning:
signed overflow. assert 1 + i ≤ 2147483647;
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
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 d66e2f2fd319d17876094133fa82c11fb2de4300..5fa488ad8824c3a4945959941a8b5d198c3995c1 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,8 +1,8 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/repeat.c (with preprocessing)
+[kernel] Parsing repeat.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/repeat.c:47: Warning:
+[wp] repeat.c:47: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 47 goals scheduled
[wp] [Qed] Goal typed_master_ensures : Valid
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 b15eec1d8c0f3329246d434eb8f8f479d12f622e..4378c5286a802774782011e5efcf035646661793 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,5 +1,5 @@
# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/wp_plugin/rte.i (no preprocessing)
+[kernel] Parsing rte.i (no preprocessing)
[wp] Running WP plugin...
[rte] annotating function job
[rte] annotating function job2
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 ce5458f78c87634b3be434ba524388d503ccd667..08751dc1962e76436108d5c150fb46acbffc110b 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
-[kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing)
+[kernel] Parsing sequence.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 39 goals scheduled
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 4bda2590b48433fac647442ebaa1d96c71b45ce6..d2806020044b634a1c493759069ee6fe5ebee4ee 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
-[kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing)
+[kernel] Parsing sequence.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 34 goals scheduled
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 9f08e04867c88212456b5f19fc1a3f40e7ba00e8..6a23c1a83b41693e26942bdfb8ea7e4eb24f6353 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Caveat)' -wp-steps 50 [...]
-[kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing)
+[kernel] Parsing sequence.i (no preprocessing)
[wp] Running WP plugin...
[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 e680fd205caf1f853548d7805358939763deccd9..97195231fdf5b44ab23f584f035a8beb8c1298cb 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing)
+[kernel] Parsing stmt.c (with preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal f_exits : Valid (Unreachable)
[wp] [CFG] Goal g_exits : 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 e5ecf9b5e00d8593bc806889fba90904b71c6b37..cc9031fcb59f098af6fb1aa7717aa675b908d1cc 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,5 +1,5 @@
# frama-c -wp -wp-timeout 120 -wp-steps 2500 [...]
-[kernel] Parsing tests/wp_plugin/string_c.c (with preprocessing)
+[kernel] Parsing string_c.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 44 goals scheduled
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 42aa2a20e4fbef7c950217e1b9386a86b2e31385..fca0d689320098ba0d0f6a51e7e1db6f58f5063a 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/struct.i (no preprocessing)
+[kernel] Parsing struct.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 18 goals scheduled
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 15e36ca17c4b10d669412b57f0051f386e9cff61..beb7d0635ebdb032fd508b4625482c767980c5b6 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
@@ -1,12 +1,12 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/struct_hack.i (no preprocessing)
-[kernel] tests/wp_plugin/struct_hack.i:46: Warning:
+[kernel] Parsing struct_hack.i (no preprocessing)
+[kernel] 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] Warning: Missing RTE guards
-[wp] tests/wp_plugin/struct_hack.i:37: Warning:
+[wp] struct_hack.i:37: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_plugin/struct_hack.i:53: Warning:
+[wp] struct_hack.i:53: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 10 goals scheduled
[wp] [Alt-Ergo] Goal typed_f0_loop_invariant_qed_ok_preserved : Valid
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 8fc2d073364afea561fc261a9a71f6f72fd199f7..1f30109b1dfbc06aee348c087507e2ff074cbd4a 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/subset.i (no preprocessing)
+[kernel] Parsing subset.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 7f76d80b00a10d94eb30f412df38843d33541efa..3f4848d627f39303da8eb3c37551b976480e9c78 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/subset_fopen.c (with preprocessing)
+[kernel] Parsing subset_fopen.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
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 a58fda9c10a8b8af8c1d5221276ae445259ef2e6..8c40c5d7ac8b0f5d89682024a25d4a93356f7aeb 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/trig.i (no preprocessing)
+[kernel] Parsing trig.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 1acc6c2f67194ac1cacb71df228693a3ff42ad02..cca078fa79b38e3d18be178e810d435242f7c601 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,8 +1,8 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/unroll.i (no preprocessing)
+[kernel] Parsing unroll.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/unroll.i:20: Warning:
+[wp] unroll.i:20: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
[wp] [Script] Goal typed_unrolled_loop_ensures_zero : Valid
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 6944a089a5680677ce9f2faad5a2eb6608eb7665..ac8bea6cd2303d32f43df9096e237c2ba50c0cb8 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/unsafe-arrays.i (no preprocessing)
+[kernel] Parsing unsafe-arrays.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 4e4af2c1d3de53e290bb2a962a64749a16586809..f5ea71506e349108dfb0029bd9f7d653742a2241 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/unsigned.i (no preprocessing)
+[kernel] Parsing unsigned.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] [Script] Goal typed_lemma_U32 : Unsuccess
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 1af004f7352a7399067955d2a6f532ea402593f8..e7bafef6d0ddb31c0c6b0bfbae553ed91e43a9ab 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/array1.i (no preprocessing)
+[kernel] Parsing array1.i (no preprocessing)
[wp] Running WP plugin...
[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 8a08fc002341f92fc59c3e0bddc74b46aafb47dd..f65e5113a5de004f1735416feae1c6cccf9a2d17 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/array2.i (no preprocessing)
+[kernel] Parsing array2.i (no preprocessing)
[wp] Running WP plugin...
[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 1344cd80f93131f3b3ce5b68df14775600fe5537..8a0eef80a86db86ded3c0259766b6e8dfa11d6a4 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/array3.i (no preprocessing)
+[kernel] Parsing array3.i (no preprocessing)
[wp] Running WP plugin...
[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 cfd2596b0591d1bc89e1a30cb9ac27a197a52ea2..43b02d2fdd5eca9ca26e7690ae3c8efd1c0dcb38 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/array4.i (no preprocessing)
+[kernel] Parsing array4.i (no preprocessing)
[wp] Running WP plugin...
[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 96c8bb9496dc74752ccd83b438b8cca2cc8f27b2..5dde4c62c227399d8568f8137b8e4b57221e8be6 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/array5.i (no preprocessing)
+[kernel] Parsing array5.i (no preprocessing)
[wp] Running WP plugin...
[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 e9b4be282bb2067de102441f7f84bf1a301329ad..87e0d0c26bf0a990fc829a839352f75b8e656f4e 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/array6.i (no preprocessing)
+[kernel] Parsing array6.i (no preprocessing)
[wp] Running WP plugin...
[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 014de0bbb3a906df837b21bab34a69366d353f29..58b7b84d760ce95e3c5d23a2c98b6be7086f2946 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/array7.i (no preprocessing)
+[kernel] Parsing array7.i (no preprocessing)
[wp] Running WP plugin...
[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 c045da519b1923ff0250a10be65fbb19fbbc44e0..ee372986dc5310bb4f6978e2add72844ddf3da6b 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/array8.i (no preprocessing)
+[kernel] Parsing array8.i (no preprocessing)
[wp] Running WP plugin...
[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 524115e64b4234b212eba54058f71db95542f2a2..65aa343de9a1b94acd10ff6274490c5a3f722d8c 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/fb_ADD.i (no preprocessing)
+[kernel] Parsing fb_ADD.i (no preprocessing)
[wp] Running WP plugin...
[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 98b5221f1755b87c0d3552511f029bb8513c6a74..eed91319fd7abab0f314fbbdfd71c1753ae78784 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/fb_SORT.i (no preprocessing)
+[kernel] Parsing fb_SORT.i (no preprocessing)
[wp] Running WP plugin...
[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 7cae27dc0bb5db0195e3dd039165b5036b2f9f7a..ef140ddb0945880bdc5b4a9fe7961a59f61aa854 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/garbled.i (no preprocessing)
+[kernel] Parsing garbled.i (no preprocessing)
[wp] Running WP plugin...
[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 851c520b6845a0e1090004ed8a87e04e687e6a37..514228d38dc3ab6a10dcfa8d33622f0628694515 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/index.i (no preprocessing)
+[kernel] Parsing index.i (no preprocessing)
[wp] Running WP plugin...
[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 bd22d004dbbb42d74264f5af2f37df6819875f8b..2b4866fb08ab090c40ba740c4ccd906303dbc66c 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/matrix.i (no preprocessing)
+[kernel] Parsing matrix.i (no preprocessing)
[wp] Running WP plugin...
[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 f420eeb6427fdbb1ca7a7764ee519a756296b0dd..ffb1d191f763685a760f84611bab0e15f56c7a1f 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/structarray1.i (no preprocessing)
+[kernel] Parsing structarray1.i (no preprocessing)
[wp] Running WP plugin...
[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 47409954b5b88eb0c499797658218f760eecf9b3..7625bb9224d3c4d3945cbc4efb68da60ffe10d52 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/structarray2.i (no preprocessing)
+[kernel] Parsing structarray2.i (no preprocessing)
[wp] Running WP plugin...
[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 1acebc060c044889880df8bffb9b73e6e12e0e65..ecc9c7ec63c066d46c5bf594011263da37558e9f 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/structarray3.i (no preprocessing)
+[kernel] Parsing structarray3.i (no preprocessing)
[wp] Running WP plugin...
[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 ec6b5a2de86270e3dbfc5304c83ce5621c8909fe..f71833e1171a8e563ddc262e66b27fa1d38b1a77 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/structarray4.i (no preprocessing)
+[kernel] Parsing structarray4.i (no preprocessing)
[wp] Running WP plugin...
[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 f736619caac65deed1a4955a8fe1996603c0dc18..ee37192b8778fae5286ec682656d921730952fbe 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_region/swap.i (no preprocessing)
+[kernel] Parsing swap.i (no preprocessing)
[wp] Running WP plugin...
[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 9373264bf9dc25047ecf3a7e64b41b779f82cf97..828f168ec2f355aba506a79cadd00b0962f91f42 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_store/array.i (no preprocessing)
+[kernel] Parsing array.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 8d3b99ea68772209a97b649d3349178c3734ce6a..99a7ed554c4b5846de141dfb494c92564e5b5bed 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_store/natural.i (no preprocessing)
+[kernel] Parsing natural.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 139e0d95e804f6aca5a9002bd87a629369a385fe..2533a1d5041400d0e3903c9ba50330b8b3c25bb7 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_store/nonaliasing.i (no preprocessing)
+[kernel] Parsing nonaliasing.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 8d1a5b9cac94b62e3b028920bf61cd6897007e1a..9ffac3505bda57866d9dabf813a7d887e79f6729 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,5 +1,5 @@
# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_store/nonaliasing.i (no preprocessing)
+[kernel] Parsing nonaliasing.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 705f7dbdd5295e27155cd343fe99868e8a3713e2..175ee82b24147aa4a38cab1438ade3bf3d4cd2f4 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_store/struct.i (no preprocessing)
+[kernel] Parsing struct.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 1fc22002b222f9cfabf273f5b1796664c486a825..799137686930a9c8e499381d87d5d5ca2ee033b8 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_tip/tac_split_quantifiers.i (no preprocessing)
+[kernel] Parsing tac_split_quantifiers.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
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 0d1a283b5f82294ce2f798f83ea9eee83fa89231..f75ed8ad5fe7f376c80b34b30de474e1ba62e951 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
@@ -1,6 +1,6 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/array_initialized.c (with preprocessing)
-[kernel] tests/wp_typed/array_initialized.c:13: Warning:
+[kernel] Parsing array_initialized.c (with preprocessing)
+[kernel] array_initialized.c:13: Warning:
Too many initializers for array g
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
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 0d1a283b5f82294ce2f798f83ea9eee83fa89231..f75ed8ad5fe7f376c80b34b30de474e1ba62e951 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
@@ -1,6 +1,6 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/array_initialized.c (with preprocessing)
-[kernel] tests/wp_typed/array_initialized.c:13: Warning:
+[kernel] Parsing array_initialized.c (with preprocessing)
+[kernel] array_initialized.c:13: Warning:
Too many initializers for array g
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
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 878e590dd1e091c3fe6db642952a77cdd1b9b449..45fd4bf0e5411018494d04b9c3c63fbe4db8e346 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,7 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/avar.i (no preprocessing)
+[kernel] Parsing avar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] tests/wp_typed/avar.i:4: Warning:
+[kernel] avar.i:4: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 1a80a196cf89532c5ad595a5ceedc2ad31dd2182..f96f47cdcd3b055ee8c79c643fdb7b07d8be3719 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,14 +1,14 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/cast_fits.i (no preprocessing)
+[kernel] Parsing cast_fits.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_typed/cast_fits.i:13: Warning:
+[wp] cast_fits.i:13: Warning:
Cast with incompatible pointers types (source: __anonstruct_L2_2*)
(target: sint32*)
-[wp] tests/wp_typed/cast_fits.i:54: Warning:
+[wp] cast_fits.i:54: Warning:
Cast with incompatible pointers types (source: __anonunion_L8_8*)
(target: sint32*)
-[wp] tests/wp_typed/cast_fits.i:60: Warning:
+[wp] cast_fits.i:60: Warning:
Cast with incompatible pointers types (source: sint32*)
(target: __anonunion_L8_8*)
[wp] 8 goals scheduled
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 96bb1c3037c84b0974790f377c051aa0257fd6fa..3316523eaeb81b8ae78f1c21db6ae4b45b3e3a6d 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/frame.i (no preprocessing)
+[kernel] Parsing frame.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 65452ad8fe8dcf8a886ab9f392404f71630df81b..6d550e0e6c72a18991068a6457109d9d4d6104d8 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,7 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/mvar.i (no preprocessing)
+[kernel] Parsing mvar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] tests/wp_typed/mvar.i:14: Warning:
+[kernel] mvar.i:14: Warning:
No code nor implicit assigns clause for function Write, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 b09f19d9e21cd1d22ac3a67730dd7a5b487d9c55..bf090f92058410ee65931150a69346250beb1c56 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/shift_lemma.i (no preprocessing)
+[kernel] Parsing shift_lemma.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
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 a7963a1a6f95d866ce43bb242984b73428ac54c3..483125f2578c3b68946adf09d692cc225cad2a63 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/struct_array_type.i (no preprocessing)
+[kernel] Parsing struct_array_type.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 18546f909a348ac909e1a04f80648b14d3305b68..6b3405cdb27e70a210dcf8301d139bcc3628a5ee 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_alloc.i (no preprocessing)
+[kernel] Parsing unit_alloc.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
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 86359ce6ec2a844ed6a61b3b7b1ff36e8998a6bf..57de44fd76abb78d88db3c569f106b5eafb156ab 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_typed/unit_alloc.i (no preprocessing)
+[kernel] Parsing unit_alloc.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
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 7459d60fcb3a9ff2576f1a64c007140d0205f2df..5c838689f12914c9e16edb03cb53b10e8ec0312c 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_bitwise.c (with preprocessing)
+[kernel] Parsing unit_bitwise.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 61 goals scheduled
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 10406f8c492cb1a2ab30b5aa6196c538c69bbab4..4e42c26ecdc94ceb3ee630300941ba2c4fb0473f 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_bitwise.c (with preprocessing)
+[kernel] Parsing unit_bitwise.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
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 e2091a07708432017ec2a5599e677cb06cab0721..db9cadfc9678a6f80d4af03f0636f8e3bfc4a625 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,7 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_call.i (no preprocessing)
+[kernel] Parsing unit_call.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] tests/wp_typed/unit_call.i:7: Warning:
+[kernel] 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
[wp] 1 goal scheduled
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 c54e6f55894426414495d56cd63c0fe1a8b2e3c1..8bfa5ac6000ca0903dd92d29100a3389678b89bc 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,8 +1,8 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_cast.i (no preprocessing)
+[kernel] Parsing unit_cast.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_typed/unit_cast.i:4: Warning:
+[wp] unit_cast.i:4: Warning:
Cast with incompatible pointers types (source: sint32*) (target: sint8*)
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_assert_OUT : Valid
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 503a254a25f00fd9ae064719d864b8f608a8b112..62c584845135b6317f98dd101ed0d7885d079732 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_cst.i (no preprocessing)
+[kernel] Parsing unit_cst.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 df568124db56b58ad7625bfc83e1d823c194dc6b..65274bde6233dd86829baeded90e6d0d58f1fa43 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
@@ -1,6 +1,6 @@
# frama-c -wp -wp-model 'Typed' [...]
-[kernel] Parsing tests/wp_typed/unit_float.i (no preprocessing)
-[kernel:parser:decimal-float] tests/wp_typed/unit_float.i:21: Warning:
+[kernel] Parsing unit_float.i (no preprocessing)
+[kernel:parser:decimal-float] unit_float.i:21: Warning:
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...
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 71e047a463e1457643a7bfa8f70f0aaef0f6c362..0ed8a513df71316c569bc0a58144bfdf54302ad8 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_hard.i (no preprocessing)
+[kernel] Parsing unit_hard.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 0fc85faf32b648767159621cd29f07da187565d4..e1e6ce212b47b6c79df6366ce5836e9d64d02e43 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_ite.i (no preprocessing)
+[kernel] Parsing unit_ite.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
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 a255ecbfec34a8abcb606596793671d050dd77f4..050fa05259a4c593b12fbb19622fe4a630f93544 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_labels.i (no preprocessing)
+[kernel] Parsing unit_labels.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 a863510b6f644cac7b250b7ea486e3389ba1fc87..9f0f8042b987e52a4a6d42a2698d491a9d1d9ec2 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_lemma.i (no preprocessing)
+[kernel] Parsing unit_lemma.i (no preprocessing)
[wp] Running WP plugin...
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_Foo : 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 137ed92886e4824874d4c3c9d6b161348f360a5e..47f5d6597bd044fee352620f445256aa504b8f63 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_local.c (with preprocessing)
+[kernel] Parsing unit_local.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 183c93047804be2c05c42fd6634638369e847318..8a6a8ae7efc1670f58366a92af8cc539af79329e 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Raw)' [...]
-[kernel] Parsing tests/wp_typed/unit_local.c (with preprocessing)
+[kernel] Parsing unit_local.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 80e267199ec95e38e3342d58984e767e822caed7..2729ba2028b9b8268232821e2e9f5db8344426bd 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,8 +1,8 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_loopscope.i (no preprocessing)
+[kernel] Parsing unit_loopscope.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_typed/unit_loopscope.i:14: Warning:
+[wp] unit_loopscope.i:14: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_f_loop_invariant_preserved : Valid
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 4417ddd127acc3f894426f6829b8d8b4766afaf2..2d96ea195b78348a5e8a5988269de806023f6071 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,8 +1,8 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_typed/unit_loopscope.i (no preprocessing)
+[kernel] Parsing unit_loopscope.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_typed/unit_loopscope.i:14: Warning:
+[wp] unit_loopscope.i:14: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_ref_f_loop_invariant_preserved : Valid
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 f48df3d43f601321a6b715fc4a9d10273b2107bc..bf852b0844c2ebc91117caf6d96ced85201f2c0f 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_matrix.i (no preprocessing)
+[kernel] Parsing unit_matrix.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
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 85998f3551920e8f3c059c0b434c9865eb6f39d0..f894ee5abeeb1e15bcae4840798ecd90cba1db3a 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_string.i (no preprocessing)
+[kernel] Parsing unit_string.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 73c76c092af6f8fd3ab0fc93f3f7af41fb7e4d83..049e72d939f1c8eb551d5acb21c7b40b1c2c8084 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/unit_tset.i (no preprocessing)
+[kernel] Parsing unit_tset.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
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 e0a7b4b82a7b3d5d7f80cfd6978774bc1b17dd1b..adb01c5d3ab87c27ccdf34f5b7717cdf85f016b9 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_typed/user_bitwise.i (no preprocessing)
+[kernel] Parsing user_bitwise.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 12 goals scheduled
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 803894a6a5d9c534aebcc30db5e4d8a0a09b6902..d2089cbf7cc36c67a4381d2aa92dd51e20fb1c74 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_typed/user_bitwise.i (no preprocessing)
+[kernel] Parsing user_bitwise.i (no preprocessing)
[wp] Running WP plugin...
[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 a6406197d72b3779c404adeb341ce848c0e7f9cd..66c3467dac6402c11221309cd39da4377c2b1399 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/user_collect.i (no preprocessing)
+[kernel] Parsing user_collect.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 32 goals scheduled
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 3945dd8f3a65ec11fffa0303fe8300c4c4e63a66..ddb2d9cf8eecc3c32bc23a338aa3146401046c44 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
+[kernel] Parsing user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal init_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t1_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 f9f0f2c219867828a57bba71fbce2fade387cf24..3214d2495341baee832b422cc909323e9e6c8f48 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
+[kernel] Parsing user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal init_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t1_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 41f563dd7bf77dbfd732205c343f841b0bad0caf..61710f4cb7db03100916a8792e860f12e2033276 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
+[kernel] Parsing user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal init_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
index e6c28bf655407f69bf063936bf2860a26d7c671d..58ae426289ceb8e43551fa5bb65fe05c6943b972 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
@@ -1,5 +1,5 @@
# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...]
-[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
+[kernel] Parsing user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
@@ -15,7 +15,7 @@
[wp] Proved goals: 8 / 8
Qed: 4
Alt-Ergo 2.0.0: 4
-[wp] Report 'tests/wp_typed/user_init.i.0.report.json'
+[wp] Report 'user_init.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
init 4 4 (48..60) 8 100%
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 20fdb332cff1128c6e165033300ad73bfea348fc..e23e6bc5d4aff76c266dee07139f818107c37582 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/user_injector.i (no preprocessing)
+[kernel] Parsing user_injector.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 20 goals scheduled
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 93b4fb88899dc8766046ac491738f5ce0f679df6..de2aed2143a8819fa642f3ed08d01a4bb5909063 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_typed/user_injector.i (no preprocessing)
+[kernel] Parsing user_injector.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 16 goals scheduled
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 16e16726067efbf2c05555f8174b25a438697575..303439c8d14682fb72b73fae8a4454377c6728da 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/user_rec.i (no preprocessing)
+[kernel] Parsing user_rec.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 18 goals scheduled
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 48d205c0e686833aab93bed4760f2e6b2b96399a..7ce998fa950fa087f225e2f05f1d2288fad51675 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/user_string.i (no preprocessing)
+[kernel] Parsing user_string.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 13 goals scheduled
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 b02ef572b0c167f0fc0adbda7ddc96eeb1a0002f..3257125abab11b9afed371919432c0c1f69fd9f6 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_typed/user_swap.i (no preprocessing)
+[kernel] Parsing user_swap.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
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 1a4f9fd916dc87ddda1ca6877dad7c9460da89d1..7bafc3fee380c48558dd637ab19ee0e5b5cb2e5f 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing tests/wp_typed/user_swap.i (no preprocessing)
+[kernel] Parsing user_swap.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
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 6c1a2b8821961dcbaf564314c55b39872a1ef6bc..d1e9944cf8bb66c1f1085a1d2716b40e9358e185 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,8 +1,8 @@
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
-[kernel] Parsing tests/wp_usage/caveat2.i (no preprocessing)
+[kernel] Parsing caveat2.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_usage/caveat2.i:22: Warning: Undefined array-size (sint32[])
+[wp] caveat2.i:22: Warning: Undefined array-size (sint32[])
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_caveat_job_ensures_N : Valid
[wp] [Alt-Ergo] Goal typed_caveat_job_ensures_A : Valid
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 050004166a73ac6f66a23eadb0131b5b510a598c..6c4b5a892b5731439e828fb6a96476fc1c17a9c2 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,5 +1,5 @@
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
-[kernel] Parsing tests/wp_usage/caveat_range.i (no preprocessing)
+[kernel] Parsing caveat_range.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 12 goals scheduled
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 1aa3a66475c495f732460268228af5de005e9a00..593b7a3bd52dd3f48bd55b82d311e40ff8397a0c 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_usage/issue-189-bis.i (no preprocessing)
+[kernel] Parsing issue-189-bis.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 30 goals scheduled
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 c2679dccf0ddd1ca3dbebec9e4eb51a652063629..a51a55e4fdf293716eb461ae0a728a45f9337fe1 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,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_usage/issue-189-bis.i (no preprocessing)
+[kernel] Parsing issue-189-bis.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled