From b13f20e6e5650d7639a6530b27c1ba476d6bdfaf Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 19 Oct 2020 17:23:16 +0200
Subject: [PATCH] [Tests] add test config qualif of wp (init)
---
Makefile | 2 +-
src/plugins/wp/tests/test_config_qualif | 3 +-
.../wp/oracle_qualif/cfg_loop.res.oracle | 2 +-
.../tests/wp/oracle_qualif/sharing.res.oracle | 2 +-
.../stmtcompiler_test.res.oracle | 8 ++--
.../stmtcompiler_test_rela.res.oracle | 2 +-
.../wp/oracle_qualif/wp_behav.0.res.oracle | 12 +++---
.../wp/oracle_qualif/wp_behav.1.res.oracle | 6 +--
.../wp/oracle_qualif/wp_call_pre.res.oracle | 6 +--
.../tests/wp/oracle_qualif/wp_eqb.res.oracle | 2 +-
.../wp/oracle_qualif/wp_strategy.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/arith.0.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/arith.1.res.oracle | 2 +-
.../oracle_qualif/assign_array.res.oracle | 2 +-
.../assigned_initialized_memtyped.res.oracle | 2 +-
.../assigned_initialized_memvar.res.oracle | 2 +-
...signed_not_initialized_memtyped.res.oracle | 2 +-
...assigned_not_initialized_memvar.res.oracle | 2 +-
.../oracle_qualif/assigns_path.res.oracle | 2 +-
.../oracle_qualif/assigns_range.0.res.oracle | 2 +-
.../oracle_qualif/assigns_range.1.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/axioms.res.oracle | 2 +-
.../oracle_qualif/base_offset.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/bitwise.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/bitwise2.res.oracle | 2 +-
.../oracle_qualif/block_length.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/boolean.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/checks.res.oracle | 2 +-
.../oracle_qualif/chunk_typing.res.oracle | 2 +-
.../chunk_typing_usable.res.oracle | 2 +-
.../oracle_qualif/classify_float.0.res.oracle | 2 +-
.../oracle_qualif/classify_float.1.res.oracle | 2 +-
.../oracle_qualif/classify_float.2.res.oracle | 2 +-
.../oracle_qualif/classify_float.3.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/cnf.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/ctor.res.oracle | 2 +-
.../oracle_qualif/div_mod.0.res.oracle | 2 +-
.../oracle_qualif/div_mod.1.res.oracle | 2 +-
.../oracle_qualif/div_mod.2.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/e_imply.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/equal.res.oracle | 2 +-
.../oracle_qualif/float_compare.0.res.oracle | 2 +-
.../oracle_qualif/float_compare.1.res.oracle | 2 +-
.../oracle_qualif/float_const.res.oracle | 4 +-
.../oracle_qualif/funvar_inv.res.oracle | 2 +-
.../generalized_checks.res.oracle | 2 +-
.../implicit_enum_cast.res.oracle | 2 +-
.../oracle_qualif/init_label.res.oracle | 4 +-
.../oracle_qualif/init_value.0.res.oracle | 2 +-
.../oracle_qualif/init_value.1.res.oracle | 2 +-
.../oracle_qualif/init_value_mem.res.oracle | 2 +-
.../initialized_memtyped.res.oracle | 2 +-
.../initialized_memvar.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/intbool.res.oracle | 2 +-
.../oracle_qualif/invalid_pointer.res.oracle | 4 +-
.../oracle_qualif/label_escape.0.res.oracle | 2 +-
.../oracle_qualif/label_escape.1.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/logic.res.oracle | 32 ++++++++--------
.../oracle_qualif/looplabels.res.oracle | 2 +-
.../memvar_chunk_typing.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/null.res.oracle | 2 +-
.../oracle_qualif/pointer.0.res.oracle | 6 +--
.../oracle_qualif/pointer.1.res.oracle | 6 +--
.../oracle_qualif/post_result.res.oracle | 2 +-
.../oracle_qualif/precedence.0.res.oracle | 38 +++++++++----------
.../oracle_qualif/precedence.1.res.oracle | 38 +++++++++----------
.../wp_acsl/oracle_qualif/range.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/reads.0.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/reads.1.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/record.0.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/record.1.res.oracle | 2 +-
.../oracle_qualif/simpl_is_type.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/sizeof.res.oracle | 2 +-
.../struct_use_case.0.res.oracle | 2 +-
.../struct_use_case.1.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/tset.res.oracle | 2 +-
.../oracle_qualif/type_guard.0.res.oracle | 2 +-
.../oracle_qualif/type_guard.1.res.oracle | 2 +-
.../oracle_qualif/unit_bit_test.res.oracle | 2 +-
.../oracle_qualif/unit_bool.res.oracle | 2 +-
.../user_def_type_guard.0.res.oracle | 2 +-
.../user_def_type_guard.1.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts0708.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts0843.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts779.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts788.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts986.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts_1174.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts_1176.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts_1360.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts_1462.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts_1586.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts_1588.res.oracle | 6 +--
.../wp_bts/oracle_qualif/bts_1601.res.oracle | 2 +-
.../oracle_qualif/bts_1828.0.res.oracle | 2 +-
.../oracle_qualif/bts_1828.1.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts_2040.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts_2079.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts_2159.res.oracle | 2 +-
.../oracle_qualif/bts_2471.0.res.oracle | 2 +-
.../oracle_qualif/bts_2471.1.res.oracle | 2 +-
.../oracle_qualif/bts_2471.2.res.oracle | 2 +-
.../oracle_qualif/ergo_typecheck.res.oracle | 2 +-
.../wp_bts/oracle_qualif/issue-364.res.oracle | 2 +-
.../oracle_qualif/issue-684-exit.res.oracle | 2 +-
.../oracle_qualif/issue_143.0.res.oracle | 2 +-
.../oracle_qualif/issue_143.1.res.oracle | 2 +-
.../oracle_qualif/issue_143.2.res.oracle | 2 +-
.../oracle_qualif/issue_143.3.res.oracle | 2 +-
.../wp_bts/oracle_qualif/issue_198.res.oracle | 2 +-
.../wp_bts/oracle_qualif/issue_447.res.oracle | 2 +-
.../wp_bts/oracle_qualif/issue_453.res.oracle | 2 +-
.../wp_bts/oracle_qualif/issue_494.res.oracle | 2 +-
.../wp_bts/oracle_qualif/issue_508.res.oracle | 2 +-
.../wp_bts/oracle_qualif/issue_711.res.oracle | 2 +-
.../oracle_qualif/issue_715_a.res.oracle | 4 +-
.../oracle_qualif/issue_715_b.res.oracle | 4 +-
.../wp_bts/oracle_qualif/issue_751.res.oracle | 2 +-
.../wp_bts/oracle_qualif/issue_801.res.oracle | 2 +-
.../wp_bts/oracle_qualif/issue_81.res.oracle | 2 +-
.../wp_bts/oracle_qualif/issue_825.res.oracle | 2 +-
.../wp_bts/oracle_qualif/issue_837.res.oracle | 2 +-
.../wp_bts/oracle_qualif/issue_898.res.oracle | 2 +-
.../oracle_qualif/nupw-bcl-bts1120.res.oracle | 2 +-
...multiplication-without-overflow.res.oracle | 2 +-
.../binary-multiplication.res.oracle | 2 +-
.../wp_gallery/oracle_qualif/find.res.oracle | 2 +-
.../frama_c_exo1_solved.res.oracle | 2 +-
.../frama_c_exo2_solved.res.oracle | 2 +-
.../frama_c_exo3_solved.old.res.oracle | 2 +-
.../frama_c_exo3_solved.old.v2.res.oracle | 2 +-
.../frama_c_exo3_solved.simplified.res.oracle | 2 +-
.../frama_c_hashtbl_solved.res.oracle | 2 +-
.../oracle_qualif/loop-statement.res.oracle | 2 +-
.../alias_assigns_hypotheses.res.oracle | 2 +-
.../wp_hoare/oracle_qualif/byref.0.res.oracle | 2 +-
.../wp_hoare/oracle_qualif/byref.1.res.oracle | 2 +-
.../oracle_qualif/dispatch_var.res.oracle | 2 +-
.../oracle_qualif/dispatch_var2.0.res.oracle | 2 +-
.../oracle_qualif/dispatch_var2.1.res.oracle | 2 +-
.../wp_hoare/oracle_qualif/isHoare.res.oracle | 2 +-
.../oracle_qualif/logicarr.res.oracle | 2 +-
.../oracle_qualif/logicref.res.oracle | 2 +-
.../oracle_qualif/logicref_simple.res.oracle | 2 +-
.../oracle_qualif/reference.res.oracle | 2 +-
.../reference_and_struct.res.oracle | 2 +-
.../oracle_qualif/reference_array.res.oracle | 2 +-
.../reference_array_simple.res.oracle | 2 +-
.../oracle_qualif/refguards.res.oracle | 2 +-
.../oracle_qualif/manual.0.res.oracle | 6 +--
.../oracle_qualif/manual.1.res.oracle | 6 +--
.../oracle_qualif/manual.2.res.oracle | 10 ++---
.../wp_plugin/oracle_qualif/abs.0.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/abs.1.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/abs.2.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/asm.res.oracle | 2 +-
.../oracle_qualif/bit_test.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/bool.0.res.oracle | 6 +--
.../wp_plugin/oracle_qualif/bool.res.oracle | 2 +-
.../oracle_qualif/convert.0.res.oracle | 2 +-
.../oracle_qualif/convert.1.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/copy.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/doomed.res.oracle | 6 +--
.../oracle_qualif/doomed_axioms.res.oracle | 8 ++--
.../oracle_qualif/doomed_call.0.res.oracle | 2 +-
.../oracle_qualif/doomed_call.1.res.oracle | 12 +++---
.../oracle_qualif/doomed_call.2.res.oracle | 12 +++---
.../oracle_qualif/doomed_dead.0.res.oracle | 6 +--
.../oracle_qualif/doomed_dead.1.res.oracle | 6 +--
.../oracle_qualif/doomed_loop.res.oracle | 8 ++--
.../oracle_qualif/doomed_report_ko.res.oracle | 8 ++--
.../oracle_qualif/doomed_report_ok.res.oracle | 2 +-
.../oracle_qualif/doomed_unroll.res.oracle | 4 +-
.../oracle_qualif/dynamic.res.oracle | 4 +-
.../oracle_qualif/fallback.res.oracle | 2 +-
.../oracle_qualif/flash.0.res.oracle | 2 +-
.../oracle_qualif/flash.1.res.oracle | 4 +-
.../oracle_qualif/flash.2.res.oracle | 2 +-
.../oracle_qualif/float_format.0.res.oracle | 4 +-
.../oracle_qualif/float_format.1.res.oracle | 4 +-
.../oracle_qualif/float_format.2.res.oracle | 4 +-
.../oracle_qualif/float_real.0.res.oracle | 4 +-
.../oracle_qualif/float_real.1.res.oracle | 4 +-
.../wp_plugin/oracle_qualif/frame.res.oracle | 2 +-
.../oracle_qualif/ground_real.res.oracle | 2 +-
.../oracle_qualif/inductive.res.oracle | 2 +-
.../oracle_qualif/init_const.res.oracle | 2 +-
.../oracle_qualif/init_const_guard.res.oracle | 2 +-
.../oracle_qualif/init_extern.res.oracle | 4 +-
.../oracle_qualif/init_valid.res.oracle | 2 +-
.../oracle_qualif/initarr.res.oracle | 2 +-
.../oracle_qualif/injector.0.res.oracle | 2 +-
.../oracle_qualif/injector.1.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/loop.res.oracle | 2 +-
.../oracle_qualif/loopcurrent.res.oracle | 4 +-
.../oracle_qualif/loopentry.res.oracle | 4 +-
.../oracle_qualif/loopextra.res.oracle | 6 +--
.../wp_plugin/oracle_qualif/mask.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/math.0.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/math.1.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/math.2.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/math.3.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/model.res.oracle | 4 +-
.../oracle_qualif/no_step_limit.res.oracle | 2 +-
.../oracle_qualif/nosession.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/nowp.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/nth.res.oracle | 2 +-
.../oracle_qualif/overarray.res.oracle | 2 +-
.../oracle_qualif/overassign.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/params.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/plet.res.oracle | 2 +-
.../oracle_qualif/post_assigns.res.oracle | 2 +-
.../oracle_qualif/post_valid.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/prenex.res.oracle | 2 +-
.../oracle_qualif/region_to_coq.res.oracle | 2 +-
.../oracle_qualif/removed.res.oracle | 4 +-
.../wp_plugin/oracle_qualif/repeat.res.oracle | 4 +-
.../wp_plugin/oracle_qualif/rte.res.oracle | 2 +-
.../oracle_qualif/sequence.0.res.oracle | 2 +-
.../oracle_qualif/sequence.1.res.oracle | 2 +-
.../oracle_qualif/sequence.2.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/stmt.res.oracle | 2 +-
.../oracle_qualif/string_c.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/struct.res.oracle | 2 +-
.../oracle_qualif/struct_hack.res.oracle | 8 ++--
.../wp_plugin/oracle_qualif/subset.res.oracle | 2 +-
.../oracle_qualif/subset_fopen.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/trig.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/unroll.res.oracle | 4 +-
.../oracle_qualif/unsafe-arrays.res.oracle | 2 +-
.../oracle_qualif/unsigned.res.oracle | 2 +-
.../wp_region/oracle_qualif/array1.res.oracle | 2 +-
.../wp_region/oracle_qualif/array2.res.oracle | 2 +-
.../wp_region/oracle_qualif/array3.res.oracle | 2 +-
.../wp_region/oracle_qualif/array4.res.oracle | 2 +-
.../wp_region/oracle_qualif/array5.res.oracle | 2 +-
.../wp_region/oracle_qualif/array6.res.oracle | 2 +-
.../wp_region/oracle_qualif/array7.res.oracle | 2 +-
.../wp_region/oracle_qualif/array8.res.oracle | 2 +-
.../wp_region/oracle_qualif/fb_ADD.res.oracle | 2 +-
.../oracle_qualif/fb_SORT.res.oracle | 2 +-
.../oracle_qualif/garbled.res.oracle | 2 +-
.../wp_region/oracle_qualif/index.res.oracle | 2 +-
.../wp_region/oracle_qualif/matrix.res.oracle | 2 +-
.../oracle_qualif/structarray1.res.oracle | 2 +-
.../oracle_qualif/structarray2.res.oracle | 2 +-
.../oracle_qualif/structarray3.res.oracle | 2 +-
.../oracle_qualif/structarray4.res.oracle | 2 +-
.../wp_region/oracle_qualif/swap.res.oracle | 2 +-
.../wp_store/oracle_qualif/array.res.oracle | 2 +-
.../wp_store/oracle_qualif/natural.res.oracle | 2 +-
.../oracle_qualif/nonaliasing.0.res.oracle | 2 +-
.../oracle_qualif/nonaliasing.1.res.oracle | 2 +-
.../wp_store/oracle_qualif/struct.res.oracle | 2 +-
.../tac_split_quantifiers.res.oracle | 2 +-
.../array_initialized.0.res.oracle | 4 +-
.../array_initialized.1.res.oracle | 4 +-
.../wp_typed/oracle_qualif/avar.res.oracle | 4 +-
.../oracle_qualif/cast_fits.res.oracle | 8 ++--
.../wp_typed/oracle_qualif/frame.res.oracle | 2 +-
.../wp_typed/oracle_qualif/mvar.res.oracle | 4 +-
.../oracle_qualif/shift_lemma.res.oracle | 2 +-
.../struct_array_type.res.oracle | 2 +-
.../oracle_qualif/unit_alloc.0.res.oracle | 2 +-
.../oracle_qualif/unit_alloc.1.res.oracle | 2 +-
.../oracle_qualif/unit_bitwise.0.res.oracle | 2 +-
.../oracle_qualif/unit_bitwise.1.res.oracle | 2 +-
.../oracle_qualif/unit_call.res.oracle | 4 +-
.../oracle_qualif/unit_cast.res.oracle | 4 +-
.../oracle_qualif/unit_cst.res.oracle | 2 +-
.../oracle_qualif/unit_float.res.oracle | 4 +-
.../oracle_qualif/unit_hard.res.oracle | 2 +-
.../oracle_qualif/unit_ite.res.oracle | 2 +-
.../oracle_qualif/unit_labels.res.oracle | 2 +-
.../oracle_qualif/unit_lemma.res.oracle | 2 +-
.../oracle_qualif/unit_local.0.res.oracle | 2 +-
.../oracle_qualif/unit_local.1.res.oracle | 2 +-
.../oracle_qualif/unit_loopscope.0.res.oracle | 4 +-
.../oracle_qualif/unit_loopscope.1.res.oracle | 4 +-
.../oracle_qualif/unit_matrix.res.oracle | 2 +-
.../oracle_qualif/unit_string.res.oracle | 2 +-
.../oracle_qualif/unit_tset.res.oracle | 2 +-
.../oracle_qualif/user_bitwise.0.res.oracle | 2 +-
.../oracle_qualif/user_bitwise.1.res.oracle | 2 +-
.../oracle_qualif/user_collect.res.oracle | 2 +-
.../oracle_qualif/user_init.0.res.oracle | 2 +-
.../oracle_qualif/user_init.1.res.oracle | 2 +-
.../oracle_qualif/user_init.2.res.oracle | 2 +-
.../oracle_qualif/user_init.res.oracle | 4 +-
.../oracle_qualif/user_injector.0.res.oracle | 2 +-
.../oracle_qualif/user_injector.1.res.oracle | 2 +-
.../oracle_qualif/user_rec.res.oracle | 2 +-
.../oracle_qualif/user_string.res.oracle | 2 +-
.../oracle_qualif/user_swap.0.res.oracle | 2 +-
.../oracle_qualif/user_swap.1.res.oracle | 2 +-
.../wp_usage/oracle_qualif/caveat2.res.oracle | 4 +-
.../oracle_qualif/caveat_range.res.oracle | 2 +-
.../oracle_qualif/issue-189-bis.0.res.oracle | 2 +-
.../oracle_qualif/issue-189-bis.1.res.oracle | 2 +-
299 files changed, 443 insertions(+), 442 deletions(-)
diff --git a/Makefile b/Makefile
index a001d3f0bc9..dd01490e9a8 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 478b7b10b1e..6883d9ff47b 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 813798a56de..4ad9b8f4400 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 94689205688..a074e6a554d 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 6e1e0c0d7c3..a8d80dc000e 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 85e1744ce20..4f68808ea91 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 faa679c9669..123cb832ada 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 5d374947a3c..836c313e00d 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 bad25e7802e..d31f94ae8d4 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 11c277d30e4..e7aa87478b2 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 90bb89816b2..4ec3f9cebef 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 7f14ed8bcd3..6421bb6a228 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 414816fbfb3..ccc1c83ed99 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 09587f786aa..e7fabb1851d 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 660872093ac..29ca6a4c21b 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 bdd6cac2653..9c9d392ccec 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 183c0c59b68..4b34e4e7ebc 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 e5a1208fc8f..b7400e96ca7 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 180d946c317..6ff8f9301d1 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 3cbb5dfd2f1..be1fcea95ac 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 18f62e7ca9b..8e75f33c163 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 f2b749cff0c..2e6f0226f8a 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 05b7c9c11f2..44e1c94ba9b 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 a91b7a0149b..2f2067dfc3a 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 df621b7dc0c..dc9160a870f 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 41e65885935..ea8709779a5 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 339f025ca51..48e6e69aca4 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 af1378e391d..7eda1878452 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 48e98d4fa14..43511c2b77f 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 01ceab39f72..d076d76ed0c 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 9d414c889b3..e5e152aa2a0 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 e4946583721..efbf0e0a5e9 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 4da1cb298a6..8d89bf6103e 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 6f5af142a49..d56892bed73 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 9ecfe8363f1..2631afd542b 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 8aa8444599f..eaecc9714e5 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 94777d12bef..8abf0f34df3 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 94777d12bef..8abf0f34df3 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 65c66c6e2b9..e0f1fa19f1b 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 1f2b15cef67..163a8786402 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 950c758b70c..bc4d3a27e1a 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 0bf84826947..9ba561787d4 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 27675ba0b68..6d1b078148d 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 ff8fe2744f8..3362c14fd99 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 538b5fb67c2..232ed2e60fe 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 ee38ba79727..f4f1b7e3145 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 1d332c3eba2..7be55226988 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 e48f553e294..42a2712a517 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 d6bc501d6c9..dfbed47d774 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 3d74eca2ac3..96e1fe244e4 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 3cf52a8c985..4d2e5f794dd 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 88684268b9c..34e09776f72 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 fa2acc12292..ffb39abe02f 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 8bf8b806834..b1ebccde248 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 089501d0a3a..3fd3eaad360 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 f71b1ba16e1..f4a753164c5 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 fa9e50b10c4..9ed64cb24ee 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 7c60acbc6bc..0fabb9c0991 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 c7494eb3cc7..3c5f14b5586 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 b6dab655323..dc3afd8b0ce 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 1f8e9e47349..57936c31ef4 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 9e0fd3122c6..2e058d9e213 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 5e0172dd87d..ac454864f98 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 d2eb8110c95..0b383ccbb58 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 24278f6c3aa..7fcb2ffab9d 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 1aa717f83fe..d08db8de9fe 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 4d389265cd8..ec9aaa9da55 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 119c06c6c1d..5bc26fcefec 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 213fdec4cb2..d7762f73d15 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 aafa831a5d6..a12022bdc95 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 9ee1634559a..cf42c84adc3 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 514d6f40bcb..64ff3d3d62f 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 5eebd01bb77..22981e00257 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 3b8c905ab63..1efc688a87a 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 f43f461d6c1..8ac28e497ac 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 bad7bc16a7c..678ead75a09 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 d891a566292..171329197f0 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 6cd53f6a5bb..f3b30166b51 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 e1fcca70b0a..7d027492563 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 6d9d902295d..2d38dce7159 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 022b0364fa9..421d5032376 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 0368f3b6126..0b69f7daf85 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 15fb0108e37..249f9cac609 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 fbd210f679c..dc3a0c6f89d 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 7f1e9b6e40f..dbb98c6df14 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 07263eaba24..2554eb42731 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 8d3d1c250bf..0ef4130fb85 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 2cdd4e30969..d9a23912c01 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 e3b5535c1cb..e8fdfc5b1a2 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 0d96c29ae0c..5072e7c6182 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 c34b04935c1..53303432f91 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 5d88cb99d2c..326de6e3cf4 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 4b070090eaa..5e2c4f9562f 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 86708cc7d79..c27e58cfd85 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 91203bd8a7c..2ad49d15f3e 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 e5edde37e9b..45b60a0df05 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 c47673e6b51..a407bf2ca06 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 6f837f71940..cb6c2c3d0f1 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 c02dc9c178f..786136c4a21 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 99642408d02..7aee840f3b3 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 ffb3913bc38..725a63572bd 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 daef8736024..8d031ef0aec 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 abf5b969263..6f05d1615c3 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 ea1d384da71..41b0c6bc783 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 be5d63c71f6..8792b49802b 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 9d615ddd682..ae88c968f4f 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 08841f4f3a5..dbc3692bd3d 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 9d615ddd682..ae88c968f4f 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 376255d0dcb..0d5c8468bef 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 19ffd064dfc..ca918c67e92 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 df5e033c97c..819ed2e218d 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 c4d33cc9b69..19339169673 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 437f33f00c3..ac23b5b748d 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 f5c735d0395..75201f17f42 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 87633b0ea70..9a296ca593e 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 2ab4a1454a9..f9c7a0b4763 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 694a10a84e8..301704e67cd 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 6fc62ce363b..69f63c6e1c9 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 455278246bd..586d8294e15 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 30935254772..bfa4234e9e1 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 2b809a025c2..da5dce9d62d 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 64c3d264d8c..4d1f4710759 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 9e1e9bcdbea..ca195b3e2f0 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 164271bc40a..d443e190ef6 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 2bf3e0ea994..8b3b8ce8f5b 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 c0a3091f89c..374c185811e 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 a081d0c388b..0760f8c1ed9 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 06ee2377636..4b982f51859 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 1780ec5c89a..d3b25a86812 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 e75ffe7ec64..5795b95d8a2 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 7672a505bc9..fcd4c52bc00 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 72409b7f36c..e2cf934a567 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 b9066d9921a..c99172a223b 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 a86dae9951b..940355bf8dd 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 33a25d793ff..0c71166950c 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 0b6ce2d0287..2ee1cf41475 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 48e1936e195..5018eadab7e 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 d97c3812bd6..300ffa2c96e 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 b5878139820..774ebc54b57 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 7a50ede52eb..250357cf24a 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 04d5a4f2629..eca3be2dd3b 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 efe1f7fdd17..03796d3e416 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 1c127a17545..273fdfb6090 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 061f51954ca..fab483750f3 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 81897c8db12..4a8b2e9e232 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 9da7484d4d2..65ceafb3356 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 5fa325b9170..aa93fe826b9 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 b5390221da4..f0b5d3dee65 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 02a4bffe2c4..0dcc419ece0 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 213ee06d29f..9cf58bd601e 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 4f1030ab270..fb13236dbf6 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 16973c988df..15ac0f70d86 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 16adfa4946a..de73a52c63e 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 3c71816dbbf..146552b7f55 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 d5a8298ccca..34c366ca1cf 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 344e6b07847..31c221bc349 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 fef95834e2e..c99721def5a 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 b908bc8578a..38370a03818 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 dac2be58e75..d72ac023e65 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 c58a574b23e..e0b8fc01010 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 e920dbe1256..7bd9172a019 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 097475c27fe..e0dfdd31412 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 06068093e7e..668ba7d83d9 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 dfc863b89cd..c455b41304a 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 b1a5c4a4fbc..771195e0c0a 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 130e2f527e0..cddd70df9fb 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 cfbb11197d4..23c3c026e3f 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 0b349526c40..4efceed332f 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 fd8fae82478..2019d6f5586 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 6cbe64cf0f1..ea9a729fb71 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 4a65820f41c..fa0963a210e 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 c578928320d..51405b44115 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 9f20f169f87..e01d87f027b 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 9144906c8da..478700185e2 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 4028fd0e199..933a85f90f2 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 0d5f90a7526..e7deb6e2aa5 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 a01eeba9e85..867c987d611 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 a87892007ee..09997a7fac3 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 5ba66e74bab..035a7253a87 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 0423017c2be..0b38dce72ac 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 fcad25a085a..876b56b73ef 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 265dcf74630..b9e76a083eb 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 a42394bed4b..c7bb7c5f628 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 1d9ae90802a..faf78acad99 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 a875c26ce74..e5e1c28c161 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 6d7143512ed..6ba6b85a7b8 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 4389c814aec..a408ed5a7aa 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 2a606446dc5..b0c49e258b1 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 bbc0f9b1738..ff210a2b5b2 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 3f9234d02bd..c3a20d407b6 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 1607fa27193..b6af203f6ca 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 65ebd21fce6..69677093255 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 8730d221d29..fd35b184958 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 602235b4e17..b489f684f7c 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 75c868bd36a..24b26ed0544 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 f62dda1b35e..3f503a108e3 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 111bb4a02c0..102c14a3aaa 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 a212cb8779f..9b679add500 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 4af858324c1..33c44e4df37 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 40753d2a146..773a5245836 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 ffc737646cc..69ac94a8689 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 81ba2360317..d0872807ed5 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 9a0ca708378..ff97bc71c53 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 4feaeefdada..2ad3c977064 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 d56af67a507..f62cd996de8 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 f11f92c390e..963e5d8a099 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 57c1c46213f..68fe97d6e4f 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 6daeab38c98..a118a81cac6 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 5bfb2cf3e34..b80b06514e7 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 f5af22f7014..4422d76ee9d 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 30017bf15b0..67fbb57a51e 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 5f2225e888c..125b85ed517 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 42883461442..93440d98a87 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 dcaa1de220c..2e2b36878d3 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 90915c00cf2..724f423702b 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 2580c0129be..c961a5d468d 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 d66e2f2fd31..5fa488ad882 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 b15eec1d8c0..4378c5286a8 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 ce5458f78c8..08751dc1962 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 4bda2590b48..d2806020044 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 9f08e04867c..6a23c1a83b4 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 e680fd205ca..97195231fdf 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 e5ecf9b5e00..cc9031fcb59 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 42aa2a20e4f..fca0d689320 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 15e36ca17c4..beb7d0635eb 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 8fc2d073364..1f30109b1df 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 7f76d80b00a..3f4848d627f 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 a58fda9c10a..8c40c5d7ac8 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 1acc6c2f671..cca078fa79b 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 6944a089a56..ac8bea6cd23 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 4e4af2c1d3d..f5ea71506e3 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 1af004f7352..e7bafef6d0d 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 8a08fc00234..f65e5113a5d 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 1344cd80f93..8a0eef80a86 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 cfd2596b059..43b02d2fdd5 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 96c8bb9496d..5dde4c62c22 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 e9b4be282bb..87e0d0c26bf 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 014de0bbb3a..58b7b84d760 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 c045da519b1..ee372986dc5 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 524115e64b4..65aa343de9a 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 98b5221f175..eed91319fd7 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 7cae27dc0bb..ef140ddb094 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 851c520b684..514228d38dc 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 bd22d004dbb..2b4866fb08a 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 f420eeb6427..ffb1d191f76 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 47409954b5b..7625bb9224d 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 1acebc060c0..ecc9c7ec63c 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 ec6b5a2de86..f71833e1171 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 f736619caac..ee37192b877 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 9373264bf9d..828f168ec2f 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 8d3b99ea687..99a7ed554c4 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 139e0d95e80..2533a1d5041 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 8d1a5b9cac9..9ffac3505bd 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 705f7dbdd52..175ee82b241 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 1fc22002b22..79913768693 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 0d1a283b5f8..f75ed8ad5fe 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 0d1a283b5f8..f75ed8ad5fe 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 878e590dd1e..45fd4bf0e54 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 1a80a196cf8..f96f47cdcd3 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 96bb1c3037c..3316523eaeb 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 65452ad8fe8..6d550e0e6c7 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 b09f19d9e21..bf090f92058 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 a7963a1a6f9..483125f2578 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 18546f909a3..6b3405cdb27 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 86359ce6ec2..57de44fd76a 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 7459d60fcb3..5c838689f12 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 10406f8c492..4e42c26ecdc 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 e2091a07708..db9cadfc967 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 c54e6f55894..8bfa5ac6000 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 503a254a25f..62c58484513 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 df568124db5..65274bde623 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 71e047a463e..0ed8a513df7 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 0fc85faf32b..e1e6ce212b4 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 a255ecbfec3..050fa05259a 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 a863510b6f6..9f0f8042b98 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 137ed92886e..47f5d6597bd 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 183c9304780..8a6a8ae7efc 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 80e267199ec..2729ba2028b 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 4417ddd127a..2d96ea195b7 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 f48df3d43f6..bf852b0844c 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 85998f35519..f894ee5abee 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 73c76c092af..049e72d939f 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 e0a7b4b82a7..adb01c5d3ab 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 803894a6a5d..d2089cbf7cc 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 a6406197d72..66c3467dac6 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 3945dd8f3a6..ddb2d9cf8ee 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 f9f0f2c2198..3214d249534 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 41f563dd7bf..61710f4cb7d 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 e6c28bf6554..58ae426289c 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 20fdb332cff..e23e6bc5d4a 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 93b4fb88899..de2aed2143a 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 16e16726067..303439c8d14 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 48d205c0e68..7ce998fa950 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 b02ef572b0c..3257125abab 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 1a4f9fd916d..7bafc3fee38 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 6c1a2b88219..d1e9944cf8b 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 050004166a7..6c4b5a892b5 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 1aa3a66475c..593b7a3bd52 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 c2679dccf0d..a51a55e4fdf 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
--
GitLab