From bde8bd24f41a8daf9d47c634ec34661dd03f41cc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 3 Apr 2020 19:35:09 +0200
Subject: [PATCH] [Eva] New option -eva-alloc-builtin to configure allocation
 builtins.

---
 src/plugins/value/value_parameters.ml  | 19 +++++++++++++++++++
 src/plugins/value/value_parameters.mli |  1 +
 2 files changed, 20 insertions(+)

diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 0677d81616e..82e05def8e6 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -1415,6 +1415,25 @@ let () = add_precision_dep ReductionDepth.parameter
 (* --- Dynamic allocation                                                 --- *)
 (* -------------------------------------------------------------------------- *)
 
+let () = Parameter_customize.set_group malloc
+module AllocBuiltin =
+  String
+    (struct
+      let option_name = "-eva-alloc-builtin"
+      let help = "Select the behavior of allocation builtins. \
+                  By default, they use up to [-eva-mlevel] bases \
+                  for each callstack (<by_stack>). They can also \
+                  use one <imprecise> base for all allocations, \
+                  create a <fresh> strong base at each call, \
+                  or create a <fresh_weak> base at each call."
+      let default = "by_stack"
+      let arg_name = "imprecise|by_stack|fresh|fresh_weak"
+    end)
+let () = add_precision_dep AllocBuiltin.parameter
+let () =
+  AllocBuiltin.set_possible_values
+    ["imprecise"; "by_stack"; "fresh"; "fresh_weak"]
+
 let () = Parameter_customize.set_group malloc
 module AllocFunctions =
   Filled_string_set
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index b31c526f864..8375ac554c7 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -149,6 +149,7 @@ module StopAtNthAlarm: Parameter_sig.Int
 
 (** Dynamic allocation *)
 
+module AllocBuiltin: Parameter_sig.String
 module AllocFunctions: Parameter_sig.String_set
 module AllocReturnsNull: Parameter_sig.Bool
 module MallocLevel: Parameter_sig.Int
-- 
GitLab