diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 0677d81616ea2cf154b21d2f196cff39b916a58e..82e05def8e6ce595ed5383d0d079061118c936aa 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 b31c526f8648c46fb06a6677000e518e45f4f94b..8375ac554c748bc7f4a861ea546502704e168937 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