package frama-c

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

Association between bases and offsets in byte.

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

    *)
type size_widen_hint = Ival.size_widen_hint
type numerical_widen_hint = Base.t -> Ival.numerical_widen_hint

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
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_Widening with type t := t 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
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
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.

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 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 : Origin.t -> 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 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_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 -> 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct