[Eva] Adds the [callstack] in the [Eval.call] record built by transfer_stmt.

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

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)

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)

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;

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

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

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