[tests] add configuration to report

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