diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 5b1478eeb934c3ad8192bda11c4b22724318b429..e945f7923794f1bc819cbb5c5b36befa230546af 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -588,23 +588,6 @@ end = struct
 
 end
 
-type execnow =
-  {
-    ex_cmd: string;      (** command to launch *)
-    ex_log: string list; (** log files *)
-    ex_bin: string list; (** bin files *)
-    ex_dir: SubDir.t;    (** directory of test suite *)
-    ex_once: bool;       (** true iff the command has to be executed only once
-                             per config file (otherwise it is executed for
-                             every file of the test suite) *)
-    ex_done: bool ref;   (** has the command been already fully executed.
-                             Shared between all copies of this EXECNOW. Do
-                             NOT use a mutable field here, as execnows
-                             are duplicated using OCaml 'with' syntax. *)
-    ex_timeout: string;
-  }
-
-
 module Macros =
 struct
   module StringMap = Map.Make (String)
@@ -612,52 +595,55 @@ struct
 
   type t = string StringMap.t
 
-  let empty = StringMap.empty
+  let add_defaults ~defaults macros =
+    StringMap.merge (fun _k default cur ->
+        match cur with
+        | Some _ -> cur
+        | _ -> default) defaults macros
 
-  let macro_regex = Str.regexp "\\([^@]*\\)@\\([^@]*\\)@\\(.*\\)"
+  let empty = StringMap.empty
 
   let print_macros macros =
     lock_printf "%% Macros (%d):@."  (StringMap.cardinal macros);
     StringMap.iter (fun key data -> lock_printf "%% - %s -> %s@." key data) macros;
     lock_printf "%% End macros@."
 
-  let does_expand macros s =
-    if !verbosity >=4 then print_macros macros;
-    let rec aux n (ptest_file_matched,s as acc) =
-      if Str.string_match macro_regex s n then begin
-        let macro = Str.matched_group 2 s in
-        let ptest_file_matched = ptest_file_matched || macro = "PTEST_FILE" in
-        let start = Str.matched_group 1 s in
-        let rest = Str.matched_group 3 s in
-        let new_n = Str.group_end 1 in
-        let n, new_s =
-          if macro = "" then begin
-            new_n + 1, String.sub s 0 new_n ^ "@" ^ rest
-          end else begin
-            try
-              if !verbosity >= 4 then lock_printf "%%     - macro is %s\n%!" macro;
-              let replacement =  find macro macros in
-              if !verbosity >= 3 then
-                lock_printf "%%     - replacement for %s is %s\n%!" macro replacement;
-              new_n,
-              String.sub s 0 n ^ start ^ replacement ^ rest
-            with
-            | Not_found -> Str.group_end 2 + 1, s
-          end
+  let does_expand =
+    let macro_regex = Str.regexp "@\\([-A-Za-z_0-9]+\\)@" in
+    fun macros s ->
+      let has_ptest_file = ref false in
+      if !verbosity >= 3 then lock_printf "%% Expand: %s@." s;
+      if !verbosity >= 4 then print_macros macros;
+      let rec aux s =
+        let expand_macro = function
+          | Str.Text s -> s
+          | Str.Delim s ->
+            if Str.string_match macro_regex s 0 then begin
+              let macro = Str.matched_group 1 s in
+              try
+                if !verbosity >= 4 then lock_printf "%%     - macro is %s\n%!" macro;
+                let replacement = find macro macros in
+                if String.(macro = "PTEST_FILE") then has_ptest_file := true;
+                if !verbosity >= 3 then
+                  lock_printf "%%     - replacement for %s is %s\n%!" macro replacement;
+                aux replacement
+              with
+              | Not_found -> s
+            end
+            else s
         in
-        if !verbosity >= 4 then lock_printf "%%    - New string is %s\n%!" new_s;
-        let new_acc = ptest_file_matched, new_s in
-        if n <= String.length new_s then aux n new_acc else new_acc
-      end else acc
-    in
-    Mutex.lock str_mutex;
-    try
-      let res = aux 0 (false,s) in
-      Mutex.unlock str_mutex; res
-    with e ->
-      lock_eprintf "Uncaught exception %s\n%!" (Printexc.to_string e);
-      Mutex.unlock str_mutex;
-      raise e
+        String.concat "" (List.map expand_macro (Str.full_split macro_regex s))
+      in
+      try
+        Mutex.lock str_mutex;
+        let r = aux s in
+        Mutex.unlock str_mutex;
+        if !verbosity >= 3 then lock_printf "%% Expansion result: %s@." r;
+        !has_ptest_file, r
+      with e ->
+        lock_eprintf "Uncaught exception %s\n%!" (Printexc.to_string e);
+        Mutex.unlock str_mutex;
+        raise e
 
   let expand macros s =
     snd (does_expand macros s)
@@ -676,6 +662,24 @@ struct
 end
 
 
+type execnow =
+  {
+    ex_cmd: string;      (** command to launch *)
+    ex_macros: Macros.t; (** current macros *)
+    ex_log: string list; (** log files *)
+    ex_bin: string list; (** bin files *)
+    ex_dir: SubDir.t;    (** directory of test suite *)
+    ex_once: bool;       (** true iff the command has to be executed only once
+                             per config file (otherwise it is executed for
+                             every file of the test suite) *)
+    ex_done: bool ref;   (** has the command been already fully executed.
+                             Shared between all copies of this EXECNOW. Do
+                             NOT use a mutable field here, as execnows
+                             are duplicated using OCaml 'with' syntax. *)
+    ex_timeout: string;
+  }
+
+
 (** configuration of a directory/test. *)
 type cmd = {
   toplevel: string;
@@ -767,7 +771,7 @@ end = struct
       dc_timeout = "";
     }
 
-  let scan_execnow ~once dir ex_timeout (s:string) =
+  let scan_execnow ~once dir ex_macros ex_timeout (s:string) =
     let rec aux (s:execnow) =
       try
         Scanf.sscanf s.ex_cmd "%_[ ]LOG%_[ ]%[-A-Za-z0-9_',+=:.\\@@]%_[ ]%s@\n"
@@ -789,6 +793,7 @@ end = struct
     in
     aux
       { ex_cmd = s;
+        ex_macros;
         ex_log = [];
         ex_bin = [];
         ex_dir = dir;
@@ -847,12 +852,12 @@ end = struct
 
 
   (* how to process options *)
-  let config_exec ~once ~drop:_ ~file:_ dir s current =
+  let config_exec ~once ~file:_ dir s current =
     { current with
       dc_execnow =
-        scan_execnow ~once dir current.dc_timeout s :: current.dc_execnow }
+        scan_execnow ~once dir current.dc_macros current.dc_timeout s :: current.dc_execnow }
 
-  let config_macro ~drop:_ ~file _dir s current =
+  let config_macro ~file _dir s current =
     let regex = Str.regexp "[ \t]*\\([^ \t@]+\\)\\([ \t]+\\(.*\\)\\|$\\)" in
     Mutex.lock str_mutex;
     if Str.string_match regex s 0 then begin
@@ -872,18 +877,12 @@ end = struct
 
   let set_load_modules deps macros =
     let name = "PTEST_LOAD_MODULES" in
-    let def = List.fold_left (fun acc s ->
-        match acc with
-        | "" -> s
-        | acc -> s ^ "," ^ acc)
-        ""
-        deps
-    in
+    let def = String.concat "," deps in
     if !verbosity >= 3 then
       lock_printf "%%   - Macro %s for -load-module with definition %s@." name def;
     Macros.add_list [name, def] macros
 
-  let add_make_modules ~drop ~file dir deps current =
+  let add_make_modules ~file dir deps current =
     let deps,current = List.fold_left (fun ((deps,curr) as acc) s ->
         if StringSet.mem s curr.dc_cmxs_module then acc
         else
@@ -894,23 +893,23 @@ end = struct
     if String.(deps = "") then current
     else
       let make_cmd = Macros.expand current.dc_macros "@PTEST_MAKE_MODULE@" in
-      config_exec ~once:true ~drop ~file dir (make_cmd ^ " " ^ deps) current
+      config_exec ~once:true ~file dir (make_cmd ^ " " ^ deps) current
 
-  let config_module ~drop ~file dir s current =
+  let config_module ~file dir s current =
     let s = Macros.expand current.dc_macros s in
     let deps = List.map (fun s -> "@PTEST_DIR@/" ^ (Filename.remove_extension s) ^ ".cmxs")
         (str_split_list s)
     in
-    let current = add_make_modules ~drop ~file dir deps current in
+    let current = add_make_modules ~file dir deps current in
     { current with dc_macros = set_load_modules deps current.dc_macros }
 
   let config_options =
     [ "CMD",
-      (fun ~drop:_ ~file:_ _ s current -> { current with dc_default_toplevel = s});
+      (fun ~file:_ _ s current -> { current with dc_default_toplevel = s});
 
       "OPT",
-      (fun ~drop ~file _ s current ->
-         if not (drop || current.dc_framac) then
+      (fun ~file _ s current ->
+         if not (current.dc_framac) then
            lock_eprintf
              "%s: a NOFRAMAC directive has been defined before a sub-test defined by a 'OPT' directive (That NOFRAMAC directive could be misleading.).@."
              file;
@@ -927,19 +926,20 @@ end = struct
            dc_commands = t :: current.dc_commands });
 
       "STDOPT",
-      (fun ~drop ~file _ s current ->
-         if not (drop || current.dc_framac) then
+      (fun ~file _ s current ->
+         if not current.dc_framac then
            lock_eprintf
              "%s: a NOFRAMAC directive has been defined before a sub-test defined by a 'STDOPT' directive (That NOFRAMAC directive could be misleading.).@."
              file;
          let new_top =
            List.map
              (fun command ->
-                { command with opts= make_custom_opts command.opts s;
-                               logs= command.logs @ current.dc_default_log;
-                               macros= current.dc_macros;
-                               exit_code = current.dc_exit_code;
-                               timeout= current.dc_timeout
+                { toplevel = current.dc_default_toplevel;
+                  opts= make_custom_opts command.opts s;
+                  logs= command.logs @ current.dc_default_log;
+                  macros= current.dc_macros;
+                  exit_code = current.dc_exit_code;
+                  timeout= current.dc_timeout
                 })
              !default_parsing_env.current_default_cmds
          in
@@ -947,10 +947,10 @@ end = struct
                         dc_default_log = !default_parsing_env.current_default_log });
 
       "FILEREG",
-      (fun ~drop:_ ~file:_ _ s current -> { current with dc_test_regexp = s });
+      (fun ~file:_ _ s current -> { current with dc_test_regexp = s });
 
       "FILTER",
-      (fun ~drop:_ ~file:_ _ s current ->
+      (fun ~file:_ _ s current ->
          let s = trim_right s in
          match current.dc_filter with
          | None when s="" -> { current with dc_filter = None }
@@ -958,18 +958,18 @@ end = struct
          | Some filter    -> { current with dc_filter = Some (s ^ " | " ^ filter) });
 
       "EXIT",
-      (fun ~drop:_ ~file:_ _ s current -> { current with dc_exit_code = Some s });
+      (fun ~file:_ _ s current -> { current with dc_exit_code = Some s });
 
       "GCC",
-      (fun ~drop ~file _ _ acc ->
-         if not drop then lock_eprintf "%s: GCC directive (DEPRECATED)@." file;
+      (fun ~file _ _ acc ->
+         lock_eprintf "%s: GCC directive (DEPRECATED)@." file;
          acc);
 
       "COMMENT",
-      (fun ~drop:_ ~file:_ _ _ acc -> acc);
+      (fun ~file:_ _ _ acc -> acc);
 
       "DONTRUN",
-      (fun ~drop:_ ~file:_ _ s current -> { current with dc_dont_run = true });
+      (fun ~file:_ _ s current -> { current with dc_dont_run = true });
 
       "EXECNOW", config_exec ~once:true;
       "EXEC", config_exec ~once:false;
@@ -979,14 +979,14 @@ end = struct
       "MODULE", config_module;
 
       "LOG",
-      (fun ~drop:_ ~file:_ _ s current -> { current with dc_default_log = s :: current.dc_default_log });
+      (fun ~file:_ _ s current -> { current with dc_default_log = s :: current.dc_default_log });
 
       "TIMEOUT",
-      (fun ~drop:_ ~file:_ _ s current -> { current with dc_timeout = s });
+      (fun ~file:_ _ s current -> { current with dc_timeout = s });
 
       "NOFRAMAC",
-      (fun ~drop ~file _ _ current ->
-         if not drop && current.dc_commands <> [] && current.dc_framac then
+      (fun ~file _ _ current ->
+         if current.dc_commands <> [] && current.dc_framac then
            lock_eprintf
              "%s: a NOFRAMAC directive has the effect of ignoring previous defined sub-tests (by some 'OPT' or 'STDOPT' directives that seems misleading). @."
              file;
@@ -1004,7 +1004,9 @@ end = struct
         Scanf.sscanf s "%[ *]%[A-Za-z0-9]: %s@\n"
           (fun _ name opt ->
              try
-               r := (List.assoc name config_options) ~drop ~file dir opt !r
+               let directive = List.assoc name config_options in
+               if not drop then
+                 r := directive ~file dir opt !r;
              with Not_found ->
                lock_eprintf "@[%s: unknown configuration option: %s@\n%!@]" file name)
       with
@@ -1093,7 +1095,7 @@ end
 
 type toplevel_command =
   { macros: Macros.t;
-    mutable log_files: string list;
+    log_files: string list;
     file : string ;
     nb_files : int ;
     options : string ;
@@ -1172,7 +1174,7 @@ module Cmd : sig
   val log_prefix : toplevel_command -> string
   val oracle_prefix : toplevel_command -> string
 
-  val get_macros : toplevel_command -> string Macros.StringMap.t
+  val expand_macros : defaults:Macros.t -> toplevel_command -> toplevel_command
 
   (* [basic_command_string cmd] does not redirect the outputs, and does
      not overwrite the result files *)
@@ -1206,7 +1208,7 @@ end = struct
 
   let get_ptest_file cmd = SubDir.make_file cmd.directory cmd.file
 
-  let get_macros cmd =
+  let expand_macros ~defaults cmd =
     let ptest_config =
       if !special_config = "" then "" else "_" ^ !special_config
     in
@@ -1225,7 +1227,17 @@ end = struct
         "PTEST_NUMBER", string_of_int cmd.n;
       ]
     in
-    Macros.add_list macros cmd.macros
+    let macros = Macros.add_list macros cmd.macros in
+    let macros = Macros.add_defaults ~defaults macros in
+    let process_macros s = Macros.expand macros s in
+    { cmd with
+      macros;
+      log_files = List.map process_macros cmd.log_files;
+      filter =
+        match cmd.filter with
+        | None -> None
+        | Some filter -> Some (process_macros filter)
+    }
 
   let contains_frama_c_binary_name =
     Str.regexp "[^( ]*\\(toplevel\\|viewer\\|frama-c-gui\\|frama-c[^-]\\).*"
@@ -1235,9 +1247,7 @@ end = struct
 
   let basic_command_string =
     fun command ->
-    let macros = get_macros command in
-    let logfiles = List.map (Macros.expand macros) command.log_files in
-    command.log_files <- logfiles;
+    let macros = command.macros in
     let has_ptest_file_t, toplevel =
       Macros.does_expand macros command.toplevel
     in
@@ -1314,9 +1324,7 @@ end = struct
     update_oracle (log_prefix ^ ".res.log") (oracle_prefix ^ ".res.oracle");
     update_oracle (log_prefix ^ ".err.log") (oracle_prefix ^ ".err.oracle");
     (* Update files related to LOG directives *)
-    let macros = get_macros command in
-    let log_files = List.map (Macros.expand macros) command.log_files in
-    List.iter (update_log_files command.directory) log_files
+    List.iter (update_log_files command.directory) command.log_files
 
 end
 
@@ -1435,8 +1443,6 @@ let do_command command =
         ignore (launch basic_command_string)
       end
       else begin
-        (* command string also replaces macros in logfiles names, which
-           is useful for Examine as well. *)
         let command_string = Cmd.command_string command in
         let summary_ret =
           if !behavior <> Examine
@@ -1932,7 +1938,7 @@ let dispatcher () =
         fun {toplevel; opts=options; logs=log_files; macros; exit_code; timeout} ->
           let n = !i in
           incr i;
-          let cmd =
+          Cmd.expand_macros ~defaults:config.dc_macros
             { file; options; toplevel; nb_files; directory; n; log_files;
               filter = config.dc_filter; macros;
               exit_code = begin
@@ -1945,12 +1951,6 @@ let dispatcher () =
               execnow=false;
               timeout;
             }
-          in
-          let macros = Cmd.get_macros cmd in
-          match cmd.filter with
-          | None -> cmd
-          | Some filter ->
-            { cmd with filter = Some (Macros.expand macros filter) }
       in
       let nb_files_execnow = List.length config.dc_execnow in
       let make_execnow_cmd =
@@ -1958,29 +1958,30 @@ let dispatcher () =
         fun execnow ->
           let n = !e in
           incr e;
-          let cmd =  {
-            file ;
-            nb_files = nb_files_execnow;
-            log_files = [];
-            options = "";
-            toplevel = execnow.ex_cmd;
-            exit_code = 0;
-            n;
-            directory;
-            filter = None; (* No filter for execnow command *)
-            macros = config.dc_macros;
-            execnow = true;
-            timeout = execnow.ex_timeout;
-          } in
-          let macros = Cmd.get_macros cmd in
-          let process_macros s = Macros.expand macros s in
+          let cmd = Cmd.expand_macros ~defaults:config.dc_macros
+              {file ;
+               nb_files = nb_files_execnow;
+               log_files = execnow.ex_log;
+               options = "";
+               toplevel = execnow.ex_cmd;
+               exit_code = 0;
+               n;
+               directory;
+               filter = None; (* No filter for execnow command *)
+               macros = execnow.ex_macros;
+               execnow = true;
+               timeout = execnow.ex_timeout;
+              }
+          in
+          let process_macros s = Macros.expand cmd.macros s in
           { ex_cmd = Cmd.basic_command_string cmd;
-            ex_log = List.map process_macros execnow.ex_log;
+            ex_macros = cmd.macros;
+            ex_log = cmd.log_files;
             ex_bin = List.map process_macros execnow.ex_bin;
             ex_dir = execnow.ex_dir;
             ex_once = execnow.ex_once;
             ex_done = execnow.ex_done;
-            ex_timeout = execnow.ex_timeout;
+            ex_timeout = cmd.timeout;
           }
       in
       let treat_option q cmd =
diff --git a/src/plugins/e-acsl/tests/arith/bitwise.c b/src/plugins/e-acsl/tests/arith/bitwise.c
index 7dfa73a7c444bbd24f5911e3abde2010c53ed6db..676150fb0315130ec0efd4a7e9c6d7ffa2588339 100644
--- a/src/plugins/e-acsl/tests/arith/bitwise.c
+++ b/src/plugins/e-acsl/tests/arith/bitwise.c
@@ -1,7 +1,7 @@
 /* run.config_ci, run.config_dev
    COMMENT: Support of bitwise operations
-   STDOPT: #"-warn-right-shift-negative -warn-left-shift-negative"
    MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -warn-right-shift-negative -warn-left-shift-negative
+   STDOPT: #"-warn-right-shift-negative -warn-left-shift-negative"
 */
 
 #include <limits.h>
diff --git a/src/plugins/e-acsl/tests/builtin/test_config_dev b/src/plugins/e-acsl/tests/builtin/test_config_dev
index a915fc61b249ed381825662eecdb83418ae70384..75244f22baf113b9a89e5613d15e66d948db1264 100644
--- a/src/plugins/e-acsl/tests/builtin/test_config_dev
+++ b/src/plugins/e-acsl/tests/builtin/test_config_dev
@@ -1 +1,2 @@
 MACRO: ROOT_EACSL_GCC_OPTS_EXT --libc-replacements
+STDOPT:
diff --git a/src/plugins/e-acsl/tests/format/test_config_dev b/src/plugins/e-acsl/tests/format/test_config_dev
index aae787763c6565f6f717eb03b30a8221feb90fb6..d7f6f441060ba9eb22b426eaf816ff05a679840b 100644
--- a/src/plugins/e-acsl/tests/format/test_config_dev
+++ b/src/plugins/e-acsl/tests/format/test_config_dev
@@ -1,2 +1,3 @@
 MACRO: ROOT_EACSL_GCC_OPTS_EXT --validate-format-strings --full-mtracking -F -variadic-no-translation
 MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|/.*/share/e-acsl|FRAMAC_SHARE/e-acsl|"
+STDOPT:
diff --git a/src/plugins/e-acsl/tests/full-mtracking/test_config_dev b/src/plugins/e-acsl/tests/full-mtracking/test_config_dev
index 80a939ea02713f1e0fb539f6bfb567096a7e2510..7341131a532b15723e4ea283ad68908ff7ec3917 100644
--- a/src/plugins/e-acsl/tests/full-mtracking/test_config_dev
+++ b/src/plugins/e-acsl/tests/full-mtracking/test_config_dev
@@ -1 +1,2 @@
 MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking
+STDOPT:
diff --git a/src/plugins/e-acsl/tests/gmp-only/test_config_dev b/src/plugins/e-acsl/tests/gmp-only/test_config_dev
index 3a3fc2c7e601d0b97416e7f858e9ddeee944102f..17fca0a799c66f8133edd943ed1f76a484263218 100644
--- a/src/plugins/e-acsl/tests/gmp-only/test_config_dev
+++ b/src/plugins/e-acsl/tests/gmp-only/test_config_dev
@@ -1 +1,2 @@
 MACRO: ROOT_EACSL_GCC_OPTS_EXT --gmp
+STDOPT:
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
index 51fc747e19cee7c58bbf9b4de18291692b85314d..3e02977ecd65d1da1459b59dfa8cdca6227eb2cc 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
@@ -1,7 +1,7 @@
 /* run.config_ci, run.config_dev
    COMMENT: test option -e-acsl-instrument; cannot run Eva on this example
-   STDOPT:#"-e-acsl-instrument='@@all,-uninstrument1,-uninstrument2'"
-   MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -e-acsl-instrument @@@@all,-uninstrument1,-uninstrument2
+   STDOPT:#"-e-acsl-instrument='@all,-uninstrument1,-uninstrument2'"
+   MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -e-acsl-instrument @all,-uninstrument1,-uninstrument2
 */
 
 #include <stdarg.h>
diff --git a/src/plugins/e-acsl/tests/temporal/test_config_dev b/src/plugins/e-acsl/tests/temporal/test_config_dev
index a390cadc7c632ab6c59fde8881a2695e0749ef4d..ddff8508c1e18074db4e26c6d93ee182b04ec0fc 100644
--- a/src/plugins/e-acsl/tests/temporal/test_config_dev
+++ b/src/plugins/e-acsl/tests/temporal/test_config_dev
@@ -1 +1,2 @@
 MACRO: ROOT_EACSL_GCC_OPTS_EXT --temporal
+STDOPT:
diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in
index c10b67e1493d2b3bb5f112244bf657a09a5e1122..045e0fac2c994cb0d4fe5edc094ed3ddfb5b5a62 100644
--- a/src/plugins/e-acsl/tests/test_config_dev.in
+++ b/src/plugins/e-acsl/tests/test_config_dev.in
@@ -4,16 +4,20 @@ MACRO: DEST @PTEST_RESULT@/@PTEST_NAME@
 MACRO: OUT @PTEST_NAME@.res.log
 MACRO: ERR @PTEST_NAME@.err.log
 MACRO: EACSL_ERR @PTEST_NAME@.e-acsl.err.log
+
 COMMENT: Define the following macro to "no" in a test to stop the execution of `e-acsl-gcc.sh`
 MACRO: ROOT_EACSL_GCC_ENABLE yes
 COMMENT: Default options for `e-acsl-gcc.sh`
 MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X
 COMMENT: Default options for the frama-c invocation
 MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0
+
+EXEC: LOG @EACSL_ERR@ if test "@ROOT_EACSL_GCC_ENABLE@" = "yes"; then ./scripts/e-acsl-gcc.sh -I @frama-c@ -c @ROOT_EACSL_GCC_MISC_OPTS@ --frama-c-extra="@ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" @ROOT_EACSL_GCC_OPTS_EXT@ -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl 2>&1 1>/dev/null | @ROOT_EACSL_EXEC_FILTER@ > @PTEST_RESULT@/@EACSL_ERR@; fi
+
+COMMENT: These next macros can be redefined in a test file
 COMMENT: Define the following macro in a test to pass extra options to the frama-c invocation
 MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT
 COMMENT: Define the following macro in a test to pass extra options to `e-acsl-gcc.sh`
 MACRO: ROOT_EACSL_GCC_OPTS_EXT
 COMMENT: Define the following macro in a test to filter the output of the test execution
 MACRO: ROOT_EACSL_EXEC_FILTER cat
-EXEC: LOG @EACSL_ERR@ if test "@ROOT_EACSL_GCC_ENABLE@" = "yes"; then ./scripts/e-acsl-gcc.sh -I @frama-c@ -c @ROOT_EACSL_GCC_MISC_OPTS@ --frama-c-extra="@ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" @ROOT_EACSL_GCC_OPTS_EXT@ -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl 2>&1 1>/dev/null | @ROOT_EACSL_EXEC_FILTER@ > @PTEST_RESULT@/@EACSL_ERR@; fi
diff --git a/tests/misc/global_decl_loc.i b/tests/misc/global_decl_loc.i
index d13cbce847364dbce968f270f47d9cae11260cd8..e0f0ea85b89fcc58dd891952d708b4b99640979d 100644
--- a/tests/misc/global_decl_loc.i
+++ b/tests/misc/global_decl_loc.i
@@ -1,4 +1,5 @@
 /* run.config
-   OPT: @PTEST_DIR@/global_decl_loc2.i -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: global_decl_loc
+   OPT: @PTEST_DIR@/global_decl_loc2.i
  */
 int g;
diff --git a/tests/misc/global_decl_loc2.i b/tests/misc/global_decl_loc2.i
index 348015c7c228d43d8c167ed1572f48c9ebd7e94b..5f1867c879f6a4a75a417751a361c9e4e98a7cea 100644
--- a/tests/misc/global_decl_loc2.i
+++ b/tests/misc/global_decl_loc2.i
@@ -1,7 +1,6 @@
 /* run.config*
- EXIT: 0
-
-   OPT: @PTEST_DIR@/global_decl_loc.i -load-module @PTEST_DIR@/global_decl_loc.cmxs
+ MODULE: global_decl_loc
+   OPT: @PTEST_DIR@/global_decl_loc.i
 */
 
 extern int g;
diff --git a/tests/misc/oracle/global_decl_loc.res.oracle b/tests/misc/oracle/global_decl_loc.res.oracle
index 91dcbad389ee7258de2940ef69b8809c8228a4c6..ebeec539157719888ba079dcd5f302761b592f79 100644
--- a/tests/misc/oracle/global_decl_loc.res.oracle
+++ b/tests/misc/oracle/global_decl_loc.res.oracle
@@ -1,3 +1,3 @@
 [kernel] Parsing tests/misc/global_decl_loc.i (no preprocessing)
 [kernel] Parsing tests/misc/global_decl_loc2.i (no preprocessing)
-[kernel] global variable g declared at tests/misc/global_decl_loc.i:4
+[kernel] global variable g declared at tests/misc/global_decl_loc.i:5
diff --git a/tests/misc/oracle/global_decl_loc2.res.oracle b/tests/misc/oracle/global_decl_loc2.res.oracle
index cb0dd4ebc1ed2ac8dc7d06588f966e722cc06704..454d932e2db64309978664a32e711b64f34a109a 100644
--- a/tests/misc/oracle/global_decl_loc2.res.oracle
+++ b/tests/misc/oracle/global_decl_loc2.res.oracle
@@ -1,3 +1,3 @@
 [kernel] Parsing tests/misc/global_decl_loc2.i (no preprocessing)
 [kernel] Parsing tests/misc/global_decl_loc.i (no preprocessing)
-[kernel] global variable g declared at tests/misc/global_decl_loc.i:4
+[kernel] global variable g declared at tests/misc/global_decl_loc.i:5
diff --git a/tests/misc/test_config b/tests/misc/test_config
index 49f38b4a622efe9bb126ca0450ad800d06fde62d..111c347883729eb88f73d71774c9496d687e21fb 100644
--- a/tests/misc/test_config
+++ b/tests/misc/test_config
@@ -1 +1,2 @@
-EXECNOW: make -s @PTEST_DIR@/global_decl_loc.cmxs
+MODULE: global_decl_loc
+MODULE:
diff --git a/tests/pdg/dyn_dpds.c b/tests/pdg/dyn_dpds.c
index 8c40c94f19d036b5c74abead1be0f9f33f9b4c93..ac0cc5c1557930cd5b24a3a03028b83fcdf47fcc 100644
--- a/tests/pdg/dyn_dpds.c
+++ b/tests/pdg/dyn_dpds.c
@@ -1,6 +1,6 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   STDOPT: +"-load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -deps"
+ MODULE: @PTEST_NAME@
+   STDOPT: +"-deps"
 */
 
 
diff --git a/tests/saveload/basic.i b/tests/saveload/basic.i
index 6e2f8318e06b079b2a35dc0d74b806f4f8664d85..4c9fc76e904c0a440e172fe92979741020451fd3 100644
--- a/tests/saveload/basic.i
+++ b/tests/saveload/basic.i
@@ -1,15 +1,15 @@
 /* run.config
  MODULE: @PTEST_NAME@
-   EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva @EVA_OPTIONS@ -out -input -deps ./@PTEST_DIR@/@PTEST_NAME@.i -save ./tests/saveload/result/basic.sav > ./tests/saveload/result/basic_sav.res 2> ./tests/saveload/result/basic_sav.err
-   EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav @frama-c@ -save ./tests/saveload/result/basic.1.sav @PTEST_DIR@/@PTEST_NAME@.i -eva @EVA_OPTIONS@ -out -input -deps > ./tests/saveload/result/basic_sav.1.res 2> ./tests/saveload/result/basic_sav.1.err
+   EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save ./tests/saveload/result/basic.sav > ./tests/saveload/result/basic_sav.res 2> ./tests/saveload/result/basic_sav.err
  MODULE:
+   EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav @frama-c@ -save ./tests/saveload/result/basic.1.sav @PTEST_FILE@ -eva @EVA_OPTIONS@ -out -input -deps > ./tests/saveload/result/basic_sav.1.res 2> ./tests/saveload/result/basic_sav.1.err
    STDOPT: +"-load ./tests/saveload/result/basic.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable"
  MODULE: @PTEST_NAME@
    STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable -print"
  MODULE:
    STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable"
  MODULE: status
-   EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -load-module @PTEST_DIR@/status -save ./tests/saveload/result/status.sav @PTEST_DIR@/@PTEST_NAME@.i > ./tests/saveload/result/status_sav.res 2> ./tests/saveload/result/status_sav.err
+   EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -save ./tests/saveload/result/status.sav @PTEST_FILE@ > ./tests/saveload/result/status_sav.res 2> ./tests/saveload/result/status_sav.err
    STDOPT: +"-load ./tests/saveload/result/status.sav"
  MODULE:
    STDOPT: +"-load ./tests/saveload/result/status.sav"
diff --git a/tests/saveload/deps.i b/tests/saveload/deps.i
index ee704399b403bbf61ee9da3eab241d193b7a9426..267cbfcdb3029c1798d22195498207c2493c07f1 100644
--- a/tests/saveload/deps.i
+++ b/tests/saveload/deps.i
@@ -1,11 +1,15 @@
 /* run.config
-   EXECNOW: make -s ./tests/saveload/deps_A.cmxs ./tests/saveload/deps_B.cmxs ./tests/saveload/deps_C.cmxs ./tests/saveload/deps_D.cmxs ./tests/saveload/deps_E.cmxs
-   EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -load-module ./tests/saveload/deps_A.cmxs -eva @EVA_OPTIONS@ -out -input -deps ./tests/saveload/deps.i -save ./tests/saveload/result/deps.sav > ./tests/saveload/result/deps_sav.res 2> ./tests/saveload/result/deps_sav.err
-   STDOPT: +"-load-module ./tests/saveload/deps_A -load ./tests/saveload/result/deps.sav -eva @EVA_OPTIONS@ -out -input -deps "
-   STDOPT: +"-load-module ./tests/saveload/deps_B -load ./tests/saveload/result/deps.sav  -out -input -deps "
-   STDOPT: +"-load-module ./tests/saveload/deps_C -load ./tests/saveload/result/deps.sav  -out -input -deps "
-   STDOPT: +"-load-module ./tests/saveload/deps_D -load ./tests/saveload/result/deps.sav  -out -input -deps "
-   STDOPT: +"-load-module ./tests/saveload/deps_E -load ./tests/saveload/result/deps.sav  -out -input -deps "
+ MODULE: deps_A
+   EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save ./tests/saveload/result/deps.sav > ./tests/saveload/result/deps_sav.res 2> ./tests/saveload/result/deps_sav.err
+   STDOPT: +"-load ./tests/saveload/result/deps.sav -eva @EVA_OPTIONS@ -out -input -deps "
+ MODULE: deps_B
+   STDOPT: +"-load ./tests/saveload/result/deps.sav  -out -input -deps "
+ MODULE: deps_C
+   STDOPT: +"-load ./tests/saveload/result/deps.sav  -out -input -deps "
+ MODULE: deps_D
+   STDOPT: +"-load ./tests/saveload/result/deps.sav  -out -input -deps "
+ MODULE: deps_E
+   STDOPT: +"-load ./tests/saveload/result/deps.sav  -out -input -deps "
 */
 
 int main() {
diff --git a/tests/saveload/oracle/deps_sav.res b/tests/saveload/oracle/deps_sav.res
index 40f9aeda11453a63ab6d1a1c2a1b0b9083ec2cbe..dcd6cc739340a467e0ac03ccc205bdd0a57b4d9a 100644
--- a/tests/saveload/oracle/deps_sav.res
+++ b/tests/saveload/oracle/deps_sav.res
@@ -4,8 +4,8 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] tests/saveload/deps.i:15: starting to merge loop iterations
-[eva:alarm] tests/saveload/deps.i:15: Warning: 
+[eva] tests/saveload/deps.i:19: starting to merge loop iterations
+[eva:alarm] tests/saveload/deps.i:19: Warning: 
   signed overflow. assert -2147483648 ≤ i - 1;
 [eva] Recording results for main
 [eva] done for function main
diff --git a/tests/saveload/serialized_queue.i b/tests/saveload/serialized_queue.i
index 3d2c450536e513b1580c0197708c6f78599e4c31..cff840881244adc6afeec32e87e92973a4f7d20c 100644
--- a/tests/saveload/serialized_queue.i
+++ b/tests/saveload/serialized_queue.i
@@ -1,6 +1,6 @@
 /* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+ MODULE: @PTEST_NAME@
+   OPT:
 */
 
 // empty C file, we're only interested in the script itself
diff --git a/tests/slicing/adpcm.c b/tests/slicing/adpcm.c
index a3efe43e78c4a5e1416afd4fcae84f65229c0037..c32b08423fe053efc10b6187635a7d2279d1084f 100644
--- a/tests/slicing/adpcm.c
+++ b/tests/slicing/adpcm.c
@@ -1,7 +1,7 @@
 /* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
-   OPT: @EVA_OPTIONS@ -machdep x86_32 -ulevel -1 -deps -slicing-level 2 -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+   OPT: @EVA_OPTIONS@ -machdep x86_32 -ulevel -1 -deps -slicing-level 2
 */
 
 #include "../test/adpcm.c"
diff --git a/tests/slicing/combine.i b/tests/slicing/combine.i
index 0f9079399f408757772f49f89f4fee8dd8289752..704851ba39349b0e151e4a225cdb9ef865970fc9 100644
--- a/tests/slicing/combine.i
+++ b/tests/slicing/combine.i
@@ -1,7 +1,7 @@
 /* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
-   OPT: @EVA_OPTIONS@ -deps -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+   OPT: @EVA_OPTIONS@ -deps
 */
 
 //@ assigns \result \from x;
diff --git a/tests/slicing/ex_spec_interproc.i b/tests/slicing/ex_spec_interproc.i
index d767426b85ff29204b11021330357cb22c02e9c1..5436193b3db7d2c419913f2a63ccda8046b34857 100644
--- a/tests/slicing/ex_spec_interproc.i
+++ b/tests/slicing/ex_spec_interproc.i
@@ -1,7 +1,7 @@
 /* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
-   OPT: @EVA_OPTIONS@ -deps -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+   OPT: @EVA_OPTIONS@ -deps
 */
 
 int X, Y;
diff --git a/tests/slicing/mark_all_slices.i b/tests/slicing/mark_all_slices.i
index 9b5441dd0b431272a9de8cab89fc030517383c9c..8f0d154cfd27bf1640fc879e12ee28455b92aa8a 100644
--- a/tests/slicing/mark_all_slices.i
+++ b/tests/slicing/mark_all_slices.i
@@ -1,7 +1,7 @@
 /* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
-   OPT: @EVA_OPTIONS@ -deps -slicing-level 3 -no-slice-callers -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+   OPT: @EVA_OPTIONS@ -deps -slicing-level 3 -no-slice-callers
 */
 int A, B, C, D;
 int A2, B2, C2, D2;
diff --git a/tests/slicing/merge.i b/tests/slicing/merge.i
index b255a2c2fe73a442d5b5f2d56918a257aa820c91..568d5231c753b2cde6ea05638e214bceeaf6e4d5 100644
--- a/tests/slicing/merge.i
+++ b/tests/slicing/merge.i
@@ -1,7 +1,7 @@
 /* run.config
-   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-   CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/libAnim.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
-   OPT: @EVA_OPTIONS@ -deps -slicing-level 3 -journal-disable
+ MODULE: libSelect libAnim @PTEST_NAME@
+
+   OPT: @EVA_OPTIONS@ -deps -slicing-level 3
 */
 
 int G1, G2, G3;
diff --git a/tests/slicing/min_call.c b/tests/slicing/min_call.c
index 5e833483762d7496d8e66d6b48b4d2f4faf700bf..6ed48e08f236ab237a4607c2af6e03ce2ff73932 100644
--- a/tests/slicing/min_call.c
+++ b/tests/slicing/min_call.c
@@ -1,7 +1,7 @@
 /* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
-   OPT: @EVA_OPTIONS@ -deps -lib-entry -main g -journal-disable -slicing-level 3
+ MODULE: libSelect @PTEST_NAME@
+
+   OPT: @EVA_OPTIONS@ -deps -lib-entry -main g -slicing-level 3
 */
 
 /* dummy source file in order to test minimal calls feature
diff --git a/tests/slicing/select_by_annot.i b/tests/slicing/select_by_annot.i
index 500831ba3d7e8ad5422b4fa618fcba881964d090..6d0e19a38c40403d993cad4716cd7879bc37abfb 100644
--- a/tests/slicing/select_by_annot.i
+++ b/tests/slicing/select_by_annot.i
@@ -1,23 +1,23 @@
 /* run.config
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
- MODULE: @PTEST_NAME@
-   OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -journal-disable
+
+ MODULE: libSelect @PTEST_NAME@
+   OPT: @EVA_OPTIONS@ -deps -lib-entry -main main
+
  MODULE:
- CMD: bin/toplevel.opt
-   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 @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/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 @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/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 @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
-   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
-   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
-   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
-   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f4 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
-   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f5 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
-   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f6 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
-   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f7 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
-   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-loop-inv f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
-   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
-   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
-   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f9 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma main -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert main -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma modifS -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f1 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f2 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f3 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f4 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f5 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f6 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f7 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-loop-inv f8 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f8 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert f8 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+   OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f9 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_RESULT@/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
 
 */
 struct Tstr { int a; int b; } S;
diff --git a/tests/slicing/select_simple.c b/tests/slicing/select_simple.c
index de81f2fc724128d61174270a1dfdb78987911e02..735494d41697de1a77b4f56634bf92e50b53b9e7 100644
--- a/tests/slicing/select_simple.c
+++ b/tests/slicing/select_simple.c
@@ -1,7 +1,7 @@
 /* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
-   OPT: @EVA_OPTIONS@ -deps -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+   OPT: @EVA_OPTIONS@ -deps
 */
 
 /* dummy source file in order to test select_simple.ml */
diff --git a/tests/slicing/simple_intra_slice.i b/tests/slicing/simple_intra_slice.i
index 24d8beb4b839f37e584f372b545916a5800e3113..b3992a123e7847f5a3eb77064d497fa856ed7b4c 100644
--- a/tests/slicing/simple_intra_slice.i
+++ b/tests/slicing/simple_intra_slice.i
@@ -1,7 +1,7 @@
 /* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
-   OPT: @EVA_OPTIONS@ -deps -no-slice-callers -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+   OPT: @EVA_OPTIONS@ -deps -no-slice-callers
 */
 int Unknown;
 int G;
diff --git a/tests/slicing/slice_no_body.i b/tests/slicing/slice_no_body.i
index aebe5da2b2cb23538247faac17de8bfbf77049d8..79b40ad2e32fe96d32753d548d9f388df87fb26c 100644
--- a/tests/slicing/slice_no_body.i
+++ b/tests/slicing/slice_no_body.i
@@ -1,7 +1,7 @@
 /* run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
-   OPT: @EVA_OPTIONS@ -deps -lib-entry -main h -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+   OPT: @EVA_OPTIONS@ -deps -lib-entry -main h
 */
 
 int G;
diff --git a/tests/slicing/switch.i b/tests/slicing/switch.i
index 997d28ba40562aea8a428d04e66a550549ef0626..dfd7b56cf1c41fd021fc66af1fcf236f59ee69bb 100644
--- a/tests/slicing/switch.i
+++ b/tests/slicing/switch.i
@@ -1,7 +1,7 @@
 /*  run.config
- MODULE: @PTEST_NAME@
- CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs
-   OPT: @EVA_OPTIONS@ -deps -journal-disable
+ MODULE: libSelect @PTEST_NAME@
+
+   OPT: @EVA_OPTIONS@ -deps
 */
 int main (char choix) {
   int x = 0, y = 0, z = 0;
diff --git a/tests/slicing/test_config b/tests/slicing/test_config
index a709a3c91d35fd4abeee2660f7e99d245df4287e..1c214a23023446fa86e655de311a60df62051ceb 100644
--- a/tests/slicing/test_config
+++ b/tests/slicing/test_config
@@ -1,2 +1,3 @@
-EXECNOW: make -s tests/slicing/libSelect.cmxs tests/slicing/libAnim.cmxs
+MODULE: libSelect libAnim
+MODULE:
 OPT: @EVA_OPTIONS@ -machdep x86_32