Frama-C:
Plug-ins:
Libraries:

Frama-C API - Bytes

Association between bases and offsets in byte.

  • before 33.0-Arsenic

    was Locations.Location_Bytes

module M : sig ... end
type t = private
  1. | Top of Base.SetLattice.t * Origin.t
    (*

    Garbled mix of the addresses in the set

    *)
  2. | Map of M.t
    (*

    Precise set of addresses+offsets

    *)

Address sets have a lattice structure, including standard operations such as join, narrow, etc.

include Lattice_type.AI_Lattice_with_cardinal_one with type t := t
include Lattice_type.Bottom_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 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_Top with type t := t
val top : t

largest element

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

over-approximation of intersection

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_Intersects with type t := t
val intersects : t -> t -> bool

intersects t1 t2 returns true iff the intersection of t1 and t2 is non-empty.

type widen_hint = Ival.widen_hint
val widen : ?size:Z.t -> ?hint:widen_hint -> t -> t -> t
include Datatype.S_with_collections with type t := t
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 datatype_name : string

Unique name of the datatype.

val datatype_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.

module Set : Datatype.Set with type elt = t
module Map : Datatype.Map with type key = t
module Hashtbl : Datatype.Hashtbl with type key = t
val singleton_zero : t

the set containing only the value for to the C expression 0

val singleton_one : t

the set containing only the value 1

val zero_or_one : t
val is_zero : t -> bool
val is_bottom : t -> bool
val top_int : t
val top_float : t
val top_single_precision_float : t
val inject : Base.t -> Ival.t -> t
val inject_ival : Ival.t -> t
val inject_float : Fval.F.t -> t
val add : Base.t -> Ival.t -> t -> t

add b i addr binds b to i in addr when i is not Ival.bottom, and returns bottom otherwise.

val replace_base : Base.substitution -> t -> bool * t

replace_base subst addr changes addresses addr by substituting the pointed bases according to subst. If substitution conflates different bases, the offsets bound to these bases are joined.

val overlaps : partial:bool -> size:Z.t -> t -> t -> bool

Is there a possibly non-empty intersection between two given locations represented by the starting addresses and a given size? If partial is true, returns true if the two locations may be overlapping without being equal. If partial is false, also returns true if the two locations may be equal. Returns false when the two locations cannot be overlapping.

val diff : t -> t -> t

Over-approximation of difference. arg2 needs to be exact or an under_approximation.

val diff_if_one : t -> t -> t

Over-approximation of difference. arg2 can be an over-approximation.

val shift : Ival.t -> t -> t
val shift_under : Ival.t -> t -> t

Over- and under-approximation of shifting the value by the given Ival.

val sub_pointwise : ?factor:Z.t -> t -> t -> Ival.t

Subtracts the offsets of two address sets addr1 and addr2. Returns the pointwise subtraction of their offsets off1 - factor * off2. factor defaults to 1.

val sub_pointer : t -> t -> t

Subtracts the offsets of two address sets. Same as sub_pointwise factor:1, except that garbled mixes from operands are propagated into the result.

val topify : Origin.kind -> t -> t

topify kind v converts v to a garbled mix of the addresses pointed to by v, with origin kind. Returns v unchanged if it is bottom, the singleton zero or already a garbled mix.

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

Same as topify above with the given origin.

val inject_top_origin : Origin.t -> Base.Hptset.t -> t

inject_top_origin origin bases creates a garbled mix of bases bases with origin origin.

val top_with_origin : Origin.t -> t

Completely imprecise value. Use only as last resort.

val fold_bases : (Base.t -> 'a -> 'a) -> t -> 'a -> 'a

Fold on all the bases of the address sets, including Top bases.

val fold_i : (Base.t -> Ival.t -> 'a -> 'a) -> t -> 'a -> 'a

Fold with offsets.

val fold_topset_ok : (Base.t -> Ival.t -> 'a -> 'a) -> t -> 'a -> 'a

Fold with offsets, including in the case Top bases. In this case, Ival.top is supplied to the iterator.

val fold_enum : (t -> 'a -> 'a) -> t -> 'a -> 'a

fold_enum f addr acc enumerates addresses in addr, and passes them to f. Make sure to call cardinal_less_than before calling this function, as all possible combinations of bases/offsets are presented to f. Raises Abstract_interp.Error_Top if addr is Top _ or if one offset cannot be enumerated.

val to_seq_i : t -> (Base.t * Ival.t) Stdlib.Seq.t

Builds a sequence of all bases (with their offsets) of the address set.

val cached_fold : cache:Hptmap_sig.cache_type -> f:(Base.t -> Ival.t -> 'a) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a

Cached version of fold_i, for advanced users

val for_all : (Base.t -> Ival.t -> bool) -> t -> bool
val exists : (Base.t -> Ival.t -> bool) -> t -> bool
val filter_base : (Base.t -> bool) -> t -> t

Number of addresses

val cardinal_zero_or_one : t -> bool
val cardinal_less_than : t -> int -> int

cardinal_less_than v card returns the cardinal of v if it is less than card, or raises Not_less_than.

val cardinal : t -> Z.t option

None if the cardinal is unbounded

val find_lonely_key : t -> Base.t * Ival.t

if there is only one base b in the address set, then returns the pair b,o where o are the offsets associated to b.

  • raises Not_found

    otherwise.

val find_lonely_binding : t -> Base.t * Ival.t

if there is only one binding b -> o in the address set (that is, only one base b with cardinal_zero_or_one o), returns the pair b,o.

  • raises Not_found

    otherwise

val find : Base.t -> t -> Ival.t

Destructuring

val find_or_bottom : Base.t -> M.t -> Ival.t
val split : Base.t -> t -> Ival.t * t
val get_bases : t -> Base.SetLattice.t

Returns the bases the addresses may point to. Never fails, but may return Base.SetLattice.Top.

Local variables inside locations

val contains_addresses_of_locals : (M.key -> bool) -> t -> bool

contains_addresses_of_locals is_local addr returns true if addr contains the address of a variable for which is_local returns true

val remove_escaping_locals : (M.key -> bool) -> t -> bool * t

remove_escaping_locals is_local addr removes from addr the information associated with bases for which is_local returns true. The returned boolean indicates that addr contained some locals.

val contains_addresses_of_any_locals : t -> bool

contains_addresses_of_any_locals addr returns true iff addr contains the address of a local variable or of a formal variable.

Misc

val is_relationable : t -> bool

is_relationable addr returns true iff addr represents a single memory address.

val may_reach : Base.t -> t -> bool

may_reach base addr is true if base might be accessed from addr.