diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli index dc8c0bae4f7a55464e4331bbacf81ef69aa63e0e..d71fa98facac49545316eaa36eac9ee5ca40cdc1 100644 --- a/src/plugins/value/Eva.mli +++ b/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 diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml index df4428ee75a433d53cc23d1ced1a4a1525d9a02f..122835c78c2f664423edae6235400c83c89f93d9 100644 --- a/src/plugins/value/value_parameters.ml +++ b/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 diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli index 573e922bde59f3540e00a19d85516740c142acdd..23816c0c964ecdba0fa6d034e11a0410bdbee094 100644 --- a/src/plugins/value/value_parameters.mli +++ b/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 ../../.."