package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 and type numerical_widen_hint = Locations.Location_Bytes.numerical_widen_hint and type size_widen_hint = Locations.Location_Bytes.size_widen_hint

Association between bases and offsets in byte.

module M : sig ... end
type t = Locations.Location_Bytes.t =
  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

    *)

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

largest element

include Lattice_type.With_Widening with type t := t with type widen_hint := widen_hint
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.

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
val inject : Base.t -> Ival.t -> t
val inject_ival : Ival.t -> t
val add : Base.t -> Ival.t -> t -> 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.

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: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.

val sub_pointer : t -> t -> t

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_arith_origin : t -> t

Topifying of values, in case of imprecise accesses

val topify_misaligned_read_origin : t -> t
val topify_merge_origin : t -> t
val topify_leaf_origin : t -> t
val topify_with_origin_kind : Origin.kind -> t -> t
val inject_top_origin : Origin.t -> Base.Hptset.t -> t

inject_top_origin origin p creates a top with origin origin and additional information param

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 location, including Top bases.

  • raises Error_Top

    in the case Top Top.

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

Fold with offsets.

  • raises Error_Top

    in the cases Top Top, Top bases.

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.

  • raises Error_Top

    in the case Top Top.

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

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.

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

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

  • raises Error_Top

    in the cases Top _.

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

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

val cardinal : t -> Integer.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 location, 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 location (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 location 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 loc returns true if loc 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 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.

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

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

val get_garbled_mix : unit -> t list

All the garbled mix that have been created so far, sorted by "temporal" order of emission.

val clear_garbled_mix : unit -> unit

Clear the information on created garbled mix.

val do_track_garbled_mix : bool -> unit
val track_garbled_mix : t -> t
include Offsetmap_lattice_with_isotropy.S with type t := t and type numerical_widen_hint := numerical_widen_hint and type size_widen_hint := size_widen_hint 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 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?

val bottom : t

smallest element

include Lattice_type.With_Widening with type t := t and type widen_hint = size_widen_hint * numerical_widen_hint with type widen_hint := widen_hint
val widen : widen_hint -> t -> t -> t

widen h t1 t2 is an over-approximation of join t1 t2. Assumes is_included t1 t2

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

Isotropy

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.

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.

exception Not_based_on_null
val project_ival : t -> Ival.t

Raises Not_based_on_null if the value may be a pointer.

val project_float : t -> Fval.t

Raises Not_based_on_null if the value may be a pointer.

val project_ival_bottom : t -> Ival.t
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 inject_float : Fval.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 reinterpret_as_int : signed:bool -> size:Integer.t -> t -> t
val cast_float_to_float : Fval.kind -> t -> t
val cast_float_to_int : signed:bool -> size:int -> t -> t
val cast_float_to_int_inverse : single_precision:bool -> t -> t option
val cast_int_to_float : Fval.kind -> t -> t
val cast_int_to_float_inverse : single_precision:bool -> t -> t option
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 mul : t -> t -> t
val div : t -> t -> t
val c_rem : t -> t -> t
val shift_right : t -> t -> t
val shift_left : t -> t -> t
val bitwise_and : t -> t -> t
val bitwise_xor : t -> t -> t
val bitwise_or : t -> t -> t
val bitwise_signed_not : t -> t
val bitwise_not : size:int -> signed:bool -> t -> t
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.