[Eva] Export a function to enable global value partitioning

src/plugins/value/Eva.mli

@@ -40,6 +40,10 @@ module Value_parameters: sig
       to interpret calls to function [kf].
       Raises [Not_found] if there is no builtin of name [name]. *)
   val use_builtin: Cil_types.kernel_function -> string -> unit
+
+  (** [use_global_value_partitioning vi] instructs the analysis to use
+      value partitioning on the global variable [vi]. *)
+  val use_global_value_partitioning: Cil_types.varinfo -> unit
 end
 
 module Eval_terms: sig

src/plugins/value/value_parameters.ml

@@ -800,6 +800,9 @@ module ValuePartitioning =
     end)
 let () = add_precision_dep ValuePartitioning.parameter
 
+let use_global_value_partitioning vi =
+  ValuePartitioning.add vi.Cil_types.vname
+
 let () = Parameter_customize.set_group precision_tuning
 module SplitLimit =
   Int

src/plugins/value/value_parameters.mli

@@ -228,6 +228,10 @@ val enabled_domains: unit -> (string * string) list
     builtin `b`. *)
 val use_builtin: Cil_types.kernel_function -> string -> unit
 
+(** [use_global_value_partitioning vi] enable value partitioning on the global
+    variable `vi`. *)
+val use_global_value_partitioning: Cil_types.varinfo -> unit
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."