diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml index 944dd8dba3c7995c00120fb9cb704544d4ea01bc..2d518f7f43e414f23fdcc7ad51a05f652a992de9 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 e0c936d92f5f6cf66ea4fd41f869141b3cf0c5a4..cabf7da511dff86c26e4bad9b233f28758968337 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 5bf496db627de90a91174ebfcc76583bd991f981..c0ea1e2ca83e0993160b21dde03da3b255732bfb 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 06b181cb86fc192f7b154ee08fde6b9b858fa6d1..620f41b7048a09259677e0dc978cbb3e3e18c919 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 ca654e78209f38466e07b35d8d1086443441fc2f..90225279e4400d667c0f54230dc4301fff40a4e9 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