diff --git a/Makefile b/Makefile
index 531ba1bf1fad242d50b3b824c728c376210b5a35..8a1d9897659a5a16bf966df630a839a416c2f6d5 100644
--- a/Makefile
+++ b/Makefile
@@ -899,7 +899,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
domains/cvalue/builtins_watchpoint \
domains/cvalue/builtins_float domains/cvalue/builtins_split \
domains/inout_domain \
- legacy/eval_terms legacy/eval_annots \
+ legacy/eval_terms \
domains/cvalue/cvalue_transfer domains/cvalue/cvalue_init \
domains/cvalue/cvalue_specification \
domains/cvalue/cvalue_domain \
@@ -908,7 +908,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
partitioning/auto_loop_unroll \
partitioning/partition partitioning/partitioning_parameters \
partitioning/partitioning_index partitioning/trace_partitioning \
- engine/recursion engine/function_calls \
+ engine/recursion engine/function_calls legacy/eval_annots \
engine/subdivided_evaluation engine/evaluation engine/abstractions \
engine/transfer_logic engine/transfer_stmt engine/transfer_specification \
engine/mem_exec engine/iterator engine/initialization \
diff --git a/src/plugins/value/engine/function_calls.ml b/src/plugins/value/engine/function_calls.ml
index eff7dbc77a5f6901692fb0970623833be131f5d1..7c368ffcbae75ebe3692dc56160438b35fbe1548 100644
--- a/src/plugins/value/engine/function_calls.ml
+++ b/src/plugins/value/engine/function_calls.ml
@@ -123,6 +123,14 @@ let analysis_status kf =
with Not_found -> Unreachable
+(* Must be consistent with the choice made by [analysis_target] below. *)
+let use_spec_instead_of_definition ?(recursion_depth = -1) kf =
+ Ast_info.is_frama_c_builtin (Kernel_function.get_name kf) ||
+ Builtins.is_builtin_overridden kf ||
+ recursion_depth >= Parameters.RecursiveUnroll.get () ||
+ not (Kernel_function.is_definition kf) ||
+ Kernel_function.Set.mem kf (Parameters.UsePrototype.get ())
+
let analysis_target ~recursion_depth callsite kf =
match Builtins.find_builtin_override kf with
| Some (name, builtin, cache, spec) ->
diff --git a/src/plugins/value/engine/function_calls.mli b/src/plugins/value/engine/function_calls.mli
index 698b62406e5db83c76b697e55acfe2d9f5169b62..c7efe940d8855a9e75c262d02d27a52fcf2f103e 100644
--- a/src/plugins/value/engine/function_calls.mli
+++ b/src/plugins/value/engine/function_calls.mli
@@ -40,6 +40,11 @@ type analysis_target =
val define_analysis_target:
?recursion_depth:int -> kinstr -> kernel_function -> analysis_target
+(** Returns true if the Eva analysis use the specification of the given
+ function instead of its body to interpret its calls. *)
+val use_spec_instead_of_definition:
+ ?recursion_depth:int -> kernel_function -> bool
+
(** Returns true if the function has been analyzed. *)
val is_called: kernel_function -> bool
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index d56f52ae0bb0ea56cd3eacb2d6132902c6c4c731..634021c6eccb088daea3311546445e8d09afb663 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -54,7 +54,7 @@ let pp_p_kind fmt = function
let post_kind kf =
if Builtins.is_builtin_overridden kf
then PostBuiltin
- else if !Db.Value.use_spec_instead_of_definition kf then
+ else if Function_calls.use_spec_instead_of_definition kf then
if Kernel_function.is_definition kf
then PostUseSpec
else PostLeaf
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 8e3c04f6d31f20deb9bbaf4aa09966db3482974d..205ad005015a33b60aa4b9434cd0831b7ee4f963 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -85,7 +85,7 @@ let do_copy_at = function
on functions whose body is analyzed. *)
let is_determinate kf =
let name = Kernel_function.get_name kf in
- (warn_indeterminate kf || !Db.Value.use_spec_instead_of_definition kf)
+ (warn_indeterminate kf || Function_calls.use_spec_instead_of_definition kf)
&& not (Ast_info.is_frama_c_builtin name)
let subdivide_stmt = Eva_utils.get_subdivision
diff --git a/src/plugins/value/gui_files/gui_eval.ml b/src/plugins/value/gui_files/gui_eval.ml
index 05ca7822f598f6266d533fc24a0ec3495b52da7a..691ec61e3e21054da275d86deaf89cf264b1147a 100644
--- a/src/plugins/value/gui_files/gui_eval.ml
+++ b/src/plugins/value/gui_files/gui_eval.ml
@@ -343,7 +343,7 @@ module Make (X: Analysis.S) = struct
let pre = pre_kf kf callstack in
let post = X.Dom.get_cvalue_or_top post in
let result =
- if !Db.Value.use_spec_instead_of_definition kf then
+ if Function_calls.use_spec_instead_of_definition kf then
None
else
let ret_stmt = Kernel_function.find_return kf in
@@ -395,7 +395,8 @@ module Make (X: Analysis.S) = struct
normal termination, and only when the function is called.
After states are not available. *)
let callstacks_at_post kf =
- if not (!Db.Value.use_spec_instead_of_definition kf) && results_kf_computed kf
+ if not (Function_calls.use_spec_instead_of_definition kf)
+ && results_kf_computed kf
then
let ret = Kernel_function.find_return kf in
let states_before = X.get_stmt_state_by_callstack ~after:true ret in
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index 8c83557fd2a766d1dde996152ae20a256e009ece..4bf4155529115dd9930da1dc8a5f579a32f3e1c4 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -109,7 +109,7 @@ let mark_unreachable () =
Visitor.visitFramacFileFunctions unreach (Ast.get ())
let c_labels kf cs =
- if !Db.Value.use_spec_instead_of_definition kf then
+ if Function_calls.use_spec_instead_of_definition kf then
Cil_datatype.Logic_label.Map.empty
else
let fdec = Kernel_function.get_definition kf in
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index c1e1695ae85b438899b4c2d4199c034d24a20eae..8732d620e1aca7f1c02075cfd2cb79d35ea9e81b 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -124,14 +124,6 @@ let find_deps_term_no_transitivity_state state t =
r.Eval_terms.ldeps
with Eval_terms.LogicEvalError _ -> raise Db.From.Not_lval
-(* If the function is a builtin, or if the user has requested it, use
- \assigns and \from clauses, that give an approximation of the result *)
-let use_spec_instead_of_definition kf =
- not (Kernel_function.is_definition kf) ||
- Ast_info.is_frama_c_builtin (Kernel_function.get_name kf) ||
- Builtins.is_builtin_overridden kf ||
- Kernel_function.Set.mem kf (Parameters.UsePrototype.get ())
-
let eval_predicate ~pre ~here p =
let open Eval_terms in
let env = env_annot ~pre ~here () in
@@ -153,7 +145,8 @@ let valid_behaviors kf state =
let () =
(* Pretty-printing *)
- Db.Value.use_spec_instead_of_definition := use_spec_instead_of_definition;
+ Db.Value.use_spec_instead_of_definition :=
+ Function_calls.use_spec_instead_of_definition;
Db.Value.assigns_outputs_to_zone := assigns_outputs_to_zone;
Db.Value.assigns_outputs_to_locations := assigns_outputs_to_locations;
Db.Value.assigns_inputs_to_zone := assigns_inputs_to_zone;