diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 879a964f59895cbeb3676562e8b220d276da0b21..797713750dceed22cddee7e68d8536579bbfcec9 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -596,7 +596,6 @@ type config =
 let default_macros () =
   let l = [
     "frama-c", !toplevel_path;
-    "PTEST_MAKE_MODULE", "make -s"
   ] in
   Macros.add_list l Macros.empty
 
@@ -1007,7 +1006,8 @@ let basic_command_string =
             (Macros.get "PTEST_LOAD_MODULES" macros) in
         let opt_pre = Macros.expand macros !additional_options_pre in
         let opt_post = Macros.expand macros !additional_options in
-        "-check " ^ opt_modules ^ " " ^ opt_pre ^ " " ^ options ^ " " ^ opt_post
+        let opt_plugin = String.concat " " (List.map (Printf.sprintf "-load-module %s") command.plugins) in
+        String.concat " " ["-check -no-autoload-plugins";opt_plugin;opt_modules;opt_pre;options;opt_post]
       end else options
     in
     let options = if !use_byte then opt_to_byte_options options else options in
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 06ec07489dc851480fc9b9964637474f4ba26b4c..eb6788d998dbc149e961930f96b3cc9a69bf3add 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -21,6 +21,7 @@
 (**************************************************************************)
 
 module CamlString = String
+module FramacFilepath = Filepath
 
 let empty_string = ""
 
@@ -322,12 +323,13 @@ struct
         end)
 
     let mk_dir d =
+      let d' = FramacFilepath.Normalized.of_string d in
       try
         Extlib.mkdir ~parents:true d 0o755;
-        L.warning "creating %s directory `%s'" O.option_name d;
+        L.warning "creating %s directory `%a'" O.option_name FramacFilepath.Normalized.pretty d';
         d
       with Unix.Unix_error _ ->
-        L.abort "cannot create %s directory `%s'" O.option_name d
+        L.abort "cannot create %s directory `%a'" O.option_name FramacFilepath.Normalized.pretty d'
 
     let set filepath = Dir_name.set filepath
     let get () = Dir_name.get ()
diff --git a/src/plugins/constant_propagation/dune b/src/plugins/constant_propagation/dune
index 4ba43a8084d2acb99ada34fbed9be6be27ddd605..0d5e5e25cb3ef41e641ffbf0ca1f94ecc90b3a96 100644
--- a/src/plugins/constant_propagation/dune
+++ b/src/plugins/constant_propagation/dune
@@ -1,5 +1,5 @@
 ( library
-  (name constant_propagation)
+  (name Constant_Propagation)
   (public_name frama-c-constant_propagation.core)
   (flags -open Frama_c_kernel)
   (libraries frama-c.kernel)
diff --git a/tests/builtins/alloc.c b/tests/builtins/alloc.c
index 36f4a7c0333c46cbd473e24fd4022abf9c670fa5..a12737dae2d09223650a18ab0f048716e04e6e0e 100644
--- a/tests/builtins/alloc.c
+++ b/tests/builtins/alloc.c
@@ -5,7 +5,7 @@
 */
 
 
-#include "share/libc/stdlib.c"
+#include "stdlib.c"
 
 int *p,*q,*r,a,b;
 char *t,*u,*v;
diff --git a/tests/builtins/from_result.c b/tests/builtins/from_result.c
index 89e1f89ae0d5a0a1eab68b623367bad8f9dcccb1..e38ba72eb1cb450f66f32242da7b55cf7921ecac 100644
--- a/tests/builtins/from_result.c
+++ b/tests/builtins/from_result.c
@@ -2,7 +2,7 @@
    OPT:  @EVA_CONFIG@ -eva-alloc-builtin fresh -deps -journal-disable
 */
 
-#include "../../share/libc/stdlib.c"
+#include "stdlib.c"
 
 struct T { int a; int b; };
 
diff --git a/tests/builtins/malloc_individual.c b/tests/builtins/malloc_individual.c
index 790ffba5e5b8e51afd50bc2b27c2eff238af28bc..bf5218700c9449bf9952365cb7f91c1ea1dcd839 100644
--- a/tests/builtins/malloc_individual.c
+++ b/tests/builtins/malloc_individual.c
@@ -2,7 +2,7 @@
    STDOPT: #"-eva-alloc-builtin fresh"
 */
 
-#include "share/libc/stdlib.c"
+#include "stdlib.c"
 
 int *p;
 int A,B,C;
diff --git a/tests/constant_propagation/test_config b/tests/constant_propagation/test_config
index 850779adb25d797c03ebc59655d31bec1c50cadf..77b08230a76f7ed9d0723cabb9208c876b411c97 100644
--- a/tests/constant_propagation/test_config
+++ b/tests/constant_propagation/test_config
@@ -1 +1,2 @@
+PLUGIN: constant_propagation
 OPT: -journal-disable -scf @EVA_OPTIONS@
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index 2e8031e2e2a877ba0f4a9a4dd8403dac10491567..268a1ad85306a893482731cd46134247b4fda956 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,4 +1,5 @@
 /* run.config
+   PLUGIN: sparecode
    CMXS: @PTEST_NAME@
    EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -load-module %{dep:@PTEST_NAME@.cmxs} -journal-enable -journal-name result/intra_journal.ml @PTEST_DIR@/@PTEST_NAME@.i > /dev/null 2> /dev/null
    CMD: @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs}
diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c
index 2fa988b1e5dc0edf41ab46dd4743b4a77b728a36..8c2b1421bfd11b12baee477e43280c7dcec33d67 100644
--- a/tests/libc/coverage.c
+++ b/tests/libc/coverage.c
@@ -1,5 +1,6 @@
 /* run.config*
-   OPT: -eva-no-builtins-auto @EVA_OPTIONS@ share/libc/string.c -eva -slevel 6 -metrics-eva-cover -then -metrics-libc
+   DEPS: ../../share/libc/string.c
+   OPT: -eva-no-builtins-auto @EVA_OPTIONS@ ../../share/libc/string.c -eva -slevel 6 -metrics-eva-cover -then -metrics-libc
 */
 
 #include "string.h"
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index f4fb5d0a12650f6b58d6104aacf9d06cea8f9b95..0a73ba18d49fc63d903d503cb53eb47f6f334ad4 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -22,7 +22,7 @@
 #define _POSIX_C_SOURCE 200112L
 #define _GNU_SOURCE 1
 
-#include "share/libc/__fc_runtime.c"
+#include "__fc_runtime.c"
 
 #include "alloca.h"
 #include "arpa/inet.h"
diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c
index 69ea8ad364922e00488a4a0c3c66fec0fbe0d032..37647e76af9d0db77fbb02015e06d9da1bde813c 100644
--- a/tests/libc/runtime.c
+++ b/tests/libc/runtime.c
@@ -1,6 +1,7 @@
 /* run.config*
    COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
-   CMD: gcc -D__FC_MACHDEP_X86_64 share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null
+   DEPS: ../../share/libc/__fc_runtime.c
+   CMD: gcc -D__FC_MACHDEP_X86_64 ../../share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null
    OPT:
  */
 
diff --git a/tests/libc/string_c_generic.c b/tests/libc/string_c_generic.c
index 9168f43d7369f9d476d037a417f24a713326f6c4..d960a9b44fc3f2c0f3253fbec8b2eb321f1bb96b 100644
--- a/tests/libc/string_c_generic.c
+++ b/tests/libc/string_c_generic.c
@@ -1,5 +1,6 @@
 /* run.config
-   STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-includeshare/libc/string.c -slevel-function strcpy:20,strncpy:5,strcmp:6,strchr:20,strrchr:20,strncat:4,memset:32,strlen:20,memcmp:8 -eva-no-skip-stdlib-specs"
+   DEPS: ../../share/libc/string.c
+   STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-include../../share/libc/string.c -slevel-function strcpy:20,strncpy:5,strcmp:6,strchr:20,strrchr:20,strncat:4,memset:32,strlen:20,memcmp:8 -eva-no-skip-stdlib-specs"
 */
 /* This file has been adapted from libc-test, which is licensed under the
    following standard MIT license:
diff --git a/tests/libc/string_c_strchr.c b/tests/libc/string_c_strchr.c
index 54ed8fab06ee3065c2a13d88a927732181b67b38..4179b4f27cb504bc1bc4681a9e27d20f0a627dfd 100644
--- a/tests/libc/string_c_strchr.c
+++ b/tests/libc/string_c_strchr.c
@@ -1,5 +1,6 @@
 /* run.config
-   STDOPT: #"-cpp-extra-args=-includeshare/libc/string.c -slevel-function strchr:256,main:256 -eva-slevel-merge-after-loop main -eva-no-builtins-auto -eva-no-skip-stdlib-specs"
+   DEPS: ../../share/libc/string.c
+   STDOPT: #"-cpp-extra-args=-include../../share/libc/string.c -slevel-function strchr:256,main:256 -eva-slevel-merge-after-loop main -eva-no-builtins-auto -eva-no-skip-stdlib-specs"
  */
 /* This file has been adapted from libc-test, which is licensed under the
    following standard MIT license:
diff --git a/tests/libc/string_c_strstr.c b/tests/libc/string_c_strstr.c
index 9f0613b351594afcadd9c41bc092315d666f320e..2bfbbdbe125972c5d18a5b5c70f39cd1adedcd67 100644
--- a/tests/libc/string_c_strstr.c
+++ b/tests/libc/string_c_strstr.c
@@ -1,5 +1,6 @@
 /* run.config
-   STDOPT: #"-cpp-extra-args=-includeshare/libc/string.c -slevel-function strstr:30 -eva-no-skip-stdlib-specs"
+   DEPS: ../../share/libc/string.c
+   STDOPT: #"-cpp-extra-args=-include../../share/libc/string.c -slevel-function strstr:30 -eva-no-skip-stdlib-specs"
  */
 /* This file has been adapted from libc-test, which is licensed under the
    following standard MIT license:
diff --git a/tests/pdg/test_config b/tests/pdg/test_config
index d9d741191d10ade715f1080b42b4a421d0d5e4c1..b5c1a82645ae29e9b9638f25ec44455605e617c8 100644
--- a/tests/pdg/test_config
+++ b/tests/pdg/test_config
@@ -1 +1,2 @@
+PLUGIN: pdg
 OPT: -journal-disable @EVA_OPTIONS@ -pdg-print -pdg-verbose 2
diff --git a/tests/rte/divmod.c b/tests/rte/divmod.c
index 8920e6031b5d6ec0e499e820761caa45754db400..13d9737ece5480dad993959c2eb136eecb831545 100644
--- a/tests/rte/divmod.c
+++ b/tests/rte/divmod.c
@@ -2,7 +2,7 @@
    OPT: -rte -warn-signed-overflow -warn-signed-downcast -print -machdep x86_32 -journal-disable
 */
 
-#include "share/libc/limits.h"
+#include "limits.h"
 
 
 int main() {
diff --git a/tests/rte/divmod_typedef.c b/tests/rte/divmod_typedef.c
index 3fd9e3f6bebfc22865fd21bc529abf5caf18791f..d3c6b330e52951b1c3354e94ea756efdcf1e8d9b 100644
--- a/tests/rte/divmod_typedef.c
+++ b/tests/rte/divmod_typedef.c
@@ -2,7 +2,7 @@
    OPT: -rte -warn-signed-overflow -warn-signed-downcast -print -machdep x86_32 -journal-disable
 */
 
-#include "share/libc/limits.h"
+#include "limits.h"
 
 typedef int tint;
 typedef unsigned int tuint;
diff --git a/tests/saveload/bool.c b/tests/saveload/bool.c
index f0752a78127389c9097ef5217c4b072b100e1c2f..c79e10630fd9d80567c6184e2d4c606064678a04 100644
--- a/tests/saveload/bool.c
+++ b/tests/saveload/bool.c
@@ -5,7 +5,7 @@
  */
 
 #include "stdbool.h"
-#include "share/libc/stdio.h"
+#include "stdio.h"
 
 bool x;
 int y;
diff --git a/tests/slicing/bts1684.i b/tests/slicing/bts1684.i
index 75f95e0c4ea31ba3274ff65fa9fddd7c4032dc79..4bcbd9707135523deabb521ccf8810306ed115c1 100644
--- a/tests/slicing/bts1684.i
+++ b/tests/slicing/bts1684.i
@@ -1,5 +1,5 @@
 /* run.config
-   STDOPT: +"-slice-calls main -journal-enable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i"
+   STDOPT: +"-session .frama-c -slice-calls main -journal-enable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i"
 */
 // one bug about JOURNALIZATION and another one about slicing CALLS TO MAIN function.
 double d1, d2, d3;
diff --git a/tests/slicing/combine.i b/tests/slicing/combine.i
index 6a8df7c51cc1bd203ac45773dee3637aa2d2e1af..678556ebe032d3c15e88bd0742241693a81e24bf 100644
--- a/tests/slicing/combine.i
+++ b/tests/slicing/combine.i
@@ -1,6 +1,6 @@
 /* run.config
    PLUGIN: constant_propagation
-   CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+   CMD: @frama-c@ -load-plugin slicing -load-plugin constant_propagation -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
    OPT: @EVA_OPTIONS@ -deps -journal-disable
 */
 
diff --git a/tests/slicing/dune b/tests/slicing/dune
index d07d404803848c477419f92be097d3ae984b3809..f602968810bdbe5820610b4be3cad73685520368 100644
--- a/tests/slicing/dune
+++ b/tests/slicing/dune
@@ -15,7 +15,7 @@
 (executables
  (names merge adpcm ex_spec_interproc horwitz mark_all_slices min_call select_by_annot select_simple simple_intra_slice slice_no_body switch)
  (modes plugin)
- (modules merge adpcm ex_spec_interproc combine horwitz mark_all_slices min_call select_by_annot select_simple simple_intra_slice slice_no_body switch)
+ (modules merge adpcm ex_spec_interproc horwitz mark_all_slices min_call select_by_annot select_simple simple_intra_slice slice_no_body switch)
  (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel frama-c-slicing.core libSelect libAnim)
  (flags -open Frama_c_kernel)
 )
@@ -25,6 +25,6 @@
  (names combine)
  (modes plugin)
  (modules combine)
- (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel frama-c-slicing.core frama-c-constant-propagation.core libSelect libAnim)
+ (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel frama-c-slicing.core frama-c-constant_propagation.core libSelect libAnim)
  (flags -open Frama_c_kernel)
 )
diff --git a/tests/slicing/ex_spec_interproc.i b/tests/slicing/ex_spec_interproc.i
index 38c8a95b01dc86eaaef470cf7cc60ab25fd05414..e31d5f2bb8206e722d33f8f88ae7c0edf09de0da 100644
--- a/tests/slicing/ex_spec_interproc.i
+++ b/tests/slicing/ex_spec_interproc.i
@@ -1,6 +1,6 @@
 /* run.config
 
-   CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+   CMD: @frama-c@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
    OPT: @EVA_OPTIONS@ -deps -journal-disable
 */
 
diff --git a/tests/slicing/horwitz.i b/tests/slicing/horwitz.i
index 10ec91fffb8670454383458ce29fa09b35706f22..66888cbb0f32f1b2f14930c243cc684ab632935e 100644
--- a/tests/slicing/horwitz.i
+++ b/tests/slicing/horwitz.i
@@ -1,6 +1,6 @@
 /* run.config
 
-   CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+   CMD: @frama-c@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
    OPT: @EVA_OPTIONS@ -deps -slicing-level 0 -journal-disable
 */
 
diff --git a/tests/slicing/mark_all_slices.i b/tests/slicing/mark_all_slices.i
index fd186b11a78f45ee2af6f9b49ebc86158c5f1053..7f9994fc771af96a61015719fe888e69dca64287 100644
--- a/tests/slicing/mark_all_slices.i
+++ b/tests/slicing/mark_all_slices.i
@@ -1,6 +1,6 @@
 /* run.config
 
-   CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+   CMD: @frama-c@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
    OPT: @EVA_OPTIONS@ -deps -slicing-level 3 -no-slice-callers -journal-disable
 */
 int A, B, C, D;
diff --git a/tests/slicing/merge.i b/tests/slicing/merge.i
index 690517f142835685c921472c0d9eb7813db77fa1..d831f24fe1c11e03a8fd8e24774b25cf779f89ee 100644
--- a/tests/slicing/merge.i
+++ b/tests/slicing/merge.i
@@ -1,5 +1,5 @@
 /* run.config
-   CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:libAnim.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+   CMD: @frama-c@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:libAnim.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
    OPT: @EVA_OPTIONS@ -deps -slicing-level 3 -journal-disable
 */
 
diff --git a/tests/slicing/min_call.i b/tests/slicing/min_call.i
index 7078fc13c26abe8b887834bcbcd20f7507280b76..a268f001ff989bd434e1a073ac7e42afc9c83010 100644
--- a/tests/slicing/min_call.i
+++ b/tests/slicing/min_call.i
@@ -1,6 +1,6 @@
 /* run.config
 
-   CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+   CMD: @frama-c@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
    OPT: @EVA_OPTIONS@ -deps -lib-entry -main g -journal-disable -slicing-level 3
 */
 
diff --git a/tests/slicing/oracle/bts1684.res.oracle b/tests/slicing/oracle/bts1684.res.oracle
index 305c7d7c0f76baa66e81a5465893a2d10f55c0e6..96c61a1f0a03fe1b8e8902bb19f2d72568176053 100644
--- a/tests/slicing/oracle/bts1684.res.oracle
+++ b/tests/slicing/oracle/bts1684.res.oracle
@@ -59,5 +59,5 @@ int main(void)
 
 
 [kernel] Parsing ocode_0_bts1684.i (no preprocessing)
-[kernel] Warning: creating session directory `/home/bobot/Sources/frama-c/_build/default/result/.frama-c'
+[kernel] Warning: creating session directory `.frama-c'
 [kernel] writing journal in file `.frama-c/frama_c_journal.ml'.
diff --git a/tests/slicing/oracle/bts336.3.res.oracle b/tests/slicing/oracle/bts336.3.res.oracle
index 3ec5777dbbc97d199debd99753f3d97d3ca14a83..e5747bf075409abbc7e822901ac8b4276355f8c1 100644
--- a/tests/slicing/oracle/bts336.3.res.oracle
+++ b/tests/slicing/oracle/bts336.3.res.oracle
@@ -37,20 +37,6 @@
 [from] entry point:
   \result FROM \nothing
 [from] ====== END OF CALLWISE DEPENDENCIES ======
-[inout] InOut (internal) for function f3:
-  Operational inputs:
-    p; a; b; c
-  Operational inputs on termination:
-    p; a; b; c
-  Sure outputs:
-    \nothing
-[inout] InOut (internal) for function main3:
-  Operational inputs:
-    \nothing
-  Operational inputs on termination:
-    \nothing
-  Sure outputs:
-    a; b; c
 [slicing] slicing requests in progress...
 [slicing] initializing slicing ...
 [slicing] interpreting slicing requests from the command line...
@@ -68,6 +54,20 @@
 [slicing] applying 0 actions...
 [sparecode] remove unused global declarations from project 'Slicing export tmp'
 [sparecode] removed unused global declarations in new project 'Slicing export'
+[inout] InOut (internal) for function f3:
+  Operational inputs:
+    p; a; b; c
+  Operational inputs on termination:
+    p; a; b; c
+  Sure outputs:
+    \nothing
+[inout] InOut (internal) for function main3:
+  Operational inputs:
+    \nothing
+  Operational inputs on termination:
+    \nothing
+  Sure outputs:
+    a; b; c
 /* Generated by Frama-C */
 void f3_slice_1(int *p)
 {
diff --git a/tests/slicing/oracle/select_by_annot.1.res.oracle b/tests/slicing/oracle/select_by_annot.1.res.oracle
index f50b98ea8fd3c8bc9210aaa2f57c4bd18b6c536d..c0f3575f5dc322dc8ddc849af89fecdd2f29787c 100644
--- a/tests/slicing/oracle/select_by_annot.1.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.1.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -176,4 +172,4 @@ void main(void)
 }
 
 
-[kernel] Parsing result/ocode_1_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_1_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.10.res.oracle b/tests/slicing/oracle/select_by_annot.10.res.oracle
index 9cb53dcddf20e2d5a9f204326317603735763142..c30f26887f6c5c0f036094807aed8fdbd49a114e 100644
--- a/tests/slicing/oracle/select_by_annot.10.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.10.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -182,4 +178,4 @@ void f7_slice_1(int cond)
 }
 
 
-[kernel] Parsing result/ocode_10_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_10_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.11.res.oracle b/tests/slicing/oracle/select_by_annot.11.res.oracle
index 88a16c2a6433f3edac23d79b286bc442bafa1573..5b27209920b895c89f8c23bb3135d9795246fff3 100644
--- a/tests/slicing/oracle/select_by_annot.11.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.11.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -174,4 +170,4 @@ void f8_slice_1(int cond)
 }
 
 
-[kernel] Parsing result/ocode_11_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_11_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.12.res.oracle b/tests/slicing/oracle/select_by_annot.12.res.oracle
index 43b2000555a88e6ee59f8e2bbf475913668b5ae8..0c6fe54f4cf7193a2ad7426653f3d44ee3dd95f9 100644
--- a/tests/slicing/oracle/select_by_annot.12.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.12.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -181,4 +177,4 @@ void f8_slice_1(int cond)
 }
 
 
-[kernel] Parsing result/ocode_12_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_12_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.13.res.oracle b/tests/slicing/oracle/select_by_annot.13.res.oracle
index e0fe78aed78ed7f54c8c459a315fae4ae58a4515..8f680bd8056d3f27317815d56659cba58465bbcd 100644
--- a/tests/slicing/oracle/select_by_annot.13.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.13.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -180,4 +176,4 @@ void f8_slice_1(int cond)
 }
 
 
-[kernel] Parsing result/ocode_13_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_13_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.14.res.oracle b/tests/slicing/oracle/select_by_annot.14.res.oracle
index 15ddc697da21379b56eaf456fc570dd9fc1ddf47..69d8673daf166031a605627daf7ea23bf6e550b7 100644
--- a/tests/slicing/oracle/select_by_annot.14.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.14.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -173,4 +169,4 @@ void f9_slice_1(int c1, int c2)
 }
 
 
-[kernel] Parsing result/ocode_14_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_14_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.2.res.oracle b/tests/slicing/oracle/select_by_annot.2.res.oracle
index 8fbdf85664008ebcc11d513649e771199db9fa1f..2447ad2d3380583eb6259cbc192eb559dc8606f5 100644
--- a/tests/slicing/oracle/select_by_annot.2.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.2.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -172,4 +168,4 @@ void main(void)
 }
 
 
-[kernel] Parsing result/ocode_2_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_2_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.3.res.oracle b/tests/slicing/oracle/select_by_annot.3.res.oracle
index cdb1a6cc2c06409105f0fe722f602d676c5f0cf4..25a50f5cd59edd247f74833690d9f3bbb92a43b2 100644
--- a/tests/slicing/oracle/select_by_annot.3.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.3.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -175,4 +171,4 @@ void modifS_slice_1(int a)
 }
 
 
-[kernel] Parsing result/ocode_3_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_3_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.4.res.oracle b/tests/slicing/oracle/select_by_annot.4.res.oracle
index 41ac22a88b8741e41c9e86b7fde830da2f8cb472..8d2642c6fa807da28c38c401e1b4c12ba49dbf92 100644
--- a/tests/slicing/oracle/select_by_annot.4.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.4.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -175,4 +171,4 @@ void f1_slice_1(void)
 }
 
 
-[kernel] Parsing result/ocode_4_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_4_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.5.res.oracle b/tests/slicing/oracle/select_by_annot.5.res.oracle
index 954a303d7ef0438a8503700301d22240e353e2b9..165cc861ab72f82a834e850c7a4f33b9433b2fe0 100644
--- a/tests/slicing/oracle/select_by_annot.5.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.5.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -174,4 +170,4 @@ void f2_slice_1(void)
 }
 
 
-[kernel] Parsing result/ocode_5_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_5_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.6.res.oracle b/tests/slicing/oracle/select_by_annot.6.res.oracle
index d476c481b8f29201245ec11d6926af1cbba4c669..fb469fe2139a5a8b7b8bdc417b29db69356e5965 100644
--- a/tests/slicing/oracle/select_by_annot.6.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.6.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -170,4 +166,4 @@ void f3_slice_1(int cond)
 }
 
 
-[kernel] Parsing result/ocode_6_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_6_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.7.res.oracle b/tests/slicing/oracle/select_by_annot.7.res.oracle
index e4910e63167f9998827696049eddfe6716f74edb..540bcb17efb6a9e698444e3b15ea6bb2c7dbf3e4 100644
--- a/tests/slicing/oracle/select_by_annot.7.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.7.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -178,4 +174,4 @@ void f4_slice_1(int cond)
 }
 
 
-[kernel] Parsing result/ocode_7_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_7_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.8.res.oracle b/tests/slicing/oracle/select_by_annot.8.res.oracle
index cff1da9a6ee45ede24ebdb04f3088c3a0a17382d..31a3e7b24478f1607ad9dd209a798ced369857cd 100644
--- a/tests/slicing/oracle/select_by_annot.8.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.8.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -170,4 +166,4 @@ void f5_slice_1(int cond)
 }
 
 
-[kernel] Parsing result/ocode_8_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_8_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.9.res.oracle b/tests/slicing/oracle/select_by_annot.9.res.oracle
index 6c0b33b045b2fe9943610a4867df0be9c9da4002..8140a0c2883108a82fbc579a14c6cd12742f03fd 100644
--- a/tests/slicing/oracle/select_by_annot.9.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.9.res.oracle
@@ -26,14 +26,12 @@
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
   Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
 [eva] Recording results for f1
 [eva] Done for function f1
 [eva] computing for function f2 <- main.
   Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
 [eva] Recording results for f2
 [eva] Done for function f2
 [eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
 [eva] Done for function f7
 [eva] computing for function f8 <- main.
   Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning: 
-  loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning: 
-  assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
 [eva:alarm] select_by_annot.i:104: Warning: 
   signed overflow. assert S.a + 1 ≤ 2147483647;
 [eva] Recording results for f8
@@ -180,4 +176,4 @@ void f6_slice_1(int cond)
 }
 
 
-[kernel] Parsing result/ocode_9_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_9_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/variadic.0.res.oracle b/tests/slicing/oracle/variadic.0.res.oracle
index 75216a2d96ce9d77f99b81c3cf683a25325253a5..5db81403d65099d71df5e71e22f7a50dd33d02a7 100644
--- a/tests/slicing/oracle/variadic.0.res.oracle
+++ b/tests/slicing/oracle/variadic.0.res.oracle
@@ -1,8 +1,70 @@
 [kernel] Parsing variadic.c (with preprocessing)
-[kernel] User Error: failed to run: gcc -E -C -I.  -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/variadic.cf732ce.i' '/home/bobot/Sources/frama-c/_build/default/result/variadic.c'
-  this is possibly due to missing preprocessor flags;
-  consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
-  See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "variadic.c" that has errors. Add '-kernel-msg-key pp'
-  for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[slicing] slicing requests in progress...
+[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] computing for function f1 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37.
+[eva] computing for function lib_f <- f1 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23.
+[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning: 
+  Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] using specification for function lib_f
+[eva] Done for function lib_f
+[eva] Recording results for f1
+[eva] Done for function f1
+[eva] computing for function f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38.
+[eva] computing for function lib_f <- f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] computing for function f3 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39.
+[eva] computing for function lib_f <- f3 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31.
+[eva] Done for function lib_f
+[eva] Recording results for f3
+[eva] Done for function f3
+[eva] computing for function f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40.
+[eva] computing for function lib_f <- f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] Recording results for main
+[eva] done for function main
+[slicing] initializing slicing ...
+[slicing] interpreting slicing requests from the command line...
+[pdg] computing for function f3
+[from] Computing for function lib_f
+[from] Done for function lib_f
+[pdg] done for function f3
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[slicing] exporting project to 'Slicing export'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Slicing export tmp'
+[sparecode] removed unused global declarations in new project 'Slicing export'
+/* Generated by Frama-C */
+int lib_f(int n, void * const *__va_params);
+
+int f3_slice_1(void)
+{
+  int tmp;
+  {
+    void *__va_args[3];
+    tmp = lib_f(3,(void * const *)(__va_args));
+  }
+  return tmp;
+}
+
+
diff --git a/tests/slicing/oracle/variadic.1.res.oracle b/tests/slicing/oracle/variadic.1.res.oracle
index ba6e34a3bc64e1e50306ebef6272d2ffe039f635..d7485ec33c9fc39ac7be2572259d7051dae00c03 100644
--- a/tests/slicing/oracle/variadic.1.res.oracle
+++ b/tests/slicing/oracle/variadic.1.res.oracle
@@ -1,8 +1,67 @@
 [kernel] Parsing variadic.c (with preprocessing)
-[kernel] User Error: failed to run: gcc -E -C -I.  -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/variadic.c65331d.i' '/home/bobot/Sources/frama-c/_build/default/result/variadic.c'
-  this is possibly due to missing preprocessor flags;
-  consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
-  See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "variadic.c" that has errors. Add '-kernel-msg-key pp'
-  for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[slicing] slicing requests in progress...
+[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] computing for function f1 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37.
+[eva] computing for function lib_f <- f1 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23.
+[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning: 
+  Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] using specification for function lib_f
+[eva] Done for function lib_f
+[eva] Recording results for f1
+[eva] Done for function f1
+[eva] computing for function f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38.
+[eva] computing for function lib_f <- f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] computing for function f3 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39.
+[eva] computing for function lib_f <- f3 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31.
+[eva] Done for function lib_f
+[eva] Recording results for f3
+[eva] Done for function f3
+[eva] computing for function f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40.
+[eva] computing for function lib_f <- f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] Recording results for main
+[eva] done for function main
+[slicing] initializing slicing ...
+[slicing] interpreting slicing requests from the command line...
+[pdg] computing for function f3
+[from] Computing for function lib_f
+[from] Done for function lib_f
+[pdg] done for function f3
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[slicing] exporting project to 'Slicing export'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Slicing export tmp'
+[sparecode] removed unused global declarations in new project 'Slicing export'
+/* Generated by Frama-C */
+int lib_f(int n , ...);
+
+int f3_slice_1(int a, int b, int c)
+{
+  int tmp;
+  tmp = lib_f(3,a,b,c);
+  return tmp;
+}
+
+
diff --git a/tests/slicing/oracle/variadic.2.res.oracle b/tests/slicing/oracle/variadic.2.res.oracle
index 967e256337f41b2829b7c3c08e857a5ae20c3ca3..9e85774a6e565cc9b02d9e22bc467e69fb2633cc 100644
--- a/tests/slicing/oracle/variadic.2.res.oracle
+++ b/tests/slicing/oracle/variadic.2.res.oracle
@@ -1,8 +1,84 @@
 [kernel] Parsing variadic.c (with preprocessing)
-[kernel] User Error: failed to run: gcc -E -C -I.  -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/variadic.c329fe5.i' '/home/bobot/Sources/frama-c/_build/default/result/variadic.c'
-  this is possibly due to missing preprocessor flags;
-  consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
-  See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "variadic.c" that has errors. Add '-kernel-msg-key pp'
-  for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[slicing] slicing requests in progress...
+[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] computing for function f1 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37.
+[eva] computing for function lib_f <- f1 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23.
+[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning: 
+  Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] using specification for function lib_f
+[eva] Done for function lib_f
+[eva] Recording results for f1
+[eva] Done for function f1
+[eva] computing for function f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38.
+[eva] computing for function lib_f <- f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] computing for function f3 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39.
+[eva] computing for function lib_f <- f3 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31.
+[eva] Done for function lib_f
+[eva] Recording results for f3
+[eva] Done for function f3
+[eva] computing for function f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40.
+[eva] computing for function lib_f <- f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] Recording results for main
+[eva] done for function main
+[slicing] initializing slicing ...
+[slicing] interpreting slicing requests from the command line...
+[pdg] computing for function f3
+[from] Computing for function lib_f
+[from] Done for function lib_f
+[pdg] done for function f3
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[pdg] computing for function main
+[from] Computing for function f1
+[from] Done for function f1
+[from] Computing for function f2
+[from] Done for function f2
+[from] Computing for function f3
+[from] Done for function f3
+[pdg] done for function main
+[slicing] exporting project to 'Slicing export'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Slicing export tmp'
+[sparecode] removed unused global declarations in new project 'Slicing export'
+/* Generated by Frama-C */
+int lib_f(int n, void * const *__va_params);
+
+int f3_slice_1(void)
+{
+  int tmp;
+  {
+    void *__va_args[3];
+    tmp = lib_f(3,(void * const *)(__va_args));
+  }
+  return tmp;
+}
+
+void main(void)
+{
+  f3_slice_1();
+  return;
+}
+
+
diff --git a/tests/slicing/oracle/variadic.3.res.oracle b/tests/slicing/oracle/variadic.3.res.oracle
index 55bbb63c595e90a981765ba7da3919249820e930..e4cedf8c754b3f10ec4e5f6cfc1338731d477c1e 100644
--- a/tests/slicing/oracle/variadic.3.res.oracle
+++ b/tests/slicing/oracle/variadic.3.res.oracle
@@ -1,8 +1,85 @@
 [kernel] Parsing variadic.c (with preprocessing)
-[kernel] User Error: failed to run: gcc -E -C -I.  -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/variadic.ce8a359.i' '/home/bobot/Sources/frama-c/_build/default/result/variadic.c'
-  this is possibly due to missing preprocessor flags;
-  consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
-  See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "variadic.c" that has errors. Add '-kernel-msg-key pp'
-  for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[slicing] slicing requests in progress...
+[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] computing for function f1 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37.
+[eva] computing for function lib_f <- f1 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23.
+[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning: 
+  Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] using specification for function lib_f
+[eva] Done for function lib_f
+[eva] Recording results for f1
+[eva] Done for function f1
+[eva] computing for function f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38.
+[eva] computing for function lib_f <- f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] computing for function f3 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39.
+[eva] computing for function lib_f <- f3 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31.
+[eva] Done for function lib_f
+[eva] Recording results for f3
+[eva] Done for function f3
+[eva] computing for function f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40.
+[eva] computing for function lib_f <- f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] Recording results for main
+[eva] done for function main
+[slicing] initializing slicing ...
+[slicing] interpreting slicing requests from the command line...
+[pdg] computing for function main
+[from] Computing for function f1
+[from] Computing for function lib_f <-f1
+[from] Done for function lib_f
+[from] Done for function f1
+[from] Computing for function f2
+[from] Done for function f2
+[from] Computing for function f3
+[from] Done for function f3
+[pdg] done for function main
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[pdg] computing for function f2
+[pdg] done for function f2
+[slicing] exporting project to 'Slicing export'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Slicing export tmp'
+[sparecode] removed unused global declarations in new project 'Slicing export'
+/* Generated by Frama-C */
+int lib_f(int n, void * const *__va_params);
+
+int f2_slice_1(void)
+{
+  int tmp;
+  {
+    void *__va_args[2];
+    tmp = lib_f(2,(void * const *)(__va_args));
+  }
+  return tmp;
+}
+
+int main(void)
+{
+  int s;
+  s = f2_slice_1();
+  return s;
+}
+
+
diff --git a/tests/slicing/oracle/variadic.4.res.oracle b/tests/slicing/oracle/variadic.4.res.oracle
index cc0e55b1e04eab1befa91feaacb2df310f6b356b..e4cedf8c754b3f10ec4e5f6cfc1338731d477c1e 100644
--- a/tests/slicing/oracle/variadic.4.res.oracle
+++ b/tests/slicing/oracle/variadic.4.res.oracle
@@ -1,8 +1,85 @@
 [kernel] Parsing variadic.c (with preprocessing)
-[kernel] User Error: failed to run: gcc -E -C -I.  -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/variadic.cdcb684.i' '/home/bobot/Sources/frama-c/_build/default/result/variadic.c'
-  this is possibly due to missing preprocessor flags;
-  consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
-  See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "variadic.c" that has errors. Add '-kernel-msg-key pp'
-  for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[slicing] slicing requests in progress...
+[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] computing for function f1 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37.
+[eva] computing for function lib_f <- f1 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23.
+[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning: 
+  Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] using specification for function lib_f
+[eva] Done for function lib_f
+[eva] Recording results for f1
+[eva] Done for function f1
+[eva] computing for function f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38.
+[eva] computing for function lib_f <- f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] computing for function f3 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39.
+[eva] computing for function lib_f <- f3 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31.
+[eva] Done for function lib_f
+[eva] Recording results for f3
+[eva] Done for function f3
+[eva] computing for function f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40.
+[eva] computing for function lib_f <- f2 <- main.
+  Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] Recording results for main
+[eva] done for function main
+[slicing] initializing slicing ...
+[slicing] interpreting slicing requests from the command line...
+[pdg] computing for function main
+[from] Computing for function f1
+[from] Computing for function lib_f <-f1
+[from] Done for function lib_f
+[from] Done for function f1
+[from] Computing for function f2
+[from] Done for function f2
+[from] Computing for function f3
+[from] Done for function f3
+[pdg] done for function main
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[pdg] computing for function f2
+[pdg] done for function f2
+[slicing] exporting project to 'Slicing export'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Slicing export tmp'
+[sparecode] removed unused global declarations in new project 'Slicing export'
+/* Generated by Frama-C */
+int lib_f(int n, void * const *__va_params);
+
+int f2_slice_1(void)
+{
+  int tmp;
+  {
+    void *__va_args[2];
+    tmp = lib_f(2,(void * const *)(__va_args));
+  }
+  return tmp;
+}
+
+int main(void)
+{
+  int s;
+  s = f2_slice_1();
+  return s;
+}
+
+
diff --git a/tests/slicing/select_by_annot.i b/tests/slicing/select_by_annot.i
index 06069b98128d2bd399460b9c2f4b27f197792352..1a70a1cd5adb13b8ad4502e25f709d911b955c58 100644
--- a/tests/slicing/select_by_annot.i
+++ b/tests/slicing/select_by_annot.i
@@ -1,8 +1,8 @@
 /* run.config
 
-   CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+   CMD: @frama-c@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
    OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -journal-disable
-   CMD: bin/toplevel.opt
+   CMD: frama-c
    OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
    OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
    OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma modifS -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
diff --git a/tests/slicing/select_simple.i b/tests/slicing/select_simple.i
index 2ff216ec85d7fc5386c3a1c0a9cdce8053f0f8bb..8452d2a73e567af0b87447ac13f468f475682815 100644
--- a/tests/slicing/select_simple.i
+++ b/tests/slicing/select_simple.i
@@ -1,6 +1,6 @@
 /* run.config
 
-   CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+   CMD: @frama-c@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
    OPT: @EVA_OPTIONS@ -deps -journal-disable
 */
 
diff --git a/tests/slicing/simple_intra_slice.i b/tests/slicing/simple_intra_slice.i
index 085ceb13737735481d8631d042219b0df636f838..76a3f94515b0005873c364c61ff74ef0376d98bc 100644
--- a/tests/slicing/simple_intra_slice.i
+++ b/tests/slicing/simple_intra_slice.i
@@ -1,6 +1,6 @@
 /* run.config
 
-   CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+   CMD: @frama-c@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
    OPT: @EVA_OPTIONS@ -deps -no-slice-callers -journal-disable
 */
 int Unknown;
diff --git a/tests/slicing/slice_no_body.i b/tests/slicing/slice_no_body.i
index 75786a6ef323420c33889ded183e67ba650c21df..83937bd08382b970bb619c22c7d7190d25963db6 100644
--- a/tests/slicing/slice_no_body.i
+++ b/tests/slicing/slice_no_body.i
@@ -1,6 +1,6 @@
 /* run.config
 
-   CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+   CMD: @frama-c@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
    OPT: @EVA_OPTIONS@ -deps -lib-entry -main h -journal-disable
 */
 
diff --git a/tests/slicing/switch.i b/tests/slicing/switch.i
index 7e0a12e0555514382e0b63d7bf7b27503e033c43..de3807ffdbe506633b03c1aa3752c2e00ccb9c70 100644
--- a/tests/slicing/switch.i
+++ b/tests/slicing/switch.i
@@ -1,6 +1,6 @@
 /*  run.config
 
-   CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+   CMD: @frama-c@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
    OPT: @EVA_OPTIONS@ -deps -journal-disable
 */
 int main (char choix) {
diff --git a/tests/slicing/test_config b/tests/slicing/test_config
index 1712a20359b38feaedc7a61eec51ffa3aebc9879..d33c6619cf51abff91f19deb6891f44a32e044f5 100644
--- a/tests/slicing/test_config
+++ b/tests/slicing/test_config
@@ -1 +1,2 @@
+PLUGIN: slicing
 OPT: @EVA_OPTIONS@
diff --git a/tests/slicing/variadic.c b/tests/slicing/variadic.c
index 9de40fa3f8165c58332963c040dfa604669dd68a..4629542db44e021920215bdaa6000a1a479e6bd5 100644
--- a/tests/slicing/variadic.c
+++ b/tests/slicing/variadic.c
@@ -1,4 +1,5 @@
 /* run.config
+    DEPS: ../pdg/variadic.c
     STDOPT: +"-slice-return f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -print"
     STDOPT: +"-slice-return f3 -no-slice-callers -journal-disable -variadic-no-translation -then-last -print"
     STDOPT: +"-slice-return f3 -journal-disable -then-on 'Slicing export' -print"
@@ -6,4 +7,4 @@
     STDOPT: +"-slice-return main -slicing-level 3  -journal-disable -then-on 'Slicing export' -print"
 */
 
-#include "../pdg/variadic.c"
+#include "../../pdg/variadic.c"
diff --git a/tests/spec/acsl_basic_allocator.c b/tests/spec/acsl_basic_allocator.c
index 6a964f453b7c985be5238eb94ae243254fa59357..1390061b451e6a2b32107cebdb3a5b55c065e107 100644
--- a/tests/spec/acsl_basic_allocator.c
+++ b/tests/spec/acsl_basic_allocator.c
@@ -8,7 +8,7 @@
 /* This file presents the basic version of the allocator.                    */
 /*****************************************************************************/
 
-#include "share/libc/stdlib.h"
+#include "stdlib.h"
 
 #define DEFAULT_BLOCK_SIZE 1000
 
diff --git a/tests/spec/purse.c b/tests/spec/purse.c
index 2d444b25ee4a8baabc067e2bab89ad0fb8bc025d..fdef9a9ee1a3887037f60a5fa4eb9265e6b03622 100644
--- a/tests/spec/purse.c
+++ b/tests/spec/purse.c
@@ -21,7 +21,7 @@
 /*  (enclosed in the file GPL).                                           */
 /*                                                                        */
 /**************************************************************************/
-#include "share/libc/stdlib.h"
+#include "stdlib.h"
 typedef struct purse {
   int balance;
 } purse;
diff --git a/tests/syntax/assert_location.c b/tests/syntax/assert_location.c
index b9575ad6a324872dcae8e455980260682fb84217..d52518141f2b8adc258ebc74b7ed4211809c82e4 100644
--- a/tests/syntax/assert_location.c
+++ b/tests/syntax/assert_location.c
@@ -1,3 +1,8 @@
+/* run.config
+DEPS: assert_location.h
+
+*/
+
 #include "assert_location.h"
 
 void c() {
diff --git "a/tests/syntax/foo\".c" "b/tests/syntax/foo\".c"
index fa4ba0ab9ae9b4f51247cc78b369db0154bdfa9a..5933f9603a0e136d34c0680af6714d936839eaa5 100644
--- "a/tests/syntax/foo\".c"
+++ "b/tests/syntax/foo\".c"
@@ -1,4 +1,4 @@
-#include "share/libc/assert.h"
+#include "assert.h"
 
 int test = 1;
 
diff --git a/tests/syntax/gcc_builtins.c b/tests/syntax/gcc_builtins.c
index d6ff8e598a2c634f393708eab6643d1200c7bdae..00a9054c8b191a212b70e1b5000c4b710c4984ae 100644
--- a/tests/syntax/gcc_builtins.c
+++ b/tests/syntax/gcc_builtins.c
@@ -2,7 +2,7 @@
    STDOPT: +"-machdep gcc_x86_32"
  */
 
-#include "share/libc/stdint.h"
+#include "stdint.h"
 
 #define likely(x)  __builtin_expect((x),1)
 #define unlikely(x)  __builtin_expect((x),0)
diff --git a/tests/syntax/merge_unused.c b/tests/syntax/merge_unused.c
index b7233c675d0c28cc82f633f8403f6b7040571f2e..c8283fabb0a857da18cd39903303c50a59c5cfca 100644
--- a/tests/syntax/merge_unused.c
+++ b/tests/syntax/merge_unused.c
@@ -1,4 +1,5 @@
 /* run.config
+DEPS: merge_unused.h
 OPT: -cpp-extra-args="-I@PTEST_DIR@" @PTEST_DIR@/@PTEST_NAME@_2.c -print
 */
 
diff --git a/tests/syntax/multiple_decls_contracts.c b/tests/syntax/multiple_decls_contracts.c
index 3ac56b12d72e1800376ceb32e99c82755cca9076..4f782213f01ed703bef0d0b575b3082157da09d0 100644
--- a/tests/syntax/multiple_decls_contracts.c
+++ b/tests/syntax/multiple_decls_contracts.c
@@ -1,7 +1,7 @@
 /* run.config
-OPT: share/libc/string.h @PTEST_FILE@ @PTEST_FILE@ -cpp-extra-args="-Ishare/libc" -print
-OPT: @PTEST_FILE@ share/libc/string.h @PTEST_FILE@ -cpp-extra-args="-Ishare/libc" -print
-OPT: @PTEST_FILE@ @PTEST_FILE@ share/libc/string.h -cpp-extra-args="-Ishare/libc" -print
+OPT: string.h @PTEST_FILE@ @PTEST_FILE@ -cpp-extra-args="-Ishare/libc" -print
+OPT: @PTEST_FILE@ string.h @PTEST_FILE@ -cpp-extra-args="-Ishare/libc" -print
+OPT: @PTEST_FILE@ @PTEST_FILE@ string.h -cpp-extra-args="-Ishare/libc" -print
 */
 
 #include "string.h"
diff --git a/tests/syntax/offsetof.c b/tests/syntax/offsetof.c
index 06a79ecae3b9f960d5824f81c79f950d653634f1..1d378d9b65851455bf52e29dfa15c9a06e94f378 100644
--- a/tests/syntax/offsetof.c
+++ b/tests/syntax/offsetof.c
@@ -1,4 +1,4 @@
-#include "share/libc/stddef.h"
+#include "stddef.h"
 
 struct c {char ca;};
 void main(void) {
diff --git a/tests/value/CruiseControl.c b/tests/value/CruiseControl.c
index 1a445a21b266bbbf36ebaa4b2026d3d7835e2a16..858b6fcc1e7b462c9a3b2335d53e0ef12cddc969 100644
--- a/tests/value/CruiseControl.c
+++ b/tests/value/CruiseControl.c
@@ -1,4 +1,5 @@
 /* run.config*
+   DEPS: CruiseControl.h
    GCC:
    STDOPT: #"-float-normal CruiseControl_const.c -lib-entry -main CruiseControl -context-depth 10 -context-valid-pointers"
 
diff --git a/tests/value/CruiseControl_const.c b/tests/value/CruiseControl_const.c
index 92a1f42e65fa3c5891272111223bbe2d233a66b9..7b8f5cf661baa1fe678a4e0975c1b5464276c670 100644
--- a/tests/value/CruiseControl_const.c
+++ b/tests/value/CruiseControl_const.c
@@ -1,4 +1,5 @@
 /* run.config*
+   DEPS: CruiseControl.h
    GCC:
    DONTRUN:
 */
diff --git a/tests/value/abstract_struct_1.c b/tests/value/abstract_struct_1.c
index 3660041bcabc0d2f2be73bb0e286c50f4151f9f9..9b66ac139f5c7310bfb651e3f9ec436f84e85692 100644
--- a/tests/value/abstract_struct_1.c
+++ b/tests/value/abstract_struct_1.c
@@ -1,7 +1,7 @@
 /* run.config*
    STDOPT: #"abstract_struct_2.c -lib-entry -eva-msg-key initial-state"
 */
-#include "share/libc/stdlib.h"
+#include "stdlib.h"
 
 struct abstracttype;
 struct something {
diff --git a/tests/value/inline.c b/tests/value/inline.c
index b0264d3f0cbc015f8dc61dd30edc4eea20cf543d..38fccd7c9f2c381deaa42e3912b28b537574ef42 100644
--- a/tests/value/inline.c
+++ b/tests/value/inline.c
@@ -1,4 +1,5 @@
 /* run.config*
+   DEPS: inline.h
    DONTRUN: test for the gui only
 */
 
diff --git a/tests/value/wide_string.c b/tests/value/wide_string.c
index bf27d1585cf474a2ee7dc565ee8beb030c0f780c..75a975feaec078898583c80c613aa76312ee8422 100644
--- a/tests/value/wide_string.c
+++ b/tests/value/wide_string.c
@@ -1,4 +1,4 @@
-#include "share/libc/stddef.h"
+#include "stddef.h"
 
 int main(volatile int v) {