module V_Or_Uninitialized: sig
.. end
Values with 'undefined' and 'escaping addresses' flags.
type
t =
| |
C_uninit_esc of Cvalue.V.t |
| |
C_uninit_noesc of Cvalue.V.t |
| |
C_init_esc of Cvalue.V.t |
| |
C_init_noesc of Cvalue.V.t |
Semantics of the constructors:
C_init_*
: definitely initialized
C_uninit_*
: possibly uninitialized
C_*_noesc
: never contains escaping addresses
C_*_esc
: may contain escaping addresses
C_uninit_noesc V.bottom
: guaranteed to be uninitialized
C_init_esc V.bottom
: guaranteed to be an escaping address
C_uninit_esc V.bottom
: either uninitialized or an escaping address
C_init_noesc V.bottom
: "real" bottom, with an empty concretization.
Corresponds to an unreachable state.
include Offsetmap_lattice_with_isotropy
include Lattice_type.With_Under_Approximation
include Lattice_type.With_Narrow
include Lattice_type.With_Top
include Lattice_type.With_Top_Opt
val get_v : t -> Cvalue.V.t
val make : initialized:bool ->
escaping:bool -> Cvalue.V.t -> t
val is_bottom : t -> bool
val is_initialized : t -> bool
is_initialized v = true
implies v
is definitely initialized.
is_initialized v = false
implies v
is possibly uninitialized.
is_initialized v = false && is_bottom v
implies v
is definitely
uninitialized.
val is_noesc : t -> bool
is_noesc v = true
implies v
has no escaping addresses.
is_noesc v = false
implies v
may have escaping addresses.
val is_indeterminate : t -> bool
is_indeterminate v = false
implies v
only has definitely initialized
values and non-escaping addresses.
is_indeterminate v = true
implies v
may have uninitialized values
and/or escaping addresses.
val uninitialized : t
Returns the canonical representant of a definitely uninitialized value.
val initialized : Cvalue.V.t -> t
initialized v
returns the definitely initialized, non-escaping
representant of v
.
val reduce_by_initializedness : bool -> t -> t
reduce_by_initializedness initialized v
reduces v
so that its result
r
verifies \initialized(r)
if initialized
is true
, and
!\initialized(r)
otherwise.
val reduce_by_danglingness : bool -> t -> t
reduce_by_danglingness dangling v
reduces v
so that its result r
verifies \dangling(r)
if dangling
is true
, and
!\dangling(r)
otherwise.
val remove_indeterminateness : t -> t
Remove 'unitialized' and 'escaping addresses' flags from the argument
val unspecify_escaping_locals : exact:bool ->
(Cvalue.V.M.key -> bool) ->
t ->
Base.SetLattice.t * t
val map : (Cvalue.V.t -> Cvalue.V.t) ->
t -> t
val map2 : (Cvalue.V.t -> Cvalue.V.t -> Cvalue.V.t) ->
t ->
t -> t
initialized/escaping information is the join of the information
on each argument.