diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index 2b743f0d8540fa1d95052b20b33ff304bd1c6d2c..0e198d4b9c299e61c985e1cd04ebf93dd05f74a7 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -88,7 +88,7 @@ module Prototype = struct
       Format.fprintf fmt "%s@ {%a}" (kind_label kind) pretty_loc loc
 end
 
-include Datatype.Make (Prototype)
+include Datatype.Make_with_collections (Prototype)
 
 let pretty_as_reason fmt org =
   if not (is_unknown org)
@@ -103,6 +103,10 @@ let join t1 t2 =
 
 let is_included = equal
 
+let is_current = function
+  | Unknown | Well -> false
+  | Origin { loc } -> Cil_datatype.Location.equal loc (Cil.CurrentLoc.get ())
+
 (* Well and Unknown origins have no location information.
    Leaf origins are also imprecise, because we may create tons of those,
    that get reduced to precise values by the specifications of the function. *)
@@ -110,6 +114,67 @@ let is_precise = function
   | Unknown | Well -> false
   | Origin { kind } -> kind <> Leaf
 
+
+module History_Info = struct
+  let name = "Origin.History"
+  let dependencies = []
+  let size = 32
+end
+
+module History_Data =
+  Datatype.Triple (Datatype.Int) (Datatype.Int) (Base.SetLattice)
+module History = State_builder.Hashtbl (Hashtbl) (History_Data) (History_Info)
+
+let clear () = Id.reset (); History.clear ()
+
+let register_write bases t =
+  if not (is_unknown t) then
+    let change (w, r, b) = w+1, r, Base.SetLattice.join b bases in
+    ignore (History.memo ~change (fun _ -> 1, 0, bases) t)
+
+let register_read bases t =
+  if not (is_unknown t || is_current t) then
+    let change (w, r, b) = w, r+1, Base.SetLattice.join b bases in
+    ignore (History.memo ~change (fun _ -> 0, 1, bases) t)
+
+
+let get_history () =
+  let list = List.of_seq (History.to_seq ()) in
+  let list = List.filter (fun (_origin, (_, r, _)) -> r > 0) list in
+  let cmp (origin1, (_, r1, _)) (origin2, (_, r2, _)) =
+    let r = r2 - r1 in
+    if r <> 0 then r else compare origin1 origin2
+  in
+  List.sort cmp list
+
+let pretty_origin fmt origin =
+  match origin with
+  | Unknown -> Format.fprintf fmt "Unknown origin"
+  | Well -> Format.fprintf fmt "Initial state"
+  | Origin { kind; loc; } ->
+    let kind =
+      match kind with
+      | Misalign_read -> "misaligned read of addresses"
+      | Leaf -> "interpretation of assigns clause"
+      | Merge -> "imprecise merge of addresses"
+      | Arith -> "arithmetic operation on addresses"
+    in
+    Format.fprintf fmt "%a: %s" Cil_datatype.Location.pretty loc kind
+
+let pretty_history fmt =
+  let list = get_history () in
+  let pp_origin fmt (origin, (w, r, bases)) =
+    let bases = Base.SetLattice.filter (fun b -> not (Base.is_null b)) bases in
+    Format.fprintf fmt
+      "@[<hov 2>%a@ (read %i times, propagated %i times)@ \
+       garbled mix of &%a@]"
+      pretty_origin origin r w Base.SetLattice.pretty bases
+  in
+  if list <> [] then
+    Format.fprintf fmt
+      "@[<v 2>Origins of garbled mix generated during analysis:@,%a@]"
+      (Pretty_utils.pp_list ~sep:"@," pp_origin) list
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index a739d8dca4c4782a0f71d99b6e9a881d0e08ebe2..cfc870300dbbe77cdcbed95c3fc43a2c9984703c 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/src/kernel_services/abstract_interp/origin.mli
@@ -52,6 +52,22 @@ val is_included: t -> t -> bool
 
 val is_precise: t -> bool
 
+(** Records the write of an imprecise value of the given bases,
+    with the given origin. *)
+val register_write: Base.SetLattice.t -> t -> unit
+
+(** Records the read of an imprecise value of the given bases,
+    with the given origin. *)
+val register_read: Base.SetLattice.t -> t -> unit
+
+(** Pretty-print a summary of the origins of imprecise values recorded
+    by [register_write] and [register_read] above. *)
+val pretty_history: Format.formatter -> unit
+
+(** Clears the history of origins saved by [register_write] and
+    [register_read] above. *)
+val clear: unit -> unit
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
index ae31230b0e8ede332ce8a485e99431acb7c51d83..a39492a45942563e4e8cdaaa3368a8812ff5480f 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -76,6 +76,10 @@ module Queries = struct
   let is_float v =
     Cvalue.V.(is_included v top_float) && Cvalue.V.contains_non_zero v
 
+  let read_garbled_mix = function
+    | Cvalue.V.Top (bases, origin) -> Origin.register_read bases origin
+    | _ -> ()
+
   let extract_scalar_lval state lval typ loc =
     let process_one_loc = eval_one_loc state lval typ in
     let acc = Cvalue.V.bottom, None in
@@ -88,6 +92,7 @@ module Queries = struct
     let incompatible_type = is_float value <> Cil.isFloatingType typ in
     let origin = if incompatible_type then Some value else None in
     let value = Cvalue_forward.reinterpret typ value in
+    read_garbled_mix value;
     if Cvalue.V.is_bottom value
     then `Bottom, alarms
     else `Value (value, origin), alarms
@@ -106,6 +111,7 @@ module Queries = struct
         let value = Cvalue.V_Offsetmap.find_imprecise_everywhere offsm in
         let alarms = indeterminate_alarms lval value in
         let v = Cvalue.V_Or_Uninitialized.get_v value in
+        read_garbled_mix v;
         let v = if Cvalue.V.is_bottom v then `Bottom else `Value (v, None) in
         v, alarms
 
diff --git a/src/plugins/eva/domains/cvalue/warn.ml b/src/plugins/eva/domains/cvalue/warn.ml
index 402f79f5702e6ba776db5bdded866e41561d0d50..81c8eede4b2324059255c60c2891d24d508926bd 100644
--- a/src/plugins/eva/domains/cvalue/warn.ml
+++ b/src/plugins/eva/domains/cvalue/warn.ml
@@ -99,7 +99,8 @@ let warn_imprecise_lval_read lv loc contents =
    [exp_val] is the part of the evaluation of [exp] that is imprecise. *)
 let warn_right_exp_imprecision lv loc_lv exp_val =
   match exp_val with
-  | Location_Bytes.Top(_topparam,origin) ->
+  | Location_Bytes.Top(topparam, origin) ->
+    Origin.register_write topparam origin;
     Self.warning ~wkey:Self.wkey_garbled_mix_write ~once:true ~current:true
       "@[<v>@[Assigning imprecise value to %a%t.@]%a%t@]"
       Printer.pp_lval lv
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 09a3b4d353b06d83d8a5a5c13396a4b28c90765f..5904de59dc64e14df9227679eda469e699d7e8bd 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -102,6 +102,7 @@ let pre_analysis () =
      degeneration states *)
   Eva_utils.DegenerationPoints.clear ();
   Cvalue.V.clear_garbled_mix ();
+  Origin.clear ();
   Eva_utils.clear_call_stack ()
 
 let post_analysis_cleanup ~aborted =
diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml
index bd0b649c6bdaa5c7d80f0a64e713d08caf666c63..32174a32d2e538f28a4746eea222bf4087f7c80d 100644
--- a/src/plugins/eva/engine/transfer_specification.ml
+++ b/src/plugins/eva/engine/transfer_specification.ml
@@ -311,16 +311,18 @@ module Make
       | Some location ->
         let loc = Precise_locs.imprecise_location (get_ploc location) in
         let cvalue = Cvalue.Model.find cvalue_state loc in
-        if Cvalue.V.is_imprecise cvalue
-        then
-          begin
+        begin
+          match cvalue with
+          | Top (bases, origin) ->
             ignore (Locations.Location_Bytes.track_garbled_mix cvalue);
+            Origin.register_write bases origin;
             Self.warning ~current:true ~once:true
               ~wkey:Self.wkey_garbled_mix_assigns
               "The specification of function %a has generated a garbled mix \
                for %a."
               Kernel_function.pretty kf pp_assign_clause (Assign, assign)
-          end
+          | _ -> ()
+        end
     in
     let check_one_state state =
       let cvalue_state = get_cvalue_or_top state in
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 73d1517b788b01dac7dfa5f7aeb7e0c589e5bb6c..3f1b88be0bf95ab1f6fa9014fcd6cde68027175c 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -286,6 +286,7 @@ let lval_to_exp =
     (fun lv -> Cil.new_exp ~loc:Cil_datatype.Location.unknown (Lval lv))
 
 let dump_garbled_mix () =
+  Self.warning ~wkey:Self.wkey_garbled_mix_summary "%t" Origin.pretty_history;
   let l = Cvalue.V.get_garbled_mix () in
   if l <> [] then
     let pp_one fmt v = Format.fprintf fmt "@[<hov 2>%a@]" Cvalue.V.pretty v in