diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 74d172f88e461db99ab816cd07f748ac071325b6..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,6 +595,12 @@ struct
type t = string StringMap.t
+ let add_defaults ~defaults macros =
+ StringMap.merge (fun _k default cur ->
+ match cur with
+ | Some _ -> cur
+ | _ -> default) defaults macros
+
let empty = StringMap.empty
let print_macros macros =
@@ -673,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;
@@ -764,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"
@@ -786,6 +793,7 @@ end = struct
in
aux
{ ex_cmd = s;
+ ex_macros;
ex_log = [];
ex_bin = [];
ex_dir = dir;
@@ -847,7 +855,7 @@ end = struct
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 ~file _dir s current =
let regex = Str.regexp "[ \t]*\\([^ \t@]+\\)\\([ \t]+\\(.*\\)\\|$\\)" in
@@ -869,13 +877,7 @@ 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
@@ -1172,7 +1174,7 @@ module Cmd : sig
val log_prefix : toplevel_command -> string
val oracle_prefix : toplevel_command -> string
- val expand_macros : toplevel_command -> toplevel_command
+ 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 expand_macros cmd =
+ let expand_macros ~defaults cmd =
let ptest_config =
if !special_config = "" then "" else "_" ^ !special_config
in
@@ -1226,6 +1228,7 @@ end = struct
]
in
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;
@@ -1935,7 +1938,7 @@ let dispatcher () =
fun {toplevel; opts=options; logs=log_files; macros; exit_code; timeout} ->
let n = !i in
incr i;
- Cmd.expand_macros
+ Cmd.expand_macros ~defaults:config.dc_macros
{ file; options; toplevel; nb_files; directory; n; log_files;
filter = config.dc_filter; macros;
exit_code = begin
@@ -1955,7 +1958,7 @@ let dispatcher () =
fun execnow ->
let n = !e in
incr e;
- let cmd = Cmd.expand_macros
+ let cmd = Cmd.expand_macros ~defaults:config.dc_macros
{file ;
nb_files = nb_files_execnow;
log_files = execnow.ex_log;
@@ -1965,13 +1968,14 @@ let dispatcher () =
n;
directory;
filter = None; (* No filter for execnow command *)
- macros = config.dc_macros;
+ 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_macros = cmd.macros;
ex_log = cmd.log_files;
ex_bin = List.map process_macros execnow.ex_bin;
ex_dir = execnow.ex_dir;
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/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/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"