Frama-C API - Location_Bytes
Association between bases and offsets in byte.
module M : sig ... end
type t = private
| Top of Base.SetLattice.t * Origin.t
(*Garbled mix of the addresses in the set
*)| Map of M.t
(*Precise set of addresses+offsets
*)
Those locations 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.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 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_Intersects with type t := t
type widen_hint = Ival.widen_hint
val widen : ?size:Integer.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 packed_descr : Structural_descr.pack
Packed version of the descriptor.
val reprs : t list
List of representants of the descriptor.
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
.
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
add b i loc
binds b
to i
in loc
when i
is not Ival.bottom
, and returns bottom
otherwise.
val replace_base : Base.substitution -> t -> bool * t
replace_base subst loc
changes the location loc
by substituting the pointed bases according to subst
. If substitution
conflates different bases, the offsets bound to these bases are joined.
Over-approximation of difference. arg2
needs to be exact or an under_approximation.
Over- and under-approximation of shifting the value by the given Ival.
val sub_pointwise : ?factor:Int_Base.t -> t -> t -> Ival.t
Subtracts the offsets of two locations loc1
and loc2
. Returns the pointwise subtraction of their offsets off1 - factor * off2
. factor
defaults to 1
.
Subtracts the offsets of two locations. 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 inject_top_origin : Origin.t -> Base.Hptset.t -> t
inject_top_origin origin bases
creates a garbled mix of bases bases
with origin origin
.
Fold on all the bases of the location, including Top bases
.
Fold with offsets, including in the case Top bases
. In this case, Ival.top
is supplied to the iterator.
fold_enum f loc acc
enumerates the locations in acc
, 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 loc
is Top _
or if one offset cannot be enumerated.
Builds a sequence of all bases (with their offsets) of the location.
val cached_fold : cache_name:string -> temporary:bool -> f:(Base.t -> Ival.t -> 'a) -> projection:(Base.t -> Ival.t) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a
Cached version of fold_i
, for advanced users
Number of locations
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
.
if there is only one base b
in the location, then returns the pair b,o
where o
are the offsets associated to b
.
if there is only one binding b -> o
in the location (that is, only one base b
with cardinal_zero_or_one o
), returns the pair b,o
.
val get_bases : t -> Base.SetLattice.t
Returns the bases the location may point to. Never fails, but may return Base.SetLattice.Top
.
Local variables inside locations
contains_addresses_of_locals is_local loc
returns true
if loc
contains the address of a variable for which is_local
returns true
remove_escaping_locals is_local v
removes from v
the information associated with bases for which is_local
returns true
. The returned boolean indicates that v
contained some locals.
val contains_addresses_of_any_locals : t -> bool
contains_addresses_of_any_locals loc
returns true
iff loc
contains the address of a local variable or of a formal variable.
Misc
val is_relationable : t -> bool
is_relationable loc
returns true
iff loc
represents a single memory location.