module Locals_scoping:sig
..end
type
clobbered_set = {
|
mutable clob : |
val structural_descr : Structural_descr.t
val bottom : unit -> clobbered_set
val top : unit -> clobbered_set
val remember_bases_with_locals : clobbered_set -> Base.SetLattice.t -> unit
val remember_if_locals_in_value : clobbered_set -> Locations.location -> Cvalue.V.t -> unit
remember_locals_in_value clob loc v
adds all bases pointed to by loc
to clob
if v
contains the address of a local or formalval remember_if_locals_in_offsetmap : clobbered_set ->
Locations.location -> Cvalue.V_Offsetmap.t -> unit
val offsetmap_contains_local : Cvalue.V_Offsetmap.t -> bool
typetopify_offsetmap =
Cvalue.V_Offsetmap.t -> Base.SetLattice.t * Cvalue.V_Offsetmap.t
typetopify_offsetmap_approx =
exact:bool -> topify_offsetmap
exact
is false, references to locals are both kept and
flagged as being escaping addresses.typetopify_state =
Cvalue.Model.t -> Cvalue.Model.t
val offsetmap_top_addresses_of_locals : (Base.t -> bool) -> topify_offsetmap_approx
offsetmap_top_addresses_of_locals is_local
returns a function that
topifies all the parts of an offsetmap that contains a pointer verifying
is_local
. For efficicent reasons, this function is meant to be partially
applied to its first argument.val state_top_addresses_of_locals : exact:bool ->
(Base.t -> Base.SetLattice.t -> unit) ->
topify_offsetmap_approx ->
clobbered_set -> topify_state
state_top_addresses_of_locals exact warn topoffsm clob
generalizes
topoffsm
into a function that topifies a memory state. topoffsm
is
called only on the offsetmaps bound to the bases in clob
. The exact
argument is passed to topoffsm
. If escaping locals locals
are referenced
in the offsetmap bound to b
, warn b locals
is called.val top_addresses_of_locals : Cil_types.fundec ->
clobbered_set ->
topify_offsetmap * topify_state
val block_top_addresses_of_locals : Cil_types.fundec ->
clobbered_set ->
Cil_types.block list -> topify_state
val state_top_addresses : Cil_types.fundec ->
clobbered_set ->
Cil_types.varinfo list -> Cvalue.Model.t -> Cvalue.Model.t
state_top_addresses kf clob l state
topifies all references to the
variables in l
. For efficiency reasons, only the variables referenced
in clob
. Indeed, by construction, clob
should be an over-approximation
of the variables that may contain a reference to l
.
This function is the one that should be used in Eva.