diff --git a/src/kernel_services/abstract_interp/eva_types.ml b/src/kernel_services/abstract_interp/eva_types.ml
index 6d07a6664995b30734696addf631c57096f3a1f2..d7638929c79d8e4f63ce59afdae00738012fd2f8 100644
--- a/src/kernel_services/abstract_interp/eva_types.ml
+++ b/src/kernel_services/abstract_interp/eva_types.ml
@@ -20,6 +20,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+let stable_hash x = Hashtbl.seeded_hash 0 x
+
+let dkey_callstack = Kernel.register_category "callstack"
+
 module Callstack =
 struct
   module Thread = Int (* Threads are identified by integers *)
@@ -136,4 +140,51 @@ struct
     (cs.entry_point, Cil_types.Kglobal) :: l
 
   let to_legacy cs = List.rev (to_call_list cs)
+
+  (* Stable hash and pretty-printing *)
+
+  let stmt_hash s =
+    let pos = fst (Cil_datatype.Stmt.loc s) in
+    stable_hash (pos.Filepath.pos_path, pos.Filepath.pos_lnum)
+
+  let kf_hash kf = stable_hash (Kernel_function.get_name kf)
+
+  let rec calls_hash = function
+    | [] -> 0
+    | (kf, stmt) :: tl -> stable_hash (kf_hash kf, stmt_hash stmt, calls_hash tl)
+
+  let stable_hash { thread; entry_point; stack } =
+    let p = stable_hash (thread, kf_hash entry_point, calls_hash stack) in
+    p mod 11_316_496 (* 58 ** 4 *)
+
+  let base58_map = "123456789ABCDEFGHJKLMNPQRSTUVWXYZabcdefghijkmnopqrstuvwxyz"
+
+  (* Converts [i] into a fixed-length, 4-wide string in base-58 *)
+  let base58_of_int n =
+    let buf = Bytes.create 4 in
+    Bytes.set buf 0 (String.get base58_map (n mod 58));
+    let n = n / 58 in
+    Bytes.set buf 1 (String.get base58_map (n mod 58));
+    let n = n / 58 in
+    Bytes.set buf 2 (String.get base58_map (n mod 58));
+    let n = n / 58 in
+    Bytes.set buf 3 (String.get base58_map (n mod 58));
+    Bytes.to_string buf
+
+  let pretty_hash fmt callstack =
+    if Kernel.is_debug_key_enabled dkey_callstack then
+      Format.fprintf fmt "<%s> " (base58_of_int (stable_hash callstack))
+    else Format.ifprintf fmt ""
+
+  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
+
+  let pretty fmt callstack =
+    Format.fprintf fmt "@[<hv>%a" pretty_hash callstack;
+    pretty fmt callstack;
+    Format.fprintf fmt "@]"
 end
diff --git a/src/kernel_services/abstract_interp/eva_types.mli b/src/kernel_services/abstract_interp/eva_types.mli
index 57944aea8dfd6898296bd6a318ff11197b549e71..08b9105f7bb04fcdffc19ee6ab2b54473c4ba5d0 100644
--- a/src/kernel_services/abstract_interp/eva_types.mli
+++ b/src/kernel_services/abstract_interp/eva_types.mli
@@ -37,6 +37,8 @@ sig
 
   include Datatype.S_with_collections with type t = callstack
 
+  val pretty_hash : Format.formatter -> t -> unit
+  val pretty_short : Format.formatter -> t -> unit
   val pretty_debug : Format.formatter -> t -> unit
 
   val compare_lex : t -> t -> int
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 7cf6b0097b1d86f42761050b1104c3ccaf7e207d..dd1fc5ab89c864f5cd47a1fe7807df2ac7855ef4 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -139,6 +139,13 @@ module Callstack: sig
     with type t = callstack
      and module Hashtbl = Eva_types.Callstack.Hashtbl
 
+  (** Print a call stack without displaying call sites. *)
+  val pretty_short : Format.formatter -> t -> unit
+
+  (** Print a hash of the callstack when '-kernel-msg-key callstack'
+      is enabled (prints nothing otherwise). *)
+  val pretty_hash : Format.formatter -> t -> unit
+
   (** [compare_lex] compares callstack lexicographically, slightly slower
       than [compare] but in a more natural order, giving more importance
       to the function at bottom of the callstack - the first functions called. *)
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
index 6460b8d5bc2fac91104ac585f4b5b0e444a57fcb..cb693ca3c453dbab015b6d1af3a21a92a8035948 100644
--- a/src/plugins/eva/types/callstack.mli
+++ b/src/plugins/eva/types/callstack.mli
@@ -44,6 +44,13 @@ include Datatype.S_with_collections
   with type t = callstack
    and module Hashtbl = Eva_types.Callstack.Hashtbl
 
+(** Print a call stack without displaying call sites. *)
+val pretty_short : Format.formatter -> t -> unit
+
+(** Print a hash of the callstack when '-kernel-msg-key callstack'
+    is enabled (prints nothing otherwise). *)
+val pretty_hash : Format.formatter -> t -> unit
+
 (** [compare_lex] compares callstack lexicographically, slightly slower
     than [compare] but in a more natural order, giving more importance
     to the function at bottom of the callstack - the first functions called. *)