From f440916e58224fb7c22a301b53dd884acd9bf793 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 18 Nov 2020 01:16:01 +0100
Subject: [PATCH] [Eva] Export a function to enable global value partitioning
---
src/plugins/value/Eva.mli | 4 ++++
src/plugins/value/value_parameters.ml | 3 +++
src/plugins/value/value_parameters.mli | 4 ++++
3 files changed, 11 insertions(+)
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index dc8c0bae4f7..d71fa98faca 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 df4428ee75a..122835c78c2 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 573e922bde5..23816c0c964 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 ../../.."
--
GitLab