Module Soteria_c_lib.Fun_ctx

module Bidirectional_map : sig ... end
type t = {
  1. counter : Soteria.Soteria_std.Z.t;
  2. bmap : Bidirectional_map.t;
}
val empty : t
val declare_fn : Bidirectional_map.M.key -> t -> t
val of_linked_program : Ail_tys.linked_program -> t
val decay_fn_sym : Cerb_frontend.Symbol.sym -> t -> [> Soteria__Bv_values__Typed.T.sloc ] Soteria__Bv_values__Typed.t Csymex.t
val get_sym : 'a Typed.t -> t -> Symbol_std.t Csymex.t