diff --git a/lustrec_tests/dune b/lustrec_tests/dune index 5b79b1cab38b05c941c63b6a707565c7e8953281..9b655ddd259b5aed41386bf233f4f075f8cca60f 100644 --- a/lustrec_tests/dune +++ b/lustrec_tests/dune @@ -1,13 +1,16 @@ (env - (dev - (flags (:standard -w -32)))) + (dev + (flags + (:standard -w -32)))) (test (name test) (libraries re unix yojson) (deps - (:lus (glob_files *.lus)) + (:lus + (glob_files *.lus)) (:cfg config.json) - (glob_files *)) ; to include `ignored` if its present + (glob_files *)) + ; to include `ignored` if its present (action (run %{test} %{project_root} %{bin:lustrec} %{cfg} "%{lus}"))) diff --git a/lustrec_tests/test.ml b/lustrec_tests/test.ml index abf188331d02e79ec5ce29cf4208c8d59de49123..f4386925030a6097b36d098333f2f63ffc96f499 100644 --- a/lustrec_tests/test.ml +++ b/lustrec_tests/test.ml @@ -1,6 +1,5 @@ open Format open Unix - module Y = Yojson.Basic module S = struct @@ -55,10 +54,10 @@ let empty_report = } type config = { - initial_timeout: int; - optimization_level: int; - ignored_file: string option; - results_directory: string; + initial_timeout : int; + optimization_level : int; + ignored_file : string option; + results_directory : string; } let frama_c = "frama-c" @@ -109,9 +108,7 @@ let wp_strategy_args = let frama_c_args f = wp_args @ (f :: "-then" :: wp_strategy_args) let frama_c_cmd f = frama_c :: frama_c_args f - let report_file cfg = Filename.concat cfg.results_directory "report" - let section h = "# " ^ h let end_section = "##" let config_section = section "CONFIG" @@ -246,7 +243,9 @@ let parse_report cfg = with _ -> empty_report let pp_config fmt cfg = - fprintf fmt "%s@;Optimization level: %s@;Frama-C options: %s@;%s@;" + fprintf + fmt + "%s@;Optimization level: %s@;Frama-C options: %s@;%s@;" config_section ("O" ^ (cfg.optimization_level |> string_of_int)) (String.concat " " wp_strategy_args) @@ -336,9 +335,11 @@ let print_results ok ko w n = let lustrec_params cfg f = [ "-acsl-spec"; - "-d"; cfg.results_directory; - "-O"; cfg.optimization_level |> string_of_int; - f + "-d"; + cfg.results_directory; + "-O"; + cfg.optimization_level |> string_of_int; + f; ] let compile cfg report lustrec fs = @@ -371,7 +372,10 @@ let compile cfg report lustrec fs = else if is_ninit report f then ninit report else let cmd = - Filename.quote_command ~stderr:err_f lustrec (lustrec_params cfg f) + Filename.quote_command + ~stderr:err_f + lustrec + (lustrec_params cfg f) in let ic = open_process_in cmd in let b = @@ -528,11 +532,12 @@ let read_config root = let tests_directory = Sys.getcwd () |> Filename.basename in let optimization_level = get_default "optimization_level" to_int 2 in let result_dir = root ^ "/../../results/" in - (try Unix.mkdir result_dir 0o755 with _ -> ()); + (try Unix.mkdir result_dir 0o755 with _ -> ()); let results_directory = - result_dir ^ tests_directory ^ "_" ^ - (if optimization_level < 0 then "wo_optimization" - else "O" ^ string_of_int optimization_level) + result_dir ^ tests_directory ^ "_" + ^ + if optimization_level < 0 then "wo_optimization" + else "O" ^ string_of_int optimization_level in (try Unix.mkdir results_directory 0o755 with _ -> ()); { @@ -548,15 +553,16 @@ let () = let cfg = read_config root in let lus_fs = Sys.argv.(4) |> Re.Str.(split (regexp_string " ")) in let ignored_fs = - Option.fold ~none:[] + Option.fold + ~none:[] ~some:(fun ignored_f -> - let ic = open_in ignored_f in - let rec read fs = - try read (input_line ic :: fs) with End_of_file -> fs - in - let fs = read [] in - close_in ic; - fs) + let ic = open_in ignored_f in + let rec read fs = + try read (input_line ic :: fs) with End_of_file -> fs + in + let fs = read [] in + close_in ic; + fs) cfg.ignored_file in let report = parse_report cfg in