sig
type clobbered_set = { mutable clob : Base.SetLattice.t; }
val bottom : unit -> Locals_scoping.clobbered_set
val top : unit -> Locals_scoping.clobbered_set
val remember_bases_with_locals :
Locals_scoping.clobbered_set -> Base.SetLattice.t -> unit
val remember_if_locals_in_value :
Locals_scoping.clobbered_set -> Locations.location -> Cvalue.V.t -> unit
val remember_if_locals_in_offsetmap :
Locals_scoping.clobbered_set ->
Locations.location -> Cvalue.V_Offsetmap.t -> unit
type topify_offsetmap =
Cvalue.V_Offsetmap.t -> Base.SetLattice.t * Cvalue.V_Offsetmap.t
type topify_offsetmap_approx =
exact:bool -> Locals_scoping.topify_offsetmap
type topify_state = Cvalue.Model.t -> Cvalue.Model.t
val offsetmap_top_addresses_of_locals :
(Base.t -> bool) -> Locals_scoping.topify_offsetmap_approx
val state_top_addresses_of_locals :
exact:bool ->
(Base.t -> Base.SetLattice.t -> unit) ->
Locals_scoping.topify_offsetmap_approx ->
Locals_scoping.clobbered_set -> Locals_scoping.topify_state
val top_addresses_of_locals :
Cil_types.fundec ->
Locals_scoping.clobbered_set ->
Locals_scoping.topify_offsetmap * Locals_scoping.topify_state
val block_top_addresses_of_locals :
Cil_types.fundec ->
Locals_scoping.clobbered_set ->
Cil_types.block list -> Locals_scoping.topify_state
end