package frama-c

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

Type of the values stored in the offsetmap

Datatype for the offsetmap

include Frama_c_kernel.Datatype.S
include Frama_c_kernel.Datatype.S_no_copy
include Frama_c_kernel.Datatype.Ty
type t
val name : string

Unique name of the datatype.

Datatype descriptor.

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 mem_project : (Frama_c_kernel.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.

Pretty-printing

val pretty_generic : ?typ:Frama_c_kernel.Cil_types.typ -> ?pretty_v:(Format.formatter -> v -> unit) -> ?skip_v:(v -> bool) -> ?sep:string -> unit -> Format.formatter -> t -> unit

Join and inclusion testing

val join : t -> t -> t
val is_included : t -> t -> bool

Finding values

val find_iset : validity:Frama_c_kernel.Base.validity -> intervals -> t -> v

Adding values

val add_binding_intervals : validity:Frama_c_kernel.Base.validity -> exact:bool -> intervals -> v -> t -> t Frama_c_kernel.Lattice_bounds.or_bottom

Creating an offsetmap

val create : size:Frama_c_kernel.Integer.t -> v -> t

size must be strictly greater than zero.

val empty : t

offsetmap containing no interval.

size_from_validity v returns the size to be used when creating a new offsetmap for a base with validity v. This is a convention that should be shared by all modules that create offsetmaps. Returns `Bottom iff v is Invalid.

  • since Aluminium-20160501

Iterators

val map : (v -> v) -> t -> t
type map2_decide =
  1. | ReturnLeft
  2. | ReturnRight
  3. | ReturnConstant of v
  4. | Recurse
    (*

    See the documentation of type Offsetmap_sig.map2_decide

    *)
val map2 : Frama_c_kernel.Hptmap_sig.cache_type -> (t -> t -> map2_decide) -> (v -> v -> v) -> t -> t -> t

See the documentation of function Offsetmap_sig.map2_on_values.

val fold : (intervals -> v -> 'a -> 'a) -> t -> 'a -> 'a
val fold_fuse_same : (intervals -> v -> 'a -> 'a) -> t -> 'a -> 'a

Same behavior as fold, except if two disjoint intervals r1 and r2 are mapped to the same value and boolean. In this case, fold will call its argument f on r1, then on r2. fold_fuse_same will call it directly on r1 U r2, where U is the join on sets of intervals.

val fold_itv : ?direction:[ `LTR | `RTL ] -> entire:bool -> (Frama_c_kernel.Int_Intervals_sig.itv -> v -> 'a -> 'a) -> Frama_c_kernel.Int_Intervals_sig.itv -> t -> 'a -> 'a

See documentation of Offsetmap_sig.fold_between.

val fold_join_itvs : cache:Frama_c_kernel.Hptmap_sig.cache_type -> (Frama_c_kernel.Integer.t -> Frama_c_kernel.Integer.t -> v -> 'a) -> ('a -> 'a -> 'a) -> 'a -> intervals -> t -> 'a

fold_join f join vempty itvs m is an implementation of fold that restricts itself to the intervals in itvs. Unlike in fold (where the equivalent of f operates on an accumulator), f returns a value on each sub-interval independently. The results are joined using joined. vempty is the value that must be returned on Int_Intervals.bottom. This function uses a cache internally. Hence, it must be partially applied to its first three arguments. If you do not need a cache, use fold instead.

Shape

val is_single_interval : t -> bool

is_single_interval o is true if the offsetmap o contains a single binding.

val single_interval_value : t -> v option

single_interval_value o returns Some v if o contains a single interval, to which v is bound, and None otherwise.

val is_same_value : t -> v -> bool

is_same_value o v is true if the offsetmap o contains a single binding to v, or is the empty offsetmap.

Misc

val clear_caches : unit -> unit

Clear the caches local to this module. Beware that they are not project-aware, and that you must call them at every project switch.

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