diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli index 9841b2a3a9d33975ff7d4ecdb73543f8fc9bff94..eb0c7aaecbdee05569a5ae9011f86b9cdc18cdf5 100644 --- a/src/plugins/eva/Eva.mli +++ b/src/plugins/eva/Eva.mli @@ -118,8 +118,6 @@ module Callstack: sig module Call : Datatype.S with type t = call - module Calls : Datatype.S with type t = call list - (** Eva callstacks. *) type callstack = { thread: int; @@ -132,15 +130,8 @@ module Callstack: sig include Datatype.S_with_collections with type t = callstack - (** Prints a callstack without displaying call sites. - - ~hide_hash forces printing wihout hash (see {!pretty_hash}), - useful when a precise format is expected. - - ~sep is the separator between function names. - - ~rev reverses the list (if true, print caller -> callee -> ...). - *) - val pretty_short : - hide_hash:bool -> sep:Pretty_utils.sformat -> rev:bool -> Format.formatter -> - t -> unit + (** Prints a callstack without displaying call sites. *) + val pretty_short : Format.formatter -> t -> unit (** Prints a hash of the callstack when '-kernel-msg-key callstack' is enabled (prints nothing otherwise). *) diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml index 8523e769449289777d4c815f2dbf24437d42695a..a3bd81ebe62d3c50591a9acfb9368ae0cc733e7c 100644 --- a/src/plugins/eva/engine/compute_functions.ml +++ b/src/plugins/eva/engine/compute_functions.ml @@ -261,8 +261,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct | Kstmt stmt when Parameters.ValShowProgress.get () -> Self.feedback "@[computing for function %a.@\nCalled from %a.@]" - (Callstack.pretty_short ~hide_hash:false ~sep:" <- " ~rev:true) - call.callstack + Callstack.pretty_short call.callstack Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc stmt) | _ -> () end; diff --git a/src/plugins/eva/types/callstack.ml b/src/plugins/eva/types/callstack.ml index 710175a51988bd7bdcb334887459663fa6e3b261..fec3d18684256394e847727bf854d578c0f3e644 100644 --- a/src/plugins/eva/types/callstack.ml +++ b/src/plugins/eva/types/callstack.ml @@ -172,11 +172,10 @@ let pretty_hash fmt callstack = Format.fprintf fmt "<%s> " (base58_of_int (stable_hash callstack)) else Format.ifprintf fmt "" -let pretty_short ~hide_hash ~sep ~rev fmt callstack = - if not hide_hash then Format.fprintf fmt "%a" pretty_hash callstack; - let list = to_kf_list callstack in - let list = if rev then List.rev list else list in - Pretty_utils.pp_flowlist ~left:"" ~sep ~right:"" +let pretty_short fmt callstack = + Format.fprintf fmt "%a" pretty_hash callstack; + let list = List.rev (to_kf_list callstack) in + Pretty_utils.pp_flowlist ~left:"" ~sep:" <- " ~right:"" (fun fmt kf -> Kernel_function.pretty fmt kf) fmt list diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli index abc23716752331631441d575cf3868728a42edd7..0340490e58ec65c80c72e53357be16657c40c4aa 100644 --- a/src/plugins/eva/types/callstack.mli +++ b/src/plugins/eva/types/callstack.mli @@ -27,8 +27,6 @@ type call = Cil_types.kernel_function * Cil_types.stmt module Call : Datatype.S with type t = call -module Calls : Datatype.S with type t = call list - (** Eva callstacks. *) type callstack = { thread: int; @@ -41,15 +39,8 @@ type callstack = { include Datatype.S_with_collections with type t = callstack -(** Prints a callstack without displaying call sites. - - ~hide_hash forces printing wihout hash (see {!pretty_hash}), - useful when a precise format is expected. - - ~sep is the separator between function names. - - ~rev reverses the list (if true, print caller -> callee -> ...). -*) -val pretty_short : - hide_hash:bool -> sep:Pretty_utils.sformat -> rev:bool -> Format.formatter -> - t -> unit +(** Prints a callstack without displaying call sites. *) +val pretty_short : Format.formatter -> t -> unit (** Prints a hash of the callstack when '-kernel-msg-key callstack' is enabled (prints nothing otherwise). *)