diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 50b0d1084fdf9d1c41f08f15226012efa981c997..ece699c60df2f50dfa57448e281799a191c9e1f8 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -331,7 +331,9 @@ module Make (Abstract: Abstractions.Eva) = struct
try
Value_util.push_call_stack kf Kglobal;
store_initial_state kf init_state;
- let call = { kf; arguments = []; rest = []; return = None; } in
+ let call =
+ { kf; callstack = []; arguments = []; rest = []; return = None; }
+ in
let final_result =
compute_using_spec_or_body Kglobal call None init_state
in
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index 634204a945292417d970cbc234e657d0255144fe..a5abcb4b90ed4470cda6e8ad546d2b8e071ef496 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -167,8 +167,8 @@ let make_recursion call depth =
{ depth; substitution; base_substitution; withdrawal; base_withdrawal; }
let make call =
- let call_stack = Value_util.call_stack () in
- let previous_calls = List.filter (fun (f, _) -> f == call.kf) call_stack in
+ let is_same_kf (f, _) = Kernel_function.equal f call.kf in
+ let previous_calls = List.filter is_same_kf call.callstack in
let depth = List.length previous_calls in
if depth > 0
then Some (make_recursion call depth)
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 68c94c2fa24d42d1e9c85cd58b5006babcbcafca..7ba3de0d199c4f9439b87c9657f175d8ff83fc09 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -538,6 +538,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Create an Eval.call *)
let create_call kf args =
let return = Library_functions.get_retres_vi kf in
+ let callstack = Value_util.call_stack () in
let arguments, rest =
let formals = Kernel_function.get_formals kf in
let rec format_arguments acc args formals = match args, formals with
@@ -551,7 +552,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let arguments = List.rev arguments in
arguments, rest
in
- {kf; arguments; rest; return; }
+ {kf; callstack; arguments; rest; return; }
let replace_value visitor substitution = function
| Assign value -> Assign (Value.replace_base substitution value)
diff --git a/src/plugins/value/eval.ml b/src/plugins/value/eval.ml
index 74eb76353824f011548ccc8fe7727b42262cda2e..7a12a168d662e1d7225531415b317ba18e5bfbaf 100644
--- a/src/plugins/value/eval.ml
+++ b/src/plugins/value/eval.ml
@@ -240,8 +240,13 @@ type ('loc, 'value) argument = {
avalue: ('loc, 'value) assigned;
}
+
+type call_site = kernel_function * kinstr
+type callstack = call_site list
+
type ('loc, 'value) call = {
kf: kernel_function;
+ callstack: callstack;
arguments: ('loc, 'value) argument list;
rest: (exp * ('loc, 'value) assigned) list;
return: varinfo option;
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index c68cebbd998e47af73b5109c6cb0384dac977530..5714172358fc24dfbc4ba07a05c4fe2722fcb2b0 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -222,9 +222,22 @@ type ('loc, 'value) argument = {
avalue: ('loc, 'value) assigned; (** The value of the concrete argument. *)
}
+(** A call_stack is a list, telling which function was called at which
+ site. The head of the list tells about the latest call. *)
+
+(** A call site: the function called, and the call statement
+ (or [Kglobal] for the main function. *)
+type call_site = kernel_function * kinstr
+
+(* A call stack is a list of call sites. The head is the latest call.
+ The last element is the main function. *)
+type callstack = call_site list
+
(** A function call. *)
type ('loc, 'value) call = {
kf: kernel_function; (** The called function. *)
+ callstack: callstack; (** The current callstack
+ (without this call). *)
arguments: ('loc, 'value) argument list; (** The arguments of the call. *)
rest: (exp * ('loc, 'value) assigned) list; (** Extra-arguments. *)
return: varinfo option; (** Fake varinfo to store the
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index 00f2871518eca24188ce2f575e0bfdc71771c7c6..13a005dd2afb149c347bfdd8ed45f51fd90b3262 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -24,11 +24,7 @@ open Cil_types
(* Callstacks related types and functions *)
-(* Function called, and calling instruction. *)
-type call_site = (kernel_function * kinstr)
-type callstack = call_site list
-
-let call_stack : callstack ref = ref []
+let call_stack : Value_types.callstack ref = ref []
(* let call_stack_for_callbacks : (kernel_function * kinstr) list ref = ref [] *)
let clear_call_stack () =
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/value_util.mli
index 61df6ce5331ea7d09ef8efb35e2e607bb5f3d0e5..0bfe89cbe916816878319417b0dc123ad79bea1c 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/value_util.mli
@@ -24,11 +24,6 @@ open Cil_types
(** {2 Callstacks related types and functions} *)
-(** A call_stack is a list, telling which function was called at which
- site. The head of the list tells about the latest call. *)
-type call_site = (kernel_function * kinstr)
-type callstack = call_site list
-
(** Functions dealing with call stacks. *)
val clear_call_stack : unit -> unit
val pop_call_stack : unit -> unit
@@ -36,7 +31,7 @@ val push_call_stack : kernel_function -> kinstr -> unit
(** The current function is the one on top of the call stack. *)
val current_kf : unit -> kernel_function
-val call_stack : unit -> callstack
+val call_stack : unit -> Value_types.callstack
(** Prints the current callstack. *)
val pp_callstack : Format.formatter -> unit