diff --git a/ptests/ptests.ml b/ptests/ptests.ml index aa26cc7bb1826aea55faf74708fb319a594bd6bf..8dbd21f63831c749cd22c0b0071db4151b6a95bf 100644 --- a/ptests/ptests.ml +++ b/ptests/ptests.ml @@ -1242,9 +1242,20 @@ module Fmt = struct let var_libavailable pr fmt s = Format.fprintf fmt "%%{lib-available:%a.core}" pr s let package_as_deps pr fmt s = Format.fprintf fmt "(package %a)" pr s end + +let home_regexp = Str.regexp "^\\(~\\|[$]HOME\\|[$]\\{HOME\\}\\)\\(/.*\\)" +let get_home_env () = + try + Unix.getenv "HOME" + with Not_found -> "~" + let pp_list_deps fmt l = List.iter (fun s -> let s = Filename.sanitize_with_space s in + let s = match str_string_match2 home_regexp s 0 with + | None -> s + | Some (_,subdir) -> (get_home_env ()) ^ subdir + in if String.contains s '*' then Format.fprintf fmt " (glob_files %S)" s else @@ -1914,7 +1925,8 @@ let () = List.iter (fun dir -> Format.printf "Test directory: %s@." dir; let absolute_tests_dir = Filename.dirname - (if Filename.is_relative dir then Filename.concat absolute_cwd dir else dir) + (if Filename.is_relative dir + then Filename.concat absolute_cwd dir else dir) in let suites = Ptests_config.parse ~dir in if !verbosity >= 1 then Format.printf "%% Nb config= %d@." (StringMap.cardinal suites); diff --git a/src/plugins/wp/tests/why3/test_config_qualif b/src/plugins/wp/tests/why3/test_config_qualif index 40a46bc821a47c59715d800508aabd855a13f2e1..0e60b550835d90fccfd265b17ba60d46e227699c 100644 --- a/src/plugins/wp/tests/why3/test_config_qualif +++ b/src/plugins/wp/tests/why3/test_config_qualif @@ -1,4 +1,5 @@ FILEREG: .*\.why +DEPS: ~/.why3.conf CMD: why3 -L @PTEST_SHARE_DIR@/why3 prove -P alt-ergo OPT: COMMENT: the filter remove the information about time and steps