Skip to content
Snippets Groups Projects
Commit fadd858a authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[ptests] closer to master branch

parent 4f063dbd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
ptests/ptests.ml
+ 165
− 116
View file @ fadd858a
...@@ -37,6 +37,7 @@ type env_t = { ...@@ -37,6 +37,7 @@ type env_t = {
config: string config: string
; dir: string ; dir: string
; dune_alias: string ; dune_alias: string
; absolute_tests_dir: string
} }
module Filename = struct module Filename = struct
...@@ -130,14 +131,17 @@ let is_file_empty_or_nonexisting filename = ...@@ -130,14 +131,17 @@ let is_file_empty_or_nonexisting filename =
let config_name ~env name = let config_name ~env name =
if env.config = "" then name else name ^ "_" ^ env.config if env.config = "" then name else name ^ "_" ^ env.config
let macro_default_options = ref "-journal-disable -check -no-autoload-plugins" let macro_post_options = ref "" (* value set to @PTEST_POST_OPTIONS@ macro *)
let macro_pre_options = ref "" (* value set to @PTEST_PRE_OPTIONS@ macro *)
let macro_options = ref "@PTEST_PRE_OPTIONS@ @PTEST_OPT@ @PTEST_POST_OPTIONS@"
let macro_default_options = ref "-journal-disable -check -no-autoload-plugins -add-symbolic-path @PTEST_SESSION@"
let macro_frama_c_exe = ref "frama-c" let macro_frama_c_exe = ref "frama-c"
let macro_frama_c_only = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@" let macro_frama_c_cmd = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@"
let macro_frama_c_cmd = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@" let macro_frama_c = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@"
let macro_frama_c = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@ @PTEST_FILE@"
let macro_frama_c_share = ref "../../../../install/default/share/frama-c/share" let macro_frama_c_share = ref "../../../../install/default/share/frama-c/share"
let default_toplevel = ref "@frama-c@ @PTEST_OPTIONS@" let default_toplevel = ref "@frama-c@"
(** the files in [suites] whose name matches (** the files in [suites] whose name matches
the pattern [test_file_regexp] will be considered as test files *) the pattern [test_file_regexp] will be considered as test files *)
...@@ -210,7 +214,6 @@ let example_msg = ...@@ -210,7 +214,6 @@ let example_msg =
@@PTEST_LOAD_OPTIONS@@ # The current list of options related to PLUGIN, MODULE, SCRIPT and LIBS to load.@ \ @@PTEST_LOAD_OPTIONS@@ # The current list of options related to PLUGIN, MODULE, SCRIPT and LIBS to load.@ \
@@PTEST_OPTIONS@@ # The current list of options related to OPT and STDOPT directives (for CMD directives).@ \ @@PTEST_OPTIONS@@ # The current list of options related to OPT and STDOPT directives (for CMD directives).@ \
@@frama-c-exe@@ # Shortcut defined as follow: %s@ \ @@frama-c-exe@@ # Shortcut defined as follow: %s@ \
@@frama-c-only@@ # Shortcut defined as follow: %s@ \
@@frama-c@@ # Shortcut defined as follow: %s@ \ @@frama-c@@ # Shortcut defined as follow: %s@ \
@@frama-c-cmd@@ # Shortcut defined as follow: %s@ \ @@frama-c-cmd@@ # Shortcut defined as follow: %s@ \
@@FRAMAC_SHARE@@ # Shortcut defined as follow: %s@ \ @@FRAMAC_SHARE@@ # Shortcut defined as follow: %s@ \
...@@ -244,7 +247,6 @@ let example_msg = ...@@ -244,7 +247,6 @@ let example_msg =
@]" @]"
!macro_default_options !macro_default_options
!macro_frama_c_exe !macro_frama_c_exe
!macro_frama_c_only
!macro_frama_c !macro_frama_c
!macro_frama_c_cmd !macro_frama_c_cmd
!macro_frama_c_share !macro_frama_c_share
...@@ -273,16 +275,20 @@ let rec argspec = ...@@ -273,16 +275,20 @@ let rec argspec =
("-adds-default-options" , Arg.String (fun s -> macro_default_options := !macro_default_options ^ " " ^ s), ("-adds-default-options" , Arg.String (fun s -> macro_default_options := !macro_default_options ^ " " ^ s),
" <options> Appends the <options> to the default value of the @PTEST_DEFAULT_OPTIONS@ macro"); " <options> Appends the <options> to the default value of the @PTEST_DEFAULT_OPTIONS@ macro");
("-add-options-pre", Arg.String (fun s -> macro_pre_options := !macro_pre_options ^ " " ^ s),
"<options> Add additional options to be passed to the toplevels \
that will be launched. <options> are added before standard test options.");
("-add-options-post", Arg.String (fun s -> macro_post_options := !macro_post_options ^ " " ^ s),
"<options> Add additional options to be passed to the toplevels \
that will be launched. <options> are added after standard test options");
("-macro-default-options" , Arg.String (fun s -> macro_default_options := s), ("-macro-default-options" , Arg.String (fun s -> macro_default_options := s),
" <value> Set the default value of the @PTEST_DEFAULT_OPTIONS@ macro (defaults to "^ !macro_default_options ^")"); " <value> Set the default value of the @PTEST_DEFAULT_OPTIONS@ macro (defaults to "^ !macro_default_options ^")");
("-macro-frama-c-exe", Arg.String (fun s -> macro_frama_c_exe := s), ("-macro-frama-c-exe", Arg.String (fun s -> macro_frama_c_exe := s),
" <value> Set the default value of the @frama-c-exe@ macro (defaults to "^ !macro_frama_c_exe ^")"); " <value> Set the default value of the @frama-c-exe@ macro (defaults to "^ !macro_frama_c_exe ^")");
("-macro-frama-c-only", Arg.String (fun s -> macro_frama_c_only := s), ("-macro-frama-c-cmd", Arg.String (fun s -> macro_frama_c_cmd := s),
" <value> Set the default value of the @frama-c-only@ macro (defaults to "^ !macro_frama_c_only ^")");
("-macro-frama-c-cmd", Arg.String (fun s -> macro_frama_c_only := s),
" <value> Set the default value of the @frama-c-cmd@ macro (defaults to "^ !macro_frama_c_cmd ^")"); " <value> Set the default value of the @frama-c-cmd@ macro (defaults to "^ !macro_frama_c_cmd ^")");
("-macro-frama-c", Arg.String (fun s -> macro_frama_c_only := s), ("-macro-frama-c", Arg.String (fun s -> macro_frama_c := s),
" <value> Set the @frama-c@ macro (defaults to "^ !macro_frama_c ^")"); " <value> Set the @frama-c@ macro (defaults to "^ !macro_frama_c ^")");
("-dune-alias", Arg.String (fun s -> default_dune_alias := s), ("-dune-alias", Arg.String (fun s -> default_dune_alias := s),
...@@ -509,18 +515,23 @@ type does_expand = { ...@@ -509,18 +515,23 @@ type does_expand = {
StringMap.add name (get name macros ^ expand macros def) macros StringMap.add name (get name macros ^ expand macros def) macros
let default_macros = add_list let default_macros = add_list
[ "PTEST_DEPS", ""; [ "frama-c-exe", !macro_frama_c_exe;
"frama-c-cmd", !macro_frama_c_cmd;
"frama-c", !macro_frama_c;
"DEV_NULL", dev_null;
"FRAMAC_SHARE",!macro_frama_c_share;
"PTEST_DEFAULT_OPTIONS", !macro_default_options;
"PTEST_OPTIONS", !macro_options;
"PTEST_PRE_OPTIONS", !macro_pre_options;
"PTEST_POST_OPTIONS", !macro_post_options;
"PTEST_DEPS", "";
"PTEST_LIBS", ""; "PTEST_LIBS", "";
"PTEST_MODULE", ""; "PTEST_MODULE", "";
"PTEST_SCRIPT", ""; "PTEST_SCRIPT", "";
"PTEST_PLUGIN", ""; "PTEST_PLUGIN", "";
"PTEST_DEFAULT_OPTIONS", !macro_default_options;
"frama-c-exe", !macro_frama_c_exe;
"frama-c-only", !macro_frama_c_only;
"frama-c-cmd", !macro_frama_c_cmd;
"frama-c", !macro_frama_c;
"FRAMAC_SHARE",!macro_frama_c_share;
"DEV_NULL", dev_null;
] empty ] empty
end end
...@@ -602,7 +613,8 @@ end = struct ...@@ -602,7 +613,8 @@ end = struct
let ptest_file = Filename.sanitize file in let ptest_file = Filename.sanitize file in
let ptest_name = Filename.remove_extension file in let ptest_name = Filename.remove_extension file in
let ptest_vars = let ptest_vars =
[ "PTEST_CONFIG", ptest_config; [ "PTEST_SESSION", env.absolute_tests_dir ^ "/_build/default:.";
"PTEST_CONFIG", ptest_config;
"PTEST_DIR", "."; "PTEST_DIR", ".";
"PTEST_RESULT", "."; "PTEST_RESULT", ".";
"PTEST_SUITE_DIR", ".."; "PTEST_SUITE_DIR", "..";
...@@ -1104,14 +1116,35 @@ let basic_command_string command = ...@@ -1104,14 +1116,35 @@ let basic_command_string command =
in in
let macros = (* set expanded macros that can be used into CMD directives *) let macros = (* set expanded macros that can be used into CMD directives *)
Macros.add_list [ Macros.add_list [
"PTEST_OPTIONS", Macros.expand command.macros command.options; "PTEST_OPT", Macros.expand command.macros command.options;
"PTEST_LOAD_OPTIONS", plugins_options; "PTEST_LOAD_OPTIONS", plugins_options;
] command.macros in ] command.macros in
let raw_command = Macros.expand macros command.toplevel in let toplevel =
if command.timeout = "" then raw_command let in_toplevel,toplevel = Macros.does_expand macros command.toplevel in
else "ulimit -t " ^ command.timeout ^ " && " ^ raw_command if command.execnow || in_toplevel.has_ptest_opt then toplevel
else begin
let has_ptest_file,options =
let in_option,options = Macros.does_expand macros command.options in
(in_option.has_ptest_file || in_toplevel.has_ptest_file),
(if in_toplevel.has_frama_c_exe then
[ Macros.expand macros "@PTEST_PRE_OPTIONS@" ;
options ;
Macros.expand macros "@PTEST_POST_OPTIONS@" ;
]
else [ options ])
in
let options = List.filter (fun s -> s <> "") options in
let options = if has_ptest_file then options
else (Filename.basename command.file)::options
in
String.concat " " (toplevel::options)
end
in
let raw_command = if command.timeout = "" then toplevel
else "ulimit -t " ^ command.timeout ^ " && " ^ toplevel
in raw_command
let print_list fmt l = List.iter (Format.fprintf fmt " %S") l let pp_list fmt l = List.iter (Format.fprintf fmt " %S") l
module Fmt = struct module Fmt = struct
let plugin_as_package fmt s = Format.fprintf fmt "frama-c-%s" s let plugin_as_package fmt s = Format.fprintf fmt "frama-c-%s" s
let quote pr fmt s = Format.fprintf fmt "%S" (Format.asprintf "%a" pr s) let quote pr fmt s = Format.fprintf fmt "%S" (Format.asprintf "%a" pr s)
...@@ -1119,6 +1152,11 @@ module Fmt = struct ...@@ -1119,6 +1152,11 @@ module Fmt = struct
let var_libavailable pr fmt s = Format.fprintf fmt "%%{lib-available:%a}" pr s let var_libavailable pr fmt s = Format.fprintf fmt "%%{lib-available:%a}" pr s
let package_as_deps pr fmt s = Format.fprintf fmt "(package %a)" pr s let package_as_deps pr fmt s = Format.fprintf fmt "(package %a)" pr s
end end
let pp_command_deps fmt command =
Format.fprintf fmt "%a %S (package frama-c)%a"
pp_list command.deps.deps_cmd
command.file
Fmt.(list (package_as_deps (quote plugin_as_package))) command.deps.load_plugin
let show_cmd = let show_cmd =
let regexp = Str.regexp "%{[a-z]+:\\([^}]+\\)}" in let regexp = Str.regexp "%{[a-z]+:\\([^}]+\\)}" in
...@@ -1206,7 +1244,6 @@ let command_string ~env ~result_fmt ~oracle_fmt command = ...@@ -1206,7 +1244,6 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
| None -> reslog,errlog | None -> reslog,errlog
| Some _ -> (log_prefix ^ ".res.unfiltered-log"),(log_prefix ^ ".err.unfiltered-log") | Some _ -> (log_prefix ^ ".res.unfiltered-log"),(log_prefix ^ ".err.unfiltered-log")
in in
let deps = command.deps in
let accepted_exit_code = Format.sprintf "with-accepted-exit-codes %d" command.exit_code in let accepted_exit_code = Format.sprintf "with-accepted-exit-codes %d" command.exit_code in
let command_string = basic_command_string command in let command_string = basic_command_string command in
let filter_res,filter_err,wtest = let filter_res,filter_err,wtest =
...@@ -1253,29 +1290,27 @@ let command_string ~env ~result_fmt ~oracle_fmt command = ...@@ -1253,29 +1290,27 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
"(rule ; %s\n \ "(rule ; %s\n \
(alias %S)\n \ (alias %S)\n \
(targets %S %S %a)\n \ (targets %S %S %a)\n \
(deps %S %S %a %a %S (package frama-c)%a)\n \ (deps %S %S %a %a)\n \
(action (run %s %%{dep:%s} %S %a))\n\ (action (run %s %%{dep:%s} %S %a))\n\
)@." )@."
(* rules: *) (* rule: *)
wtest.info wtest.info
(* alias *) (* alias: *)
wrapper_basename wrapper_basename
(* targets: *) (* targets: *)
cmderrlog cmderrlog
cmdreslog cmdreslog
print_list command.log_files pp_list command.log_files
(* deps: *) (* deps: *)
wtest.oracle_out wtest.oracle_out
wtest.oracle_err wtest.oracle_err
print_list (List.map (Filename.concat wtest.oracle_dir) command.log_files) pp_list (List.map (Filename.concat wtest.oracle_dir) command.log_files)
print_list deps.deps_cmd pp_command_deps command
command.file
Fmt.(list (package_as_deps (quote plugin_as_package))) command.deps.load_plugin
(* action: *) (* action: *)
!wrapper_cmd !wrapper_cmd
wrapper_basename wrapper_basename
wtest.cmd wtest.cmd
print_list (if command.filter = None then [] else [wtest.sedout ; wtest.sederr]); pp_list (if command.filter = None then [] else [wtest.sedout ; wtest.sederr]);
let wtest = let wtest =
{ wtest with { wtest with
...@@ -1293,21 +1328,19 @@ let command_string ~env ~result_fmt ~oracle_fmt command = ...@@ -1293,21 +1328,19 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
"(rule ; %s\n \ "(rule ; %s\n \
(alias %S)\n \ (alias %S)\n \
(targets %S %S %a)\n \ (targets %S %S %a)\n \
(deps %a %S (package frama-c)%a)\n \ (deps %a)\n \
(action (with-stderr-to %S (with-stdout-to %S (%s (system %S)))))\n\ (action (with-stderr-to %S (with-stdout-to %S (%s (system %S)))))\n\
)@." )@."
(* rules: *) (* rule: *)
wtest.info wtest.info
(* alias *) (* alias: *)
wrapper_basename wrapper_basename
(* targets: *) (* targets: *)
cmderrlog cmderrlog
cmdreslog cmdreslog
print_list command.log_files pp_list command.log_files
(* deps: *) (* deps: *)
print_list deps.deps_cmd pp_command_deps command
command.file
Fmt.(list (package_as_deps (quote plugin_as_package))) command.deps.load_plugin
(* action: *) (* action: *)
cmderrlog cmderrlog
cmdreslog cmdreslog
...@@ -1321,12 +1354,13 @@ let command_string ~env ~result_fmt ~oracle_fmt command = ...@@ -1321,12 +1354,13 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(deps %S) (deps %S)
(action (with-stdout-to %S (with-accepted-exit-codes (or 0 1 2 125) (system %S))))\n\ (action (with-stdout-to %S (with-accepted-exit-codes (or 0 1 2 125) (system %S))))\n\
)@." )@."
(* rule: *)
txt txt
command.nth command.nth
command.file command.file
(* deps *) (* deps: *)
fin fin
(*action *) (* action: *)
fout cmd fout cmd
in in
filter_rule "RES" cmdreslog reslog filter_res ; filter_rule "RES" cmdreslog reslog filter_res ;
...@@ -1337,36 +1371,43 @@ let command_string ~env ~result_fmt ~oracle_fmt command = ...@@ -1337,36 +1371,43 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(alias %s)\n \ (alias %s)\n \
(action (diff %S %S))\n\ (action (diff %S %S))\n\
)@." )@."
(* rule: *)
n command.nth command.file n command.nth command.file
(* alias: *)
(ptests_alias ~env) (ptests_alias ~env)
(* action: *)
(SubDir.make_file (SubDir.oracle_subdir ~env SubDir.upper_dir) log) (SubDir.make_file (SubDir.oracle_subdir ~env SubDir.upper_dir) log)
log log
) command.log_files; ) command.log_files;
Format.fprintf result_fmt Format.fprintf result_fmt
"(rule ; REPRODUCE TEST #%d OF TEST FILE %S\n \ "(rule ; REPRODUCE TEST #%d OF TEST FILE %S\n \
(alias %S)\n \ (alias %S)\n \
(deps %a %S (package frama-c)%a (universe))\n \ (deps %a (universe))\n \
(action (%s (system %S)))\n\ (action (%s (system %S)))\n\
)@." )@."
(* rule: *)
command.nth command.file command.nth command.file
(* alias: *)
(mk_alias command "exec") (mk_alias command "exec")
print_list deps.deps_cmd (* deps: *)
command.file pp_command_deps command
Fmt.(list (package_as_deps (quote plugin_as_package))) command.deps.load_plugin (* action: *)
accepted_exit_code accepted_exit_code
command_string command_string
; ;
Format.fprintf result_fmt Format.fprintf result_fmt
"(rule ; SHOW TEST COMMAND #%d OF TEST FILE %S\n \ "(rule ; SHOW TEST COMMAND #%d OF TEST FILE %S\n \
(alias %S)\n \ (alias %S)\n \
(deps %a %S (package frama-c)%a (universe))\n \ (deps %a (universe))\n \
(action (system %S))\n\ (action (system %S))\n\
)@." )@."
(* rule: *)
command.nth command.file command.nth command.file
(* alias: *)
(mk_alias command "exec.show") (mk_alias command "exec.show")
print_list deps.deps_cmd (* deps: *)
command.file pp_command_deps command (* to get an updated build even in case of using the result *)
Fmt.(list (package_as_deps (quote plugin_as_package))) command.deps.load_plugin (* action: *)
("echo '" ^ show_cmd wtest.cmd ^"'"); ("echo '" ^ show_cmd wtest.cmd ^"'");
let diff_alias = log_prefix ^ ".diff" in let diff_alias = log_prefix ^ ".diff" in
...@@ -1376,7 +1417,9 @@ let command_string ~env ~result_fmt ~oracle_fmt command = ...@@ -1376,7 +1417,9 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(alias %S)\n \ (alias %S)\n \
(action (diff %S %S))\n\ (action (diff %S %S))\n\
)@." )@."
(* alias: *)
diff_alias diff_alias
(* action: *)
wtest.oracle_out wtest.oracle_out
reslog; reslog;
Format.fprintf result_fmt Format.fprintf result_fmt
...@@ -1384,7 +1427,9 @@ let command_string ~env ~result_fmt ~oracle_fmt command = ...@@ -1384,7 +1427,9 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(alias %S)\n \ (alias %S)\n \
(action (diff %S %S))\n\ (action (diff %S %S))\n\
)@." )@."
diff_alias (* alias: *)
diff_alias
(* action: *)
wtest.oracle_err wtest.oracle_err
errlog; errlog;
Format.fprintf result_fmt Format.fprintf result_fmt
...@@ -1400,36 +1445,36 @@ let command_string ~env ~result_fmt ~oracle_fmt command = ...@@ -1400,36 +1445,36 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
List.iter (oracle_target oracle_fmt oracle_subdir) command.log_files ; List.iter (oracle_target oracle_fmt oracle_subdir) command.log_files ;
() ()
(** process a test file *) let deps_command macros deps =
let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules = let subst = Macros.expand macros in
let load_plugin = List.map subst deps.load_plugin in
let load_module = List.map subst deps.load_module in
let load_libs = List.map (fun s -> (subst s)^".cmxs") deps.load_libs in
let deps_cmd = List.map subst deps.deps_cmd in
{ load_plugin; load_module; load_libs;
deps_cmd = load_libs @ load_module @ deps_cmd;
}
let update_modules file modules deps =
if deps.load_module <> [] then begin
let plugin_libs = StringSet.union
(StringSet.of_list (List.map (Format.sprintf "frama-c-%s.core") deps.load_plugin))
(StringSet.of_list (List.map (fun s -> Filename.remove_extension (Filename.basename s))
deps.load_libs))
in
List.iter (fun cmxs ->
let cmxs = Filename.remove_extension cmxs in
modules := StringMap.update cmxs (function
| None -> Some (plugin_libs,[file])
| Some (set,files) -> Some ((StringSet.inter set plugin_libs),file::files)
) !modules) (StringSet.elements (StringSet.of_list deps.load_module));
end
(** process a test file *)
let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
let config = Test_config.scan_test_file ~env directory ~file config in let config = Test_config.scan_test_file ~env directory ~file config in
if not config.dc_dont_run then if not config.dc_dont_run then
let test_name,config,ptest_vars = Test_config.ptest_vars ~env directory ~file config in let test_name,config,ptest_vars = Test_config.ptest_vars ~env directory ~file config in
let deps_command macros deps =
let subst = Macros.expand macros in
let load_plugin = List.map subst deps.load_plugin in
let load_module = List.map subst deps.load_module in
let load_libs = List.map (fun s -> (subst s)^".cmxs") deps.load_libs in
let deps_cmd = List.map subst deps.deps_cmd in
{ load_plugin; load_module; load_libs;
deps_cmd = load_libs @ load_module @ deps_cmd;
};
in
let update_modules deps =
if deps.load_module <> [] then begin
let plugin_libs = StringSet.union
(StringSet.of_list (List.map (Format.sprintf "frama-c-%s.core") deps.load_plugin))
(StringSet.of_list (List.map (fun s -> Filename.remove_extension (Filename.basename s))
deps.load_libs))
in
List.iter (fun cmxs ->
let cmxs = Filename.remove_extension cmxs in
modules := StringMap.update cmxs (function
| None -> Some (plugin_libs,[file])
| Some (set,files) -> Some ((StringSet.inter set plugin_libs),file::files)
) !modules) (StringSet.elements (StringSet.of_list deps.load_module));
end
in
let nb_files = List.length config.dc_commands in let nb_files = List.length config.dc_commands in
let make_cmd = let make_cmd =
let i = ref 0 in let i = ref 0 in
...@@ -1439,7 +1484,7 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules = ...@@ -1439,7 +1484,7 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules =
let macros = ptest_vars ~nth macros in let macros = ptest_vars ~nth macros in
let log_files = List.map (Macros.expand macros) logs in let log_files = List.map (Macros.expand macros) logs in
let deps = deps_command macros deps in let deps = deps_command macros deps in
update_modules deps; update_modules file modules deps;
command_string ~env ~result_fmt ~oracle_fmt command_string ~env ~result_fmt ~oracle_fmt
{ test_name ; file; options; toplevel; nb_files; directory; nth; timeout; { test_name ; file; options; toplevel; nb_files; directory; nth; timeout;
macros; log_files; macros; log_files;
...@@ -1463,9 +1508,9 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules = ...@@ -1463,9 +1508,9 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules =
let nth = !e in let nth = !e in
incr e ; incr e ;
let macros = ptest_vars ~nth Macros.empty in let macros = ptest_vars ~nth Macros.empty in
let deps = deps_command macros execnow.ex_deps in
update_modules deps;
let cmd = let cmd =
let deps = deps_command macros execnow.ex_deps in
update_modules file modules deps;
{ test_name; file; nb_files = nb_files_execnow; directory; nth; { test_name; file; nb_files = nb_files_execnow; directory; nth;
log_files = []; log_files = [];
options = ""; options = "";
...@@ -1478,12 +1523,13 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules = ...@@ -1478,12 +1523,13 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules =
deps = deps; deps = deps;
} }
in in
let cmd_string = basic_command_string cmd in
let wtest = { let wtest = {
default_wtest with default_wtest with
dir = SubDir.get (SubDir.result_subdir ~env cmd.directory) ; dir = SubDir.get (SubDir.result_subdir ~env cmd.directory) ;
info = Format.sprintf "EXECNOW #%d OF TEST FILE %s/%s" info = Format.sprintf "EXECNOW #%d OF TEST FILE %s/%s"
nth (SubDir.get directory) file; nth (SubDir.get directory) file;
cmd = basic_command_string cmd; cmd = cmd_string;
log = List.map (Macros.expand cmd.macros) execnow.ex_log; log = List.map (Macros.expand cmd.macros) execnow.ex_log;
bin = List.map (Macros.expand cmd.macros) execnow.ex_bin; bin = List.map (Macros.expand cmd.macros) execnow.ex_bin;
} }
...@@ -1493,22 +1539,21 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules = ...@@ -1493,22 +1539,21 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules =
Format.fprintf result_fmt Format.fprintf result_fmt
"(rule ; %s\n \ "(rule ; %s\n \
(alias %s)\n \ (alias %s)\n \
(deps %a %a %a (package frama-c)%a)\n \ (deps %a %a %a)\n \
(targets %a %a)\n \ (targets %a %a)\n \
(action (run %s %%{dep:%s} %S))\n\ (action (run %s %%{dep:%s} %S))\n\
)@." )@."
(* rules: *) (* rule: *)
wtest.info wtest.info
(* alias *) (* alias: *)
wrapper_basename wrapper_basename
(* deps: *) (* deps: *)
print_list (List.map (Filename.concat wtest.oracle_dir) wtest.log) pp_list (List.map (Filename.concat wtest.oracle_dir) wtest.log)
print_list (List.map (Filename.concat wtest.oracle_dir) wtest.bin) pp_list (List.map (Filename.concat wtest.oracle_dir) wtest.bin)
print_list cmd.deps.deps_cmd pp_command_deps cmd
Fmt.(list (package_as_deps (quote plugin_as_package))) cmd.deps.load_plugin
(* targets: *) (* targets: *)
print_list wtest.log pp_list wtest.log
print_list wtest.bin pp_list wtest.bin
(* action: *) (* action: *)
!wrapper_cmd !wrapper_cmd
wrapper_basename wrapper_basename
...@@ -1530,16 +1575,16 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules = ...@@ -1530,16 +1575,16 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules =
(targets %a %a)\n \ (targets %a %a)\n \
(action (system %S))\n\ (action (system %S))\n\
)@." )@."
(* rules: *) (* rule: *)
wtest.info wtest.info
(* alias *) (* alias: *)
wrapper_basename wrapper_basename
(* deps: *) (* deps: *)
print_list config.dc_deps pp_list config.dc_deps
Fmt.(list (package_as_deps (quote plugin_as_package))) cmd.deps.load_plugin pp_command_deps cmd
(* targets: *) (* targets: *)
print_list wtest.log pp_list wtest.log
print_list wtest.bin pp_list wtest.bin
(* action: *) (* action: *)
wtest.cmd wtest.cmd
end; end;
...@@ -1549,16 +1594,15 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules = ...@@ -1549,16 +1594,15 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules =
Format.fprintf result_fmt Format.fprintf result_fmt
"(rule ; SHOW EXECNOW COMMAND #%d OF TEST FILE %S\n \ "(rule ; SHOW EXECNOW COMMAND #%d OF TEST FILE %S\n \
(alias %s)\n \ (alias %s)\n \
(deps %a (package frama-c)%a (universe))\n \ (deps %a (universe))\n \
(action (system %S))\n\ (action (system %S))\n\
)@." )@."
(* rules: *) (* rule: *)
nth file nth file
(* alias *) (* alias: *)
(mk_alias cmd "execnow.show") (mk_alias cmd "execnow.show")
(* deps: *) (* deps: *)
print_list config.dc_deps pp_command_deps cmd (* to get an updated build even in case of using the result *)
Fmt.(list (package_as_deps (quote plugin_as_package))) cmd.deps.load_plugin
(* action: *) (* action: *)
("echo '" ^ show_cmd wtest.cmd ^"'"); ("echo '" ^ show_cmd wtest.cmd ^"'");
; ;
...@@ -1568,9 +1612,9 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules = ...@@ -1568,9 +1612,9 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules =
(alias %s)\n \ (alias %s)\n \
(action (diff %S %S))\n\ (action (diff %S %S))\n\
)@." )@."
(* rules: *) (* rule: *)
n nth file n nth file
(* alias *) (* alias: *)
(ptests_alias ~env) (ptests_alias ~env)
(* action: *) (* action: *)
(SubDir.make_file (SubDir.oracle_subdir ~env SubDir.upper_dir) log) (SubDir.make_file (SubDir.oracle_subdir ~env SubDir.upper_dir) log)
...@@ -1578,19 +1622,19 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules = ...@@ -1578,19 +1622,19 @@ let dispatcher ~env ~result_fmt ~oracle_fmt file directory config modules =
) wtest.log ) wtest.log
in in
if config.dc_commands <> [] || config.dc_execnow <> [] then begin if config.dc_commands <> [] || config.dc_execnow <> [] then begin
let print_list_alias fmt l = List.iter (Format.fprintf fmt "(alias %S)") l in let pp_list_alias fmt l = List.iter (Format.fprintf fmt "(alias %S)") l in
Format.fprintf result_fmt Format.fprintf result_fmt
"; TEST FILE %S\n\ "; TEST FILE %S\n\
(alias (deps %a%a) (name %S)) ; to performs all sub-tests related to a file\n\ (alias (deps %a%a) (name %S)) ; to performs all sub-tests related to a file\n\
(alias (deps %a%a) (name %S)) ; to reproduce and visualize the all sub-test outputs related to a file@." (alias (deps %a%a) (name %S)) ; to reproduce and visualize the all sub-test outputs related to a file@."
file file
(* alias #1 *) (* alias #1 *)
print_list_alias (List.mapi (fun i _ -> Format.sprintf "%s.%d.exec.wtests" test_name i) config.dc_commands) pp_list_alias (List.mapi (fun i _ -> Format.sprintf "%s.%d.exec.wtests" test_name i) config.dc_commands)
print_list_alias (List.mapi (fun i _ -> Format.sprintf "%s.%d.execnow.wtests" test_name i) config.dc_execnow) pp_list_alias (List.mapi (fun i _ -> Format.sprintf "%s.%d.execnow.wtests" test_name i) config.dc_execnow)
(Format.sprintf "%s.wtests" test_name) (Format.sprintf "%s.wtests" test_name)
(* alias #2 *) (* alias #2 *)
print_list_alias (List.mapi (fun i _ -> Format.sprintf "%s.%d.exec" test_name i) config.dc_commands) pp_list_alias (List.mapi (fun i _ -> Format.sprintf "%s.%d.exec" test_name i) config.dc_commands)
print_list_alias (List.mapi (fun i _ -> Format.sprintf "%s.%d.execnow.wtests" test_name i) config.dc_execnow) pp_list_alias (List.mapi (fun i _ -> Format.sprintf "%s.%d.execnow.wtests" test_name i) config.dc_execnow)
file; file;
end ; end ;
List.iter make_cmd config.dc_commands; List.iter make_cmd config.dc_commands;
...@@ -1650,11 +1694,12 @@ let process ~env default_config (suites:Ptests_config.alias StringMap.t) = ...@@ -1650,11 +1694,12 @@ let process ~env default_config (suites:Ptests_config.alias StringMap.t) =
if test_pattern dir_config file if test_pattern dir_config file
then begin then begin
if !verbosity >= 2 then Format.printf "%% - Process test file %s ...@." file; if !verbosity >= 2 then Format.printf "%% - Process test file %s ...@." file;
has_test := dispatcher ~env ~result_fmt ~oracle_fmt file directory dir_config modules || !has_test; has_test := process_file ~env ~result_fmt ~oracle_fmt file directory dir_config modules || !has_test;
end; end;
) dir_files; ) dir_files;
let n = ref 0 in let n = ref 0 in
StringMap.iter (fun cmxs (libs,files) -> StringMap.iter (fun cmxs (libs,files) ->
let cmxs = Filename.basename cmxs in
let files = StringSet.elements (StringSet.of_list files) in let files = StringSet.elements (StringSet.of_list files) in
incr n; incr n;
Format.fprintf result_fmt Format.fprintf result_fmt
...@@ -1663,16 +1708,16 @@ let process ~env default_config (suites:Ptests_config.alias StringMap.t) = ...@@ -1663,16 +1708,16 @@ let process ~env default_config (suites:Ptests_config.alias StringMap.t) =
(modules %S)\n \ (modules %S)\n \
(modes plugin)\n \ (modes plugin)\n \
(libraries frama-c.init.cmdline frama-c.boot frama-c.kernel %a)\n \ (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel %a)\n \
(flags -open Frama_c_kernel)\n\ (flags :standard -w -50-9-32-6-34 -open Frama_c_kernel)\n\
)@." )@."
(* executable: *) (* executable: *)
!n print_list files !n pp_list files
(* name: *) (* name: *)
cmxs cmxs
(* module: *) (* module: *)
cmxs cmxs
(* libraries: *) (* libraries: *)
print_list (StringSet.elements libs)) pp_list (StringSet.elements libs))
!modules ; !modules ;
Format.fprintf result_fmt "@."; Format.fprintf result_fmt "@.";
Format.fprintf oracle_fmt "@."; Format.fprintf oracle_fmt "@.";
...@@ -1704,8 +1749,12 @@ let () = ...@@ -1704,8 +1749,12 @@ let () =
| [] -> [ "tests" ] | [] -> [ "tests" ]
| l -> l | l -> l
in in
let pwd = Unix.getcwd () in
List.iter (fun dir -> List.iter (fun dir ->
Format.printf "Test directory: %s@." dir; Format.printf "Test directory: %s@." dir;
let absolute_tests_dir = Filename.dirname
(if Filename.is_relative dir then Filename.concat pwd dir else dir)
in
let suites = Ptests_config.parse ~dir in let suites = Ptests_config.parse ~dir in
if !verbosity >= 1 then Format.printf "%% Nb config= %d@." (StringMap.cardinal suites); if !verbosity >= 1 then Format.printf "%% Nb config= %d@." (StringMap.cardinal suites);
let nb = !nb_dune_files in let nb = !nb_dune_files in
...@@ -1713,7 +1762,7 @@ let () = ...@@ -1713,7 +1762,7 @@ let () =
StringMap.iter (fun config_mode suites -> StringMap.iter (fun config_mode suites ->
if !verbosity >= 1 then Format.printf "%% - %s_SUITES -> nb suites= %d@." if !verbosity >= 1 then Format.printf "%% - %s_SUITES -> nb suites= %d@."
(match config_mode with "" -> "DEFAULT" | s -> s) (StringMap.cardinal suites); (match config_mode with "" -> "DEFAULT" | s -> s) (StringMap.cardinal suites);
let env = { config = config_mode ; dir ; dune_alias = "" } in let env = { config = config_mode ; dir ; dune_alias = "" ; absolute_tests_dir} in
let directory = SubDir.create ~with_subdir:false ~env dir in let directory = SubDir.create ~with_subdir:false ~env dir in
let config = Test_config.current_config ~env directory in let config = Test_config.current_config ~env directory in
let config = update_dir_ref directory config in let config = update_dir_ref directory config in
......
src/dune
+ 1
− 1
View file @ fadd858a
...@@ -20,7 +20,7 @@ ...@@ -20,7 +20,7 @@
(public_name frama-c.kernel) (public_name frama-c.kernel)
(optional) (optional)
(foreign_stubs (language c) (names c_bindings)) (foreign_stubs (language c) (names c_bindings))
(flags -w -50) (flags :standard -w -50-9-32-6-34)
(libraries frama-c.init str unix zarith ocamlgraph dynlink bytes yojson dune-site dune-site.plugins) (libraries frama-c.init str unix zarith ocamlgraph dynlink bytes yojson dune-site dune-site.plugins)
) )
......
src/init/boot/dune
+ 2
− 2
View file @ fadd858a
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
(name frama_c_boot) (name frama_c_boot)
(public_name frama-c.boot) (public_name frama-c.boot)
(modules boot) (modules boot)
(flags -open Frama_c_kernel) (flags :standard -open Frama_c_kernel)
(libraries frama_c_kernel) (libraries frama_c_kernel)
) )
...@@ -23,7 +23,7 @@ ...@@ -23,7 +23,7 @@
(public_name frama-c) (public_name frama-c)
(modules empty_file) (modules empty_file)
(package frama-c) (package frama-c)
(flags -open Frama_c_kernel -linkall) (flags :standard -open Frama_c_kernel -linkall)
(libraries frama-c.kernel frama-c.init.cmdline frama-c.boot) (libraries frama-c.kernel frama-c.init.cmdline frama-c.boot)
) )
......
src/plugins/sparecode/dune
+ 2
− 2
View file @ fadd858a
...@@ -2,8 +2,8 @@ ...@@ -2,8 +2,8 @@
(name Sparecode) (name Sparecode)
(public_name frama-c-sparecode.core) (public_name frama-c-sparecode.core)
(private_modules sparecode_params globs spare_marks transform register) (private_modules sparecode_params globs spare_marks transform register)
(flags -open Frama_c_kernel) (flags :standard -w -50-9-32-6-34 -open Frama_c_kernel)
(libraries frama-c.kernel frama-c-users.core frama-c-eva.core frama-c-pdg.core) (libraries frama-c.kernel frama-c-users.core frama-c-eva.core frama-c-pdg.core frama-c-inout.core)
) )
(plugin (optional) (name sparecode) (libraries frama-c-sparecode.core) (site (frama-c plugins))) (plugin (optional) (name sparecode) (libraries frama-c-sparecode.core) (site (frama-c plugins)))
src/plugins/wp/tests/ptests_config
+ 1
− 1
View file @ fadd858a
...@@ -2,7 +2,7 @@ DEFAULT_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare ...@@ -2,7 +2,7 @@ DEFAULT_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip
# todo: to fixes # todo: to fixes
DEFAULT_SUITES= wp_region IGNORE= DEFAULT_SUITES= wp_region
IGNORE= qualif_SUITES= wp wp_plugin wp_acsl wp_bts wp_store wp_hoare IGNORE= qualif_SUITES= wp wp_plugin wp_acsl wp_bts wp_store wp_hoare
IGNORE= qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip wp_region IGNORE= qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip wp_region
......
tests/ptests_config
+ 2
− 2
View file @ fadd858a
...@@ -4,11 +4,11 @@ ...@@ -4,11 +4,11 @@
# todo: adds verisec? # todo: adds verisec?
DEFAULT_SUITES= builtins callgraph cil constant_propagation compliance dynamic float idct impact DEFAULT_SUITES= builtins callgraph cil constant_propagation compliance dynamic float idct impact
DEFAULT_SUITES= jcdb journal libc metrics misc occurrence pdg pretty_printing rte rte_manual DEFAULT_SUITES= journal libc metrics occurrence pdg pretty_printing rte rte_manual
DEFAULT_SUITES= saveload scope slicing sparecode spec syntax test value value/traces DEFAULT_SUITES= saveload scope slicing sparecode spec syntax test value value/traces
# todo: fixes fc_script # todo: fixes fc_script
IGNORE= DEFAULT_SUITES= fc_script IGNORE= DEFAULT_SUITES= fc_script jcdb misc
# todo: adds make_run_script? # todo: adds make_run_script?
IGNORE= DEFAULT_SUITES= make_run_script IGNORE= DEFAULT_SUITES= make_run_script
......
tests/value/recursion.i deleted 100644 → 0
+ 0
− 77
View file @ 4f063dbd
/* run.config*
EXIT: 1
OPT: -lib-entry -main main -eva @EVA_CONFIG@
OPT: -lib-entry -main main -eva @EVA_CONFIG@ -eva-ignore-recursive-calls
*/
int G;
int ff() {
if (G) ff();
return 5;
}
int x;
volatile int c;
struct s {
int f1;
int f2;
} s;
// Use given assigns
/*@ assigns x \from x, y;
assigns s.f1 \from s.f2;
assigns \result \from s;
*/
struct s f(int y) {
x = 2+y;
Frama_C_show_each(x, y);
if (c) {
s = f(y);
Frama_C_show_each(x, y);
}
s.f1 = s.f2;
return s;
}
// Infers assigns \nothing
void g() {
g();
}
// Infer assigns clause that overwrite *p1 and *p2. Currently unsound
void h(int *p1, int *p2) {
h(p1, p2);
}
int *pg;
/* &i escapes. The precondition is true on all calls, but could be computed
false if one overwrites the value of i naively at each call. Currently unsound */
/*@ requires stage > 0 ==> *pg == i-5;
assigns *pg \from \nothing;
ensures stage > 0 ==> *pg == 8;
*/
void escaping_formal(int stage, int i) {
pg = &i;
Frama_C_show_each (pg, *pg, stage, i);
escaping_formal (1, i+5);
if (stage > 0)
*pg = 8;
Frama_C_show_each (pg, *pg, stage, i);
pg = 0;
}
int main() {
G = ff();
g();
int v1, v2;
h(&v1, &v2);
Frama_C_show_each(v1, v2);
escaping_formal(0, 10);
struct s r = f(0);
Frama_C_show_each(x);
return r.f1+1;
}
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