DecayMap (soteria-rust.Soteria_rust

type t

val empty : t

val pp : Stdlib.Format.formatter -> t -> unit

val decay : 
  expose:bool ->
  size:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  align:[< Soteria_rust_lib.Typed.T.nonzero ] Typed.t ->
  [< Soteria_rust_lib.Typed.T.sloc ] Typed.t ->
  t ->
  (Soteria_rust_lib.Typed.T.sint Typed.t * t) Rustsymex.t

Decays the given location into an integer, updating the decay map accordingly. If expose is true, the provenance is marked as exposed, and can be retrieved later with from_exposed. Returns the decayed integer, along with the updated decay map.

val from_exposed : 
  [< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  t ->
  ((Soteria_rust_lib.Typed.T.sloc Typed.t
    * Soteria_rust_lib.Typed.T.sint Typed.t)
     option
   * t)
    Rustsymex.t

Tries finding, for the given integer, the matching provenance in the decay map. If found, it returns that provenance, along with the exposed address for that allocation at offset 0. Otherwise returns None.