From 047b1f38f7a650eafeb694acf74e55c34246c089 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:32:31 +0100
Subject: [PATCH] [Kernel] Moves new option -cache-size in the kernel.
---
share/analysis-scripts/analysis.mk | 2 +-
.../plugin_entry_points/kernel.ml | 20 +++++++++++++++++++
src/libraries/utils/binary_cache.ml | 6 +++---
src/plugins/eva/parameters.ml | 18 -----------------
tests/fc_script/make-wrapper.t/run.t | 2 +-
5 files changed, 25 insertions(+), 23 deletions(-)
diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk
index 9165754c380..311e93d2fb2 100644
--- a/share/analysis-scripts/analysis.mk
+++ b/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 ?=
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index cabf7da511d..5ffc6d21ff0 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/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} *)
(* ************************************************************************* *)
diff --git a/src/libraries/utils/binary_cache.ml b/src/libraries/utils/binary_cache.ml
index 9b1e58c5d00..24eaa41957a 100644
--- a/src/libraries/utils/binary_cache.ml
+++ b/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:
diff --git a/src/plugins/eva/parameters.ml b/src/plugins/eva/parameters.ml
index c347010dd82..131d5afea37 100644
--- a/src/plugins/eva/parameters.ml
+++ b/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 --- *)
(* ------------------------------------------------------------------------- *)
diff --git a/tests/fc_script/make-wrapper.t/run.t b/tests/fc_script/make-wrapper.t/run.t
index 936b5c2b4d2..c1ea52b1202 100644
--- a/tests/fc_script/make-wrapper.t/run.t
+++ b/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:
--
GitLab