From 2f276a0cf29c8b8541d44c26cd85c7db827123a3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 15 Jan 2025 14:57:00 +0100
Subject: [PATCH] [kernel] Moves new parameter "-memory-footprint" in the
kernel.
Configures the OCaml garbage collector in the first parsing stage of the
command line.
---
.../cmdline_parameters/cmdline.ml | 13 +++++++++++
.../plugin_entry_points/kernel.ml | 23 +++++++++++++++++++
src/plugins/eva/engine/analysis.ml | 12 ----------
src/plugins/eva/parameters.ml | 14 -----------
src/plugins/eva/parameters.mli | 2 --
5 files changed, 36 insertions(+), 28 deletions(-)
diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index 944dd8dba3c..2d518f7f43e 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/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
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index e0c936d92f5..cabf7da511d 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/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} *)
(* ************************************************************************* *)
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index 5bf496db627..c0ea1e2ca83 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/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
diff --git a/src/plugins/eva/parameters.ml b/src/plugins/eva/parameters.ml
index 06b181cb86f..620f41b7048 100644
--- a/src/plugins/eva/parameters.ml
+++ b/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 --- *)
(* ------------------------------------------------------------------------- *)
diff --git a/src/plugins/eva/parameters.mli b/src/plugins/eva/parameters.mli
index ca654e78209..90225279e44 100644
--- a/src/plugins/eva/parameters.mli
+++ b/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
--
GitLab