[Kernel] Moves new option -cache-size in the kernel.

share/analysis-scripts/analysis.mk

@@ -125,7 +125,7 @@ EVAFLAGS   ?= \
   -no-deps-print -no-calldeps-print \
   -eva-warn-key garbled-mix=active,garbled-mix:write=active \
   -calldeps -from-verbose 0 \
-	-eva-cache-size 8 \
+	-cache-size 8 \
   $(if $(EVABUILTINS), -eva-builtin=$(call fc_list,$(EVABUILTINS)),) \
   $(if $(EVAUSESPECS), -eva-use-spec $(call fc_list,$(EVAUSESPECS)),)
 WPFLAGS    ?=

src/kernel_services/plugin_entry_points/kernel.ml

@@ -1847,6 +1847,26 @@ module MemoryFootprint =
     end)
 let () = MemoryFootprint.set_range ~min:1 ~max:10
 
+let () = Parameter_customize.set_group performance
+let () = Parameter_customize.do_not_reset_on_copy ()
+module CacheSize =
+  Int
+    (struct
+      let module_name = "CacheSize"
+      let default = 2
+      let option_name = "-cache-size"
+      let arg_name = "n"
+      let help =
+        "Control the amount of memory allocated to some internal caches. \
+         Must be between 1 and 10; default value is 2. \
+         Each increase of 1 doubles the size of these caches. \
+         Small values are most suitable for the analysis of small programs \
+         (less than 1000 lines). Higher values (around 7-8) can speed up the \
+         analysis of large code bases."
+    end)
+let () = CacheSize.set_range ~min:1 ~max:10
+let () = CacheSize.add_update_hook (fun _ i -> Binary_cache.set_cache_size i)
+
 (* ************************************************************************* *)
 (** {2 Other options} *)
 (* ************************************************************************* *)

src/libraries/utils/binary_cache.ml

@@ -23,11 +23,11 @@
 let compute_cache_size i = 1 lsl (8 + i)
 let default_value = 2
 
-(* Should not be used to create cache before the value from -eva-cache-size
-   has been set by Eva. *)
+(* Should not be used to create cache before the value from -cache-size
+   has been set. *)
 let cache_size = ref (compute_cache_size default_value)
 
-(* Set by Eva, according to the -eva-cache-size parameter. *)
+(* Set by the kernel, according to the -cache-size parameter. *)
 let set_cache_size i = cache_size := compute_cache_size i
 
 (** The caches of this module are lazy, for two reasons:

src/plugins/eva/parameters.ml

@@ -398,24 +398,6 @@ module JoinResults =
       let default = true
     end)
 
-let () = Parameter_customize.set_group performance
-module CacheSize =
-  Int
-    (struct
-      let default = 2
-      let option_name = "-eva-cache-size"
-      let arg_name = "n"
-      let help =
-        "Control the amount of memory allocated to the internal caches \
-         of Eva. Must be between 1 and 10; default value is 2. \
-         Each increase of 1 doubles the size of these caches. \
-         Small values are most suitable for the analysis of small programs \
-         (less than 1000 lines). Higher values (around 7-8) can speed up the \
-         analysis of large code bases."
-    end)
-let () = CacheSize.set_range ~min:1 ~max:10
-let () = CacheSize.add_update_hook (fun _ i -> Binary_cache.set_cache_size i)
-
 (* ------------------------------------------------------------------------- *)
 (* --- Non-standard alarms                                               --- *)
 (* ------------------------------------------------------------------------- *)

tests/fc_script/make-wrapper.t/run.t

@@ -11,7 +11,7 @@ verbose output for Make.
   [kernel] Parsing make-wrapper.c (with preprocessing)
   [kernel] Parsing make-wrapper2.c (with preprocessing)
   
-  Command: frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -eva -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state -eva-print-callstacks -eva-warn-key alarm=inactive -no-deps-print -no-calldeps-print -eva-warn-key garbled-mix=active,garbled-mix:write=active -calldeps -from-verbose 0 -eva-warn-key builtins:missing-spec=abort
+  Command: frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -eva -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state -eva-print-callstacks -eva-warn-key alarm=inactive -no-deps-print -no-calldeps-print -eva-warn-key garbled-mix=active,garbled-mix:write=active -calldeps -from-verbose 0 -cache-size 8 -eva-warn-key builtins:missing-spec=abort
   
   [eva] Analyzing a complete application starting at main
   [eva:recursion] make-wrapper.c:17: