diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml index ac17b268d15e9a6f9819f355b847fbbe84907786..c4288155ea6abb07ccb022ba7de51213ed68918e 100644 --- a/src/plugins/value/engine/compute_functions.ml +++ b/src/plugins/value/engine/compute_functions.ml @@ -352,9 +352,8 @@ module Make (Abstract: Abstractions.Eva) = struct let compute () = Eva_utils.push_call_stack kf Kglobal; store_initial_state kf init_state; - let call = - { kf; callstack = []; arguments = []; rest = []; return = None; } - in + let callstack = [kf, Kglobal] in + let call = { kf; callstack; arguments = []; rest = []; return = None; } in let final_result = compute_call Kglobal call None init_state in let final_states = List.map snd (final_result.Transfer.states) in let final_state = PowersetDomain.(final_states |> of_list |> join) in diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml index 9134b02da047024d6cc98b06eceb891721f6108c..fb0da4b9b937d09ce4fa8aac3de912354e5851ab 100644 --- a/src/plugins/value/engine/recursion.ml +++ b/src/plugins/value/engine/recursion.ml @@ -179,7 +179,7 @@ let make_recursion call depth = let make call = 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 + let depth = List.length previous_calls - 1 in if depth > 0 then Some (make_recursion call depth) else None diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml index 303e69ee16dde632435d82c0f774c42a3d3b122a..34ec661ec424d7d3512c5952c5700ce21c34c8ef 100644 --- a/src/plugins/value/engine/transfer_stmt.ml +++ b/src/plugins/value/engine/transfer_stmt.ml @@ -531,9 +531,9 @@ module Make (Abstract: Abstractions.Eva) = struct (* ------------------------- Make an Eval.call ---------------------------- *) (* Create an Eval.call *) - let create_call kf args = + let create_call stmt kf args = let return = Library_functions.get_retres_vi kf in - let callstack = Eva_utils.call_stack () in + let callstack = (kf, Kstmt stmt) :: Eva_utils.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 @@ -572,12 +572,12 @@ module Make (Abstract: Abstractions.Eva) = struct let arguments = List.map replace_arg call.arguments in { call with arguments; } - let make_call ~subdivnb kf arguments valuation state = + let make_call ~subdivnb stmt kf arguments valuation state = (* Evaluate the arguments of the call. *) let determinate = is_determinate kf in compute_actuals ~subdivnb ~determinate valuation state arguments >>=: fun (args, valuation) -> - let call = create_call kf args in + let call = create_call stmt kf args in let recursion = Recursion.make call in let call = Extlib.opt_fold replace_recursive_call recursion call in call, recursion, valuation @@ -756,7 +756,7 @@ module Make (Abstract: Abstractions.Eva) = struct [(Partition.Key.empty, state)] else (* Create the call. *) - let eval, alarms = make_call ~subdivnb kf args valuation state in + let eval, alarms = make_call ~subdivnb stmt kf args valuation state in Alarmset.emit ki_call alarms; let states = let+ call, recursion, valuation = eval in diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli index 76f96cf20bc10c0f141cb2ac03e1448bd620c1b8..c0335e7761b4eb99e365b9775c9ceb7061e78fc5 100644 --- a/src/plugins/value/eval.mli +++ b/src/plugins/value/eval.mli @@ -238,7 +238,7 @@ type callstack = call_site list type ('loc, 'value) call = { kf: kernel_function; (** The called function. *) callstack: callstack; (** The current callstack - (without this call). *) + (with this call on top). *) 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