From 98d6dfeee0f574a5f8a647217007631c5089b234 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 15 Jul 2019 15:52:06 +0200
Subject: [PATCH] [Eva] New option -eva-subdivide-non-linear-function.
Overrides the global option -eva-subdivide-non-linear for the given functions.
---
src/plugins/value/engine/transfer_stmt.ml | 3 +--
src/plugins/value/utils/value_util.ml | 6 ++++++
src/plugins/value/utils/value_util.mli | 1 +
src/plugins/value/value_parameters.ml | 24 +++++++++++++++++++++++
src/plugins/value/value_parameters.mli | 4 ++++
5 files changed, 36 insertions(+), 2 deletions(-)
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 5c4f2650e53..62f33145250 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -90,8 +90,7 @@ let is_determinate kf =
|| (name >= "Frama_C" && name < "Frama_D")
|| Builtins.find_builtin_override kf <> None)
-let subdivide_stmt _stmt =
- Value_parameters.LinearLevel.get ()
+let subdivide_stmt = Value_util.get_subdivision
let subdivide_kinstr = function
| Kglobal -> Value_parameters.LinearLevel.get ()
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index 99bfd13838f..24df6f735e5 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -71,6 +71,12 @@ let get_slevel kf =
try Value_parameters.SlevelFunction.find kf
with Not_found -> Value_parameters.SemanticUnrollingLevel.get ()
+let get_subdivision stmt =
+ try
+ let kf = Kernel_function.find_englobing_kf stmt in
+ Value_parameters.LinearLevelFunction.find kf
+ with Not_found -> Value_parameters.LinearLevel.get ()
+
let pretty_actuals fmt actuals =
let pp fmt (e,x,_) = Cvalue.V.pretty_typ (Some (Cil.typeOf e)) fmt x in
Pretty_utils.pp_flowlist pp fmt actuals
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/value_util.mli
index a631d797987..1613ca7b695 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/value_util.mli
@@ -46,6 +46,7 @@ val pp_callstack : Format.formatter -> unit
(* TODO: Document the rest of this file. *)
val emitter : Emitter.t
val get_slevel : Kernel_function.t -> Value_parameters.SlevelFunction.value
+val get_subdivision: stmt -> int
val pretty_actuals :
Format.formatter -> (Cil_types.exp * Cvalue.V.t * 'b) list -> unit
val pretty_current_cfunction_name : Format.formatter -> unit
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index a45ba4188c1..1c1f48833fd 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -1020,6 +1020,30 @@ module LinearLevel =
let () = add_precision_dep LinearLevel.parameter
let () = LinearLevel.add_aliases ["-val-subdivide-non-linear"]
+let () = Parameter_customize.set_group precision_tuning
+module LinearLevelFunction =
+ Kernel_function_map
+ (struct
+ include Datatype.Int
+ type key = Cil_types.kernel_function
+ let of_string ~key:_ ~prev:_ s =
+ Extlib.opt_map
+ (fun s ->
+ try int_of_string s
+ with Failure _ ->
+ raise (Cannot_build ("'" ^ s ^ "' is not an integer")))
+ s
+ let to_string ~key:_ = Extlib.opt_map string_of_int
+ end)
+ (struct
+ let option_name = "-eva-subdivide-non-linear-function"
+ let arg_name = "f:n"
+ let help = "override the global option -eva-subdivide-non-linear with <n>\
+ when analyzing the function <f>."
+ let default = Kernel_function.Map.empty
+ end)
+let () = add_precision_dep LinearLevelFunction.parameter
+
let () = Parameter_customize.set_group precision_tuning
let () = Parameter_customize.argument_may_be_fundecl ()
module UsePrototype =
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 7ead8310a01..a6f0c7077ba 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -129,6 +129,10 @@ module SkipLibcSpecs: Parameter_sig.Bool
module RmAssert: Parameter_sig.Bool
module LinearLevel: Parameter_sig.Int
+module LinearLevelFunction:
+ Parameter_sig.Map with type key = Cil_types.kernel_function
+ and type value = int
+
module BuiltinsOverrides:
Parameter_sig.Map with type key = Cil_types.kernel_function
and type value = string
--
GitLab