Frama-C API - V
Values.
Values are essentially bytes-indexed locations, the NULL base representing basic integers or float. Operations that are not related to locations (ie that are not present in Location_Bytes
) are defined below.
include module type of Locations.Location_Bytes with type M.t = Locations.Location_Bytes.M.t and type t = Locations.Location_Bytes.t
Association between bases and offsets in byte.
module M : sig ... end
type t = Locations.Location_Bytes.t =
| 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
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
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
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 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_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.
include Offsetmap_lattice_with_isotropy.S with type t := t and type widen_hint := 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 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
.
val bottom : t
smallest element
include Lattice_type.With_Cardinal_One with type t := t
val cardinal_zero_or_one : t -> bool
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.
Isotropy
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 pretty_typ : Cil_types.typ option -> t Pretty_utils.formatter
val is_arithmetic : t -> bool
Returns true if the value may not be a pointer.
val is_imprecise : t -> bool
val is_topint : t -> bool
val is_bottom : t -> bool
val is_isotropic : t -> bool
val contains_zero : t -> bool
val contains_non_zero : t -> bool
val of_char : char -> t
val of_int64 : int64 -> t
val backward_mult_int_left : right:t -> result:t -> t option Lattice_bounds.or_bottom
val backward_comp_int_left : Abstract_interp.Comp.t -> t -> t -> t
val backward_comp_float_left_true : Abstract_interp.Comp.t -> Fval.kind -> t -> t -> t
val backward_comp_float_left_false : Abstract_interp.Comp.t -> Fval.kind -> t -> t -> t
val forward_comp_int : signed:bool -> Abstract_interp.Comp.t -> t -> t -> Abstract_interp.Comp.result
val inject_comp_result : Abstract_interp.Comp.result -> t
val inject_int : Abstract_interp.Int.t -> t
val interp_boolean : contains_zero:bool -> contains_non_zero:bool -> t
val cast_int_to_int : size:Abstract_interp.Int.t -> signed:bool -> t -> t
cast_int_to_int ~size ~signed v
applies to the abstract value v
the conversion to the integer type described by size
and signed
. Offsets of bases other than NULL are not clipped. If they were clipped, they should be clipped at the validity of the base. The C standard does not say that p+(1ULL<<32+1)
is the same as p+1
, it says that p+(1ULL<<32+1)
is invalid.
val reinterpret_as_float : Cil_types.fkind -> t -> t
val add_untyped : factor:Int_Base.t -> t -> t -> t
add_untyped ~factor e1 e2
computes e1+factor*e2
using C semantic for +, i.e. ptr+v
is add_untyped ~factor:sizeof( *ptr ) ptr v
. (Thus, factor
is in bytes.) This function handles simultaneously PlusA, MinusA, PlusPI, MinusPI and sometimes MinusPP, by setting factor
accordingly. This is more precise than having multiple functions, as computations such as (int)&t[1] - (int)&t[2]
would not be treated precisely otherwise.
val add_untyped_under : factor:Int_Base.t -> t -> t -> t
Under-approximating variant of add_untyped
. Takes two under-approximation, and returns an under-approximation.
val sub_untyped_pointwise : ?factor:Int_Base.t -> t -> t -> Ival.t
See Locations.sub_pointwise
. In this module, factor
is expressed in bytes.
val all_values : size:Abstract_interp.Int.t -> t -> bool
all_values ~size v
returns true iff v contains all integer values representable in size
bits.
val create_all_values : signed:bool -> size:int -> t
val cardinal_estimate : t -> size:Abstract_interp.Int.t -> Abstract_interp.Int.t
cardinal_estimate v ~size
returns an estimation of the cardinal of v
, knowing that v
fits in size
bits.