Frama-C:
Plug-ins:
Libraries:

Frama-C API - V_Or_Uninitialized

Values with 'undefined' and 'escaping addresses' flags.

type t =
  1. | C_uninit_esc of V.t
  2. | C_uninit_noesc of V.t
  3. | C_init_esc of V.t
  4. | C_init_noesc of 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.S with type t := t and type widen_hint = Locations.Location_Bytes.widen_hint
include Lattice_type.Join_Semi_Lattice with type t := t

datatype of element of the lattice

include Datatype.S with type t := t
include Datatype.S_no_copy with type t := t
include Datatype.Ty with type t := t
val ty : t Type.t
val name : string

Unique name of the datatype.

val descr : t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val pretty : Stdlib.Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

val mem_project : (Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

val join : t -> t -> t

over-approximation of union

val is_included : t -> t -> bool

is first argument included in the second?

include Lattice_type.With_Cardinal_One with type t := t
val cardinal_zero_or_one : t -> bool

Hints for the widening.

val widen : ?size:Integer.t -> ?hint:widen_hint -> t -> t -> t

widen ~size ~hint v1 v2 is an over-approximation of join v1 v2. size is the size (in bits) of the widened value, and hint is some hint for the widening.

val pretty_typ : Cil_types.typ option -> t Pretty_utils.formatter

Isotropy

val is_isotropic : t -> bool

Are the bits independent?

val topify_with_origin : Origin.t -> t -> t

Force a value to be isotropic, when a loss of imprecision occurs. The resulting value must verify is_isotropic.

Reading bits of values

val extract_bits : topify:Origin.kind -> start:Integer.t -> stop:Integer.t -> size:Integer.t -> t -> bool * t

Extract the bits between start and stop in the value of type t, assuming this value has size bits. Return the corresponding value, and a boolean indicating that an imprecision occurred during the operation. In the latter case, the origin of the imprecision is flagged as having kind topify.

val shift_bits : topify:Origin.kind -> offset:Integer.t -> size:Integer.t -> t -> t

Left-shift the given value, of size size, by offset bits. topify indicates which operation caused this shift to take place, for imprecision tracking.

val merge_distinct_bits : topify:Origin.kind -> conflate_bottom:bool -> t -> t -> t

Merge the bits of the two given values, that span disjoint bit ranges by construction. (So either an abstraction of + or | are correct implementations.)

The conflate_bottom argument deals with bottom values in either of the arguments. If conflate_bottom holds, any pre-existing bottom value must result in bottom. Otherwise, the bottom value is ignored.

topify indicates which operation caused this merge to take place, for imprecision tracking.

val merge_neutral_element : t

Value that can be passed to merge_distinct_bits as the starting value. This value must be neutral wrt. merging of values.

val anisotropic_cast : size:Integer.t -> t -> t

Optionnally change the representation of the given value, under the assumption that it fits in size bits. Returning the value argument is alwas correct.

include Lattice_type.With_Under_Approximation with type t := t

under-approximation of union

val meet : t -> t -> t

under-approximation of intersection

include Lattice_type.With_Narrow with type t := t
val narrow : t -> t -> t

over-approximation of intersection

include Lattice_type.With_Top with type t := t
val top : t

largest element

include Lattice_type.With_Top_Opt with type t := t
val top_opt : t option

optional largest element

val get_v : t -> V.t
val make : initialized:bool -> escaping:bool -> V.t -> t
val inject_or_bottom : t Lattice_bounds.or_bottom -> t
val bottom : 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 : 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 -> (V.M.key -> bool) -> t -> bool * t
val replace_base : Base.substitution -> t -> bool * t
val map : (V.t -> V.t) -> t -> t
val map2 : (V.t -> V.t -> V.t) -> t -> t -> t

initialized/escaping information is the join of the information on each argument.