Module Cvalue.V_Or_Uninitialized

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 'uninitialized' and 'escaping addresses' flags from the argument

val unspecify_escaping_locals : exact:bool ->
       (Cvalue.V.M.key -> bool) ->
       t -> bool * t

val replace_base : Base.substitution ->
       t -> bool * 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.