package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-30.0-beta-Zinc.tar.gz

sha256=93a291a8764644df2f3618d7ea18258b5fbe0912ec98dfdfd180967afdf24474

doc/frama-c.kernel/Frama_c_kernel/Cvalue/V_Or_Uninitialized/index.html

Module `Cvalue.V_Or_Uninitialized`

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

type t =

| C_uninit_esc of V.t
| C_uninit_noesc of V.t
| C_init_esc of V.t
| 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.Bounded_Join_Semi_Lattice with type t := t

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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.(=).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

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

Pretty print each value in an user-friendly way.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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?

val bottom : t

smallest element

include Lattice_type.With_Cardinal_One with type t := t

val cardinal_zero_or_one : t -> bool

type widen_hint = Locations.Location_Bytes.widen_hint

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

val link : t -> 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 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.