[Eva] New parameter -eva-memory-footprint to configure the ocaml gc.

src/plugins/eva/engine/analysis.ml

@@ -177,16 +177,21 @@ let () =
     ~user_only:true (fun _ -> reset_analyzer ());
   Project.register_after_global_load_hook reset_analyzer
 
-let tune_gc () =
-  if Sys.ocaml_release.major >= 5 then
-    let minor_heap_size = 8192000 in
-    let space_overhead = 40 in
-    Gc.(set { (get ()) with minor_heap_size; space_overhead; })
+(* Configure the OCaml Garbage Collector according to the
+   -eva-memory-footprint parameter (only if it has been set). *)
+let configure_ocaml_gc () =
+  if Parameters.MemoryFootprint.is_set () then
+    let gc_control = Gc.get () in
+    let n = Parameters.MemoryFootprint.get () in
+    let values = [| 24; 30; 40; 60; 90; 120; 150; 190; 240; 300 |] in
+    let space_overhead = values.(n-1) in
+    if space_overhead <> gc_control.space_overhead then
+      Gc.set { gc_control with space_overhead }
 
 (* Builds the analyzer if needed, and run the analysis. *)
 let force_compute () =
+  configure_ocaml_gc ();
   Ast.compute ();
-  tune_gc ();
   Parameters.configure_precision ();
   if not (Kernel.AuditCheck.is_empty ()) then
     Eva_audit.check_configuration (Kernel.AuditCheck.get ());

src/plugins/eva/parameters.ml

@@ -398,6 +398,20 @@ module JoinResults =
       let default = true
     end)
 
+let () = Parameter_customize.set_group performance
+module MemoryFootprint =
+  Int
+    (struct
+      let default = 6
+      let option_name = "-eva-memory-footprint"
+      let arg_name = "n"
+      let help =
+        "Control the memory usage of the analysis. \
+         With smaller values, the analysis consumes much less memory but is \
+         also slightly slower. Must be between 1 and 10; default is 6."
+    end)
+let () = MemoryFootprint.set_range ~min:1 ~max:10
+
 (* ------------------------------------------------------------------------- *)
 (* --- Non-standard alarms                                               --- *)
 (* ------------------------------------------------------------------------- *)

src/plugins/eva/parameters.mli

@@ -58,6 +58,8 @@ module ResultsAll: Parameter_sig.Bool
 
 module JoinResults: Parameter_sig.Bool
 
+module MemoryFootprint: Parameter_sig.Int
+
 module WarnSignedConvertedDowncast: Parameter_sig.Bool
 module WarnPointerSubstraction: Parameter_sig.Bool
 module WarnCopyIndeterminate: Parameter_sig.Kernel_function_set