diff --git a/lustrec_tests/test.ml b/lustrec_tests/test.ml index c7b9c6e5bc164db1f281fc79bae2fe842d19fdb4..abf188331d02e79ec5ce29cf4208c8d59de49123 100644 --- a/lustrec_tests/test.ml +++ b/lustrec_tests/test.ml @@ -61,10 +61,60 @@ type config = { results_directory: string; } +let frama_c = "frama-c" +let wp_provers = [ "alt-ergo"; "z3"; "cvc4" ] |> String.concat "," +let wp_models = [ "ref"; "real" ] |> String.concat "," +let wp_timeout = 60 |> string_of_int +let wp_par = 48 |> string_of_int +let wp_cache = "none" + +(* let wp_cache_dir = Filename.concat dir "cache" *) +let wp_args = + [ + "-wp"; + "-wp-prover"; + wp_provers; + "-wp-model"; + wp_models; + "-wp-no-warn-memory-model"; + "-wp-timeout"; + wp_timeout; + "-wp-par"; + wp_par; + (* "-wp-cache-dir"; wp_cache_dir *) + "-wp-cache"; + wp_cache; + ] + +let wp_strategy = + String.concat + "," + [ + "LustreC:Transitions"; (* "LustreC:ResetCleared"; *) "LustreC:MemoryPacks"; + ] + +let wp_auto_depth = 100 |> string_of_int +let wp_auto_width = 100 |> string_of_int + +let wp_strategy_args = + wp_args + @ [ + "-wp-auto"; + wp_strategy; + "-wp-auto-depth"; + wp_auto_depth; + "-wp-auto-width"; + wp_auto_width; + ] + +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" let compiled_section = section "COMPILED" let ninit_section = section "BAD_INIT" @@ -195,6 +245,13 @@ let parse_report cfg = r with _ -> empty_report +let pp_config fmt cfg = + 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) + end_section + let pp_compiled fmt report = fprintf fmt "%s@;%a%s@;" compiled_section S.pp report.compiled end_section @@ -211,10 +268,12 @@ let pp_verified fmt report = fmt (List.sort (fun (i, _) (j, _) -> compare i j) (M.bindings report.verified)) -let pp_report fmt report = +let pp_report fmt cfg report = fprintf fmt - "@[<v>%a@;%a@;%a@;%a@]@." + "@[<v>%a@;%a@;%a@;%a@;%a@]@." + pp_config + cfg pp_compiled report pp_ninits @@ -227,7 +286,7 @@ let pp_report fmt report = let write_report cfg report = let oc = open_out (report_file cfg) in let fmt = formatter_of_out_channel oc in - pp_report fmt report; + pp_report fmt cfg report; close_out oc let config_format_tags = @@ -333,55 +392,6 @@ let compile cfg report lustrec fs = print_results ok ko ninits n; report -let frama_c = "frama-c" -let wp_provers = [ "alt-ergo"; "z3"; "cvc4" ] |> String.concat "," -let wp_models = [ "ref"; "real" ] |> String.concat "," -let wp_timeout = 60 |> string_of_int -let wp_par = 48 |> string_of_int -let wp_cache = "none" - -(* let wp_cache_dir = Filename.concat dir "cache" *) -let wp_args = - [ - "-wp"; - "-wp-prover"; - wp_provers; - "-wp-model"; - wp_models; - "-wp-no-warn-memory-model"; - "-wp-timeout"; - wp_timeout; - "-wp-par"; - wp_par; - (* "-wp-cache-dir"; wp_cache_dir *) - "-wp-cache"; - wp_cache; - ] - -let wp_strategy = - String.concat - "," - [ - "LustreC:Transitions"; (* "LustreC:ResetCleared"; *) "LustreC:MemoryPacks"; - ] - -let wp_auto_depth = 100 |> string_of_int -let wp_auto_width = 100 |> string_of_int - -let wp_strategy_args = - wp_args - @ [ - "-wp-auto"; - wp_strategy; - "-wp-auto-depth"; - wp_auto_depth; - "-wp-auto-width"; - wp_auto_width; - ] - -let frama_c_args f = wp_args @ (f :: "-then" :: wp_strategy_args) -let frama_c_cmd f = frama_c :: frama_c_args f - let goals log = let open Re.Str in let reg = "\\([0-9]+\\) / \\([0-9]+\\)" in