[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

@@ -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 ()

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

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

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 =

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