[kernel] Moves new parameter "-memory-footprint" in the kernel.

Configures the OCaml garbage collector in the first parsing stage of the
command line.

src/kernel_services/cmdline_parameters/cmdline.ml

@@ -380,6 +380,18 @@ let parse known_options_list then_expected options_list =
 
 let non_initial_options_ref = ref []
 
+(* Configure the OCaml Garbage Collector. *)
+let configure_ocaml_gc n =
+  if n < 1 || n > 10 then
+    Kernel_log.warning "Ignoring option -memory-footprint %i, \
+                        its argument should be between 1 and 10." n
+  else
+    let gc_control = Gc.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 }
+
 let () =
   let first_parsing_stage () =
     parse
@@ -394,6 +406,7 @@ let () =
         "-kernel-debug", Int (fun n -> Kernel_debug_level.set n);
         "-deterministic", Unit (fun () -> deterministic := true);
         "-permissive", Unit (fun () -> permissive := true);
+        "-memory-footprint", Int configure_ocaml_gc
       ]
       false
       all_options

src/kernel_services/plugin_entry_points/kernel.ml

@@ -1824,6 +1824,29 @@ module TypeCheck =
     let help = "forces typechecking of the source files"
   end)
 
+(* ************************************************************************* *)
+(** {2 Performance options} *)
+(* ************************************************************************* *)
+
+let performance = add_group "Performance"
+
+let () = Parameter_customize.set_group performance
+let () = Parameter_customize.do_not_projectify ()
+let () = Parameter_customize.set_cmdline_stage Cmdline.Early
+module MemoryFootprint =
+  Int
+    (struct
+      let module_name = "MemoryFootprint"
+      let default = 6
+      let option_name = "-memory-footprint"
+      let arg_name = "n"
+      let help =
+        "Control the memory usage of Frama-C. \
+         With smaller values, analyses consume much less memory but are \
+         also slightly slower. Must be between 1 and 10; default is 6."
+    end)
+let () = MemoryFootprint.set_range ~min:1 ~max:10
+
 (* ************************************************************************* *)
 (** {2 Other options} *)
 (* ************************************************************************* *)

src/plugins/eva/engine/analysis.ml

@@ -177,20 +177,8 @@ let () =
     ~user_only:true (fun _ -> reset_analyzer ());
   Project.register_after_global_load_hook reset_analyzer
 
-(* 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 ();
   Parameters.configure_precision ();
   if not (Kernel.AuditCheck.is_empty ()) then

src/plugins/eva/parameters.ml

@@ -398,20 +398,6 @@ 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,8 +58,6 @@ 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