Skip to content
Snippets Groups Projects
Commit 995f3a6f authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'feature/patrick/ptests' into 'master' 

[Ptests] simplifies macro expansion

See merge request frama-c/frama-c!3154
parents 07e2ed10 20835991
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 174 additions and 159 deletions
ptests/ptests.ml
+ 130
− 129
View file @ 995f3a6f
...@@ -588,23 +588,6 @@ end = struct ...@@ -588,23 +588,6 @@ end = struct
end 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 = module Macros =
struct struct
module StringMap = Map.Make (String) module StringMap = Map.Make (String)
...@@ -612,52 +595,55 @@ struct ...@@ -612,52 +595,55 @@ struct
type t = string StringMap.t 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 = let print_macros macros =
lock_printf "%% Macros (%d):@." (StringMap.cardinal macros); lock_printf "%% Macros (%d):@." (StringMap.cardinal macros);
StringMap.iter (fun key data -> lock_printf "%% - %s -> %s@." key data) macros; StringMap.iter (fun key data -> lock_printf "%% - %s -> %s@." key data) macros;
lock_printf "%% End macros@." lock_printf "%% End macros@."
let does_expand macros s = let does_expand =
if !verbosity >=4 then print_macros macros; let macro_regex = Str.regexp "@\\([-A-Za-z_0-9]+\\)@" in
let rec aux n (ptest_file_matched,s as acc) = fun macros s ->
if Str.string_match macro_regex s n then begin let has_ptest_file = ref false in
let macro = Str.matched_group 2 s in if !verbosity >= 3 then lock_printf "%% Expand: %s@." s;
let ptest_file_matched = ptest_file_matched || macro = "PTEST_FILE" in if !verbosity >= 4 then print_macros macros;
let start = Str.matched_group 1 s in let rec aux s =
let rest = Str.matched_group 3 s in let expand_macro = function
let new_n = Str.group_end 1 in | Str.Text s -> s
let n, new_s = | Str.Delim s ->
if macro = "" then begin if Str.string_match macro_regex s 0 then begin
new_n + 1, String.sub s 0 new_n ^ "@" ^ rest let macro = Str.matched_group 1 s in
end else begin try
try if !verbosity >= 4 then lock_printf "%% - macro is %s\n%!" macro;
if !verbosity >= 4 then lock_printf "%% - macro is %s\n%!" macro; let replacement = find macro macros in
let replacement = find macro macros in if String.(macro = "PTEST_FILE") then has_ptest_file := true;
if !verbosity >= 3 then if !verbosity >= 3 then
lock_printf "%% - replacement for %s is %s\n%!" macro replacement; lock_printf "%% - replacement for %s is %s\n%!" macro replacement;
new_n, aux replacement
String.sub s 0 n ^ start ^ replacement ^ rest with
with | Not_found -> s
| Not_found -> Str.group_end 2 + 1, s end
end else s
in in
if !verbosity >= 4 then lock_printf "%% - New string is %s\n%!" new_s; String.concat "" (List.map expand_macro (Str.full_split macro_regex s))
let new_acc = ptest_file_matched, new_s in in
if n <= String.length new_s then aux n new_acc else new_acc try
end else acc Mutex.lock str_mutex;
in let r = aux s in
Mutex.lock str_mutex; Mutex.unlock str_mutex;
try if !verbosity >= 3 then lock_printf "%% Expansion result: %s@." r;
let res = aux 0 (false,s) in !has_ptest_file, r
Mutex.unlock str_mutex; res with e ->
with e -> lock_eprintf "Uncaught exception %s\n%!" (Printexc.to_string e);
lock_eprintf "Uncaught exception %s\n%!" (Printexc.to_string e); Mutex.unlock str_mutex;
Mutex.unlock str_mutex; raise e
raise e
let expand macros s = let expand macros s =
snd (does_expand macros s) snd (does_expand macros s)
...@@ -676,6 +662,24 @@ struct ...@@ -676,6 +662,24 @@ struct
end 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. *) (** configuration of a directory/test. *)
type cmd = { type cmd = {
toplevel: string; toplevel: string;
...@@ -767,7 +771,7 @@ end = struct ...@@ -767,7 +771,7 @@ end = struct
dc_timeout = ""; 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) = let rec aux (s:execnow) =
try try
Scanf.sscanf s.ex_cmd "%_[ ]LOG%_[ ]%[-A-Za-z0-9_',+=:.\\@@]%_[ ]%s@\n" Scanf.sscanf s.ex_cmd "%_[ ]LOG%_[ ]%[-A-Za-z0-9_',+=:.\\@@]%_[ ]%s@\n"
...@@ -789,6 +793,7 @@ end = struct ...@@ -789,6 +793,7 @@ end = struct
in in
aux aux
{ ex_cmd = s; { ex_cmd = s;
ex_macros;
ex_log = []; ex_log = [];
ex_bin = []; ex_bin = [];
ex_dir = dir; ex_dir = dir;
...@@ -847,12 +852,12 @@ end = struct ...@@ -847,12 +852,12 @@ end = struct
(* how to process options *) (* how to process options *)
let config_exec ~once ~drop:_ ~file:_ dir s current = let config_exec ~once ~file:_ dir s current =
{ current with { current with
dc_execnow = 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 let regex = Str.regexp "[ \t]*\\([^ \t@]+\\)\\([ \t]+\\(.*\\)\\|$\\)" in
Mutex.lock str_mutex; Mutex.lock str_mutex;
if Str.string_match regex s 0 then begin if Str.string_match regex s 0 then begin
...@@ -872,18 +877,12 @@ end = struct ...@@ -872,18 +877,12 @@ end = struct
let set_load_modules deps macros = let set_load_modules deps macros =
let name = "PTEST_LOAD_MODULES" in let name = "PTEST_LOAD_MODULES" in
let def = List.fold_left (fun acc s -> let def = String.concat "," deps in
match acc with
| "" -> s
| acc -> s ^ "," ^ acc)
""
deps
in
if !verbosity >= 3 then if !verbosity >= 3 then
lock_printf "%% - Macro %s for -load-module with definition %s@." name def; lock_printf "%% - Macro %s for -load-module with definition %s@." name def;
Macros.add_list [name, def] macros 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 -> let deps,current = List.fold_left (fun ((deps,curr) as acc) s ->
if StringSet.mem s curr.dc_cmxs_module then acc if StringSet.mem s curr.dc_cmxs_module then acc
else else
...@@ -894,23 +893,23 @@ end = struct ...@@ -894,23 +893,23 @@ end = struct
if String.(deps = "") then current if String.(deps = "") then current
else else
let make_cmd = Macros.expand current.dc_macros "@PTEST_MAKE_MODULE@" in 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 s = Macros.expand current.dc_macros s in
let deps = List.map (fun s -> "@PTEST_DIR@/" ^ (Filename.remove_extension s) ^ ".cmxs") let deps = List.map (fun s -> "@PTEST_DIR@/" ^ (Filename.remove_extension s) ^ ".cmxs")
(str_split_list s) (str_split_list s)
in 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 } { current with dc_macros = set_load_modules deps current.dc_macros }
let config_options = let config_options =
[ "CMD", [ "CMD",
(fun ~drop:_ ~file:_ _ s current -> { current with dc_default_toplevel = s}); (fun ~file:_ _ s current -> { current with dc_default_toplevel = s});
"OPT", "OPT",
(fun ~drop ~file _ s current -> (fun ~file _ s current ->
if not (drop || current.dc_framac) then if not (current.dc_framac) then
lock_eprintf lock_eprintf
"%s: a NOFRAMAC directive has been defined before a sub-test defined by a 'OPT' directive (That NOFRAMAC directive could be misleading.).@." "%s: a NOFRAMAC directive has been defined before a sub-test defined by a 'OPT' directive (That NOFRAMAC directive could be misleading.).@."
file; file;
...@@ -927,19 +926,20 @@ end = struct ...@@ -927,19 +926,20 @@ end = struct
dc_commands = t :: current.dc_commands }); dc_commands = t :: current.dc_commands });
"STDOPT", "STDOPT",
(fun ~drop ~file _ s current -> (fun ~file _ s current ->
if not (drop || current.dc_framac) then if not current.dc_framac then
lock_eprintf lock_eprintf
"%s: a NOFRAMAC directive has been defined before a sub-test defined by a 'STDOPT' directive (That NOFRAMAC directive could be misleading.).@." "%s: a NOFRAMAC directive has been defined before a sub-test defined by a 'STDOPT' directive (That NOFRAMAC directive could be misleading.).@."
file; file;
let new_top = let new_top =
List.map List.map
(fun command -> (fun command ->
{ command with opts= make_custom_opts command.opts s; { toplevel = current.dc_default_toplevel;
logs= command.logs @ current.dc_default_log; opts= make_custom_opts command.opts s;
macros= current.dc_macros; logs= command.logs @ current.dc_default_log;
exit_code = current.dc_exit_code; macros= current.dc_macros;
timeout= current.dc_timeout exit_code = current.dc_exit_code;
timeout= current.dc_timeout
}) })
!default_parsing_env.current_default_cmds !default_parsing_env.current_default_cmds
in in
...@@ -947,10 +947,10 @@ end = struct ...@@ -947,10 +947,10 @@ end = struct
dc_default_log = !default_parsing_env.current_default_log }); dc_default_log = !default_parsing_env.current_default_log });
"FILEREG", "FILEREG",
(fun ~drop:_ ~file:_ _ s current -> { current with dc_test_regexp = s }); (fun ~file:_ _ s current -> { current with dc_test_regexp = s });
"FILTER", "FILTER",
(fun ~drop:_ ~file:_ _ s current -> (fun ~file:_ _ s current ->
let s = trim_right s in let s = trim_right s in
match current.dc_filter with match current.dc_filter with
| None when s="" -> { current with dc_filter = None } | None when s="" -> { current with dc_filter = None }
...@@ -958,18 +958,18 @@ end = struct ...@@ -958,18 +958,18 @@ end = struct
| Some filter -> { current with dc_filter = Some (s ^ " | " ^ filter) }); | Some filter -> { current with dc_filter = Some (s ^ " | " ^ filter) });
"EXIT", "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", "GCC",
(fun ~drop ~file _ _ acc -> (fun ~file _ _ acc ->
if not drop then lock_eprintf "%s: GCC directive (DEPRECATED)@." file; lock_eprintf "%s: GCC directive (DEPRECATED)@." file;
acc); acc);
"COMMENT", "COMMENT",
(fun ~drop:_ ~file:_ _ _ acc -> acc); (fun ~file:_ _ _ acc -> acc);
"DONTRUN", "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; "EXECNOW", config_exec ~once:true;
"EXEC", config_exec ~once:false; "EXEC", config_exec ~once:false;
...@@ -979,14 +979,14 @@ end = struct ...@@ -979,14 +979,14 @@ end = struct
"MODULE", config_module; "MODULE", config_module;
"LOG", "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", "TIMEOUT",
(fun ~drop:_ ~file:_ _ s current -> { current with dc_timeout = s }); (fun ~file:_ _ s current -> { current with dc_timeout = s });
"NOFRAMAC", "NOFRAMAC",
(fun ~drop ~file _ _ current -> (fun ~file _ _ current ->
if not drop && current.dc_commands <> [] && current.dc_framac then if current.dc_commands <> [] && current.dc_framac then
lock_eprintf lock_eprintf
"%s: a NOFRAMAC directive has the effect of ignoring previous defined sub-tests (by some 'OPT' or 'STDOPT' directives that seems misleading). @." "%s: a NOFRAMAC directive has the effect of ignoring previous defined sub-tests (by some 'OPT' or 'STDOPT' directives that seems misleading). @."
file; file;
...@@ -1004,7 +1004,9 @@ end = struct ...@@ -1004,7 +1004,9 @@ end = struct
Scanf.sscanf s "%[ *]%[A-Za-z0-9]: %s@\n" Scanf.sscanf s "%[ *]%[A-Za-z0-9]: %s@\n"
(fun _ name opt -> (fun _ name opt ->
try 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 -> with Not_found ->
lock_eprintf "@[%s: unknown configuration option: %s@\n%!@]" file name) lock_eprintf "@[%s: unknown configuration option: %s@\n%!@]" file name)
with with
...@@ -1093,7 +1095,7 @@ end ...@@ -1093,7 +1095,7 @@ end
type toplevel_command = type toplevel_command =
{ macros: Macros.t; { macros: Macros.t;
mutable log_files: string list; log_files: string list;
file : string ; file : string ;
nb_files : int ; nb_files : int ;
options : string ; options : string ;
...@@ -1172,7 +1174,7 @@ module Cmd : sig ...@@ -1172,7 +1174,7 @@ module Cmd : sig
val log_prefix : toplevel_command -> string val log_prefix : toplevel_command -> string
val oracle_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 (* [basic_command_string cmd] does not redirect the outputs, and does
not overwrite the result files *) not overwrite the result files *)
...@@ -1206,7 +1208,7 @@ end = struct ...@@ -1206,7 +1208,7 @@ end = struct
let get_ptest_file cmd = SubDir.make_file cmd.directory cmd.file let get_ptest_file cmd = SubDir.make_file cmd.directory cmd.file
let get_macros cmd = let expand_macros ~defaults cmd =
let ptest_config = let ptest_config =
if !special_config = "" then "" else "_" ^ !special_config if !special_config = "" then "" else "_" ^ !special_config
in in
...@@ -1225,7 +1227,17 @@ end = struct ...@@ -1225,7 +1227,17 @@ end = struct
"PTEST_NUMBER", string_of_int cmd.n; "PTEST_NUMBER", string_of_int cmd.n;
] ]
in 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 = let contains_frama_c_binary_name =
Str.regexp "[^( ]*\\(toplevel\\|viewer\\|frama-c-gui\\|frama-c[^-]\\).*" Str.regexp "[^( ]*\\(toplevel\\|viewer\\|frama-c-gui\\|frama-c[^-]\\).*"
...@@ -1235,9 +1247,7 @@ end = struct ...@@ -1235,9 +1247,7 @@ end = struct
let basic_command_string = let basic_command_string =
fun command -> fun command ->
let macros = get_macros command in let macros = command.macros in
let logfiles = List.map (Macros.expand macros) command.log_files in
command.log_files <- logfiles;
let has_ptest_file_t, toplevel = let has_ptest_file_t, toplevel =
Macros.does_expand macros command.toplevel Macros.does_expand macros command.toplevel
in in
...@@ -1314,9 +1324,7 @@ end = struct ...@@ -1314,9 +1324,7 @@ end = struct
update_oracle (log_prefix ^ ".res.log") (oracle_prefix ^ ".res.oracle"); update_oracle (log_prefix ^ ".res.log") (oracle_prefix ^ ".res.oracle");
update_oracle (log_prefix ^ ".err.log") (oracle_prefix ^ ".err.oracle"); update_oracle (log_prefix ^ ".err.log") (oracle_prefix ^ ".err.oracle");
(* Update files related to LOG directives *) (* Update files related to LOG directives *)
let macros = get_macros command in List.iter (update_log_files command.directory) command.log_files
let log_files = List.map (Macros.expand macros) command.log_files in
List.iter (update_log_files command.directory) log_files
end end
...@@ -1435,8 +1443,6 @@ let do_command command = ...@@ -1435,8 +1443,6 @@ let do_command command =
ignore (launch basic_command_string) ignore (launch basic_command_string)
end end
else begin 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 command_string = Cmd.command_string command in
let summary_ret = let summary_ret =
if !behavior <> Examine if !behavior <> Examine
...@@ -1932,7 +1938,7 @@ let dispatcher () = ...@@ -1932,7 +1938,7 @@ let dispatcher () =
fun {toplevel; opts=options; logs=log_files; macros; exit_code; timeout} -> fun {toplevel; opts=options; logs=log_files; macros; exit_code; timeout} ->
let n = !i in let n = !i in
incr i; incr i;
let cmd = Cmd.expand_macros ~defaults:config.dc_macros
{ file; options; toplevel; nb_files; directory; n; log_files; { file; options; toplevel; nb_files; directory; n; log_files;
filter = config.dc_filter; macros; filter = config.dc_filter; macros;
exit_code = begin exit_code = begin
...@@ -1945,12 +1951,6 @@ let dispatcher () = ...@@ -1945,12 +1951,6 @@ let dispatcher () =
execnow=false; execnow=false;
timeout; 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 in
let nb_files_execnow = List.length config.dc_execnow in let nb_files_execnow = List.length config.dc_execnow in
let make_execnow_cmd = let make_execnow_cmd =
...@@ -1958,29 +1958,30 @@ let dispatcher () = ...@@ -1958,29 +1958,30 @@ let dispatcher () =
fun execnow -> fun execnow ->
let n = !e in let n = !e in
incr e; incr e;
let cmd = { let cmd = Cmd.expand_macros ~defaults:config.dc_macros
file ; {file ;
nb_files = nb_files_execnow; nb_files = nb_files_execnow;
log_files = []; log_files = execnow.ex_log;
options = ""; options = "";
toplevel = execnow.ex_cmd; toplevel = execnow.ex_cmd;
exit_code = 0; exit_code = 0;
n; n;
directory; directory;
filter = None; (* No filter for execnow command *) filter = None; (* No filter for execnow command *)
macros = config.dc_macros; macros = execnow.ex_macros;
execnow = true; execnow = true;
timeout = execnow.ex_timeout; timeout = execnow.ex_timeout;
} in }
let macros = Cmd.get_macros cmd in in
let process_macros s = Macros.expand macros s in let process_macros s = Macros.expand cmd.macros s in
{ ex_cmd = Cmd.basic_command_string cmd; { 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_bin = List.map process_macros execnow.ex_bin;
ex_dir = execnow.ex_dir; ex_dir = execnow.ex_dir;
ex_once = execnow.ex_once; ex_once = execnow.ex_once;
ex_done = execnow.ex_done; ex_done = execnow.ex_done;
ex_timeout = execnow.ex_timeout; ex_timeout = cmd.timeout;
} }
in in
let treat_option q cmd = let treat_option q cmd =
......
src/plugins/e-acsl/tests/arith/bitwise.c
+ 1
− 1
View file @ 995f3a6f
/* run.config_ci, run.config_dev /* run.config_ci, run.config_dev
COMMENT: Support of bitwise operations 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 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> #include <limits.h>
......
src/plugins/e-acsl/tests/builtin/test_config_dev
+ 1
− 0
View file @ 995f3a6f
MACRO: ROOT_EACSL_GCC_OPTS_EXT --libc-replacements MACRO: ROOT_EACSL_GCC_OPTS_EXT --libc-replacements
STDOPT:
src/plugins/e-acsl/tests/format/test_config_dev
+ 1
− 0
View file @ 995f3a6f
MACRO: ROOT_EACSL_GCC_OPTS_EXT --validate-format-strings --full-mtracking -F -variadic-no-translation 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|" MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|/.*/share/e-acsl|FRAMAC_SHARE/e-acsl|"
STDOPT:
src/plugins/e-acsl/tests/full-mtracking/test_config_dev
+ 1
− 0
View file @ 995f3a6f
MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking
STDOPT:
src/plugins/e-acsl/tests/gmp-only/test_config_dev
+ 1
− 0
View file @ 995f3a6f
MACRO: ROOT_EACSL_GCC_OPTS_EXT --gmp MACRO: ROOT_EACSL_GCC_OPTS_EXT --gmp
STDOPT:
src/plugins/e-acsl/tests/special/e-acsl-instrument.c
+ 2
− 2
View file @ 995f3a6f
/* run.config_ci, run.config_dev /* run.config_ci, run.config_dev
COMMENT: test option -e-acsl-instrument; cannot run Eva on this example COMMENT: test option -e-acsl-instrument; cannot run Eva on this example
STDOPT:#"-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 MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -e-acsl-instrument @all,-uninstrument1,-uninstrument2
*/ */
#include <stdarg.h> #include <stdarg.h>
......
src/plugins/e-acsl/tests/temporal/test_config_dev
+ 1
− 0
View file @ 995f3a6f
MACRO: ROOT_EACSL_GCC_OPTS_EXT --temporal MACRO: ROOT_EACSL_GCC_OPTS_EXT --temporal
STDOPT:
src/plugins/e-acsl/tests/test_config_dev.in
+ 5
− 1
View file @ 995f3a6f
...@@ -4,16 +4,20 @@ MACRO: DEST @PTEST_RESULT@/@PTEST_NAME@ ...@@ -4,16 +4,20 @@ MACRO: DEST @PTEST_RESULT@/@PTEST_NAME@
MACRO: OUT @PTEST_NAME@.res.log MACRO: OUT @PTEST_NAME@.res.log
MACRO: ERR @PTEST_NAME@.err.log MACRO: ERR @PTEST_NAME@.err.log
MACRO: EACSL_ERR @PTEST_NAME@.e-acsl.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` 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 MACRO: ROOT_EACSL_GCC_ENABLE yes
COMMENT: Default options for `e-acsl-gcc.sh` COMMENT: Default options for `e-acsl-gcc.sh`
MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X
COMMENT: Default options for the frama-c invocation COMMENT: Default options for the frama-c invocation
MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0 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 COMMENT: Define the following macro in a test to pass extra options to the frama-c invocation
MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT
COMMENT: Define the following macro in a test to pass extra options to `e-acsl-gcc.sh` COMMENT: Define the following macro in a test to pass extra options to `e-acsl-gcc.sh`
MACRO: ROOT_EACSL_GCC_OPTS_EXT MACRO: ROOT_EACSL_GCC_OPTS_EXT
COMMENT: Define the following macro in a test to filter the output of the test execution COMMENT: Define the following macro in a test to filter the output of the test execution
MACRO: ROOT_EACSL_EXEC_FILTER cat 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
tests/misc/global_decl_loc.i
+ 2
− 1
View file @ 995f3a6f
/* run.config /* 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; int g;
tests/misc/global_decl_loc2.i
+ 2
− 3
View file @ 995f3a6f
/* run.config* /* run.config*
EXIT: 0 MODULE: global_decl_loc
OPT: @PTEST_DIR@/global_decl_loc.i
OPT: @PTEST_DIR@/global_decl_loc.i -load-module @PTEST_DIR@/global_decl_loc.cmxs
*/ */
extern int g; extern int g;
......
tests/misc/oracle/global_decl_loc.res.oracle
+ 1
− 1
View file @ 995f3a6f
[kernel] Parsing tests/misc/global_decl_loc.i (no preprocessing) [kernel] Parsing tests/misc/global_decl_loc.i (no preprocessing)
[kernel] Parsing tests/misc/global_decl_loc2.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
tests/misc/oracle/global_decl_loc2.res.oracle
+ 1
− 1
View file @ 995f3a6f
[kernel] Parsing tests/misc/global_decl_loc2.i (no preprocessing) [kernel] Parsing tests/misc/global_decl_loc2.i (no preprocessing)
[kernel] Parsing tests/misc/global_decl_loc.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
tests/misc/test_config
+ 2
− 1
View file @ 995f3a6f
EXECNOW: make -s @PTEST_DIR@/global_decl_loc.cmxs MODULE: global_decl_loc
MODULE:
tests/pdg/dyn_dpds.c
+ 2
− 2
View file @ 995f3a6f
/* run.config /* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs MODULE: @PTEST_NAME@
STDOPT: +"-load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -deps" STDOPT: +"-deps"
*/ */
......
tests/saveload/basic.i
+ 3
− 3
View file @ 995f3a6f
/* run.config /* run.config
MODULE: @PTEST_NAME@ 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.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
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
MODULE: 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" STDOPT: +"-load ./tests/saveload/result/basic.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable"
MODULE: @PTEST_NAME@ MODULE: @PTEST_NAME@
STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable -print" STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable -print"
MODULE: MODULE:
STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable" STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable"
MODULE: status 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" STDOPT: +"-load ./tests/saveload/result/status.sav"
MODULE: MODULE:
STDOPT: +"-load ./tests/saveload/result/status.sav" STDOPT: +"-load ./tests/saveload/result/status.sav"
......
tests/saveload/deps.i
+ 11
− 7
View file @ 995f3a6f
/* run.config /* 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 MODULE: deps_A
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 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-module ./tests/saveload/deps_A -load ./tests/saveload/result/deps.sav -eva @EVA_OPTIONS@ -out -input -deps " STDOPT: +"-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 " MODULE: deps_B
STDOPT: +"-load-module ./tests/saveload/deps_C -load ./tests/saveload/result/deps.sav -out -input -deps " STDOPT: +"-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 " MODULE: deps_C
STDOPT: +"-load-module ./tests/saveload/deps_E -load ./tests/saveload/result/deps.sav -out -input -deps " 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() { int main() {
......
tests/saveload/oracle/deps_sav.res
+ 2
− 2
View file @ 995f3a6f
...@@ -4,8 +4,8 @@ ...@@ -4,8 +4,8 @@
[eva] Initial state computed [eva] Initial state computed
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
[eva] tests/saveload/deps.i:15: starting to merge loop iterations [eva] tests/saveload/deps.i:19: starting to merge loop iterations
[eva:alarm] tests/saveload/deps.i:15: Warning: [eva:alarm] tests/saveload/deps.i:19: Warning:
signed overflow. assert -2147483648 ≤ i - 1; signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for main [eva] Recording results for main
[eva] done for function main [eva] done for function main
......
tests/saveload/serialized_queue.i
+ 2
− 2
View file @ 995f3a6f
/* run.config /* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs MODULE: @PTEST_NAME@
OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs OPT:
*/ */
// empty C file, we're only interested in the script itself // empty C file, we're only interested in the script itself
tests/slicing/adpcm.c
+ 3
− 3
View file @ 995f3a6f
/* run.config /* run.config
MODULE: @PTEST_NAME@ MODULE: libSelect @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 OPT: @EVA_OPTIONS@ -machdep x86_32 -ulevel -1 -deps -slicing-level 2
*/ */
#include "../test/adpcm.c" #include "../test/adpcm.c"
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment