package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Pretty-printing
Join and inclusion testing
Finding values
Adding values
Creating an offsetmap
Iterators
Shape
Misc

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-eva.core/Eva/Assigns/Memory/LOffset/index.html

Module `Memory.LOffset`

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val ty : t Frama_c_kernel.Type.t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val name : string

Unique name of the datatype.

val descr : t Frama_c_kernel.Descr.t

Datatype descriptor.

val packed_descr : Frama_c_kernel.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.(=).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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.

type intervals = Frama_c_kernel.Int_Intervals.t

Pretty-printing

val pretty : t Frama_c_kernel.Pretty_utils.formatter

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

val pretty_debug : t Frama_c_kernel.Pretty_utils.formatter

Join and inclusion testing

val join : t -> t -> t

val is_included : t -> t -> bool

Finding values

val find : Frama_c_kernel.Int_Intervals_sig.itv -> t -> v

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

val add_binding_ival : 
  validity:Frama_c_kernel.Base.validity ->
  exact:bool ->
  Frama_c_kernel.Ival.t ->
  size:Frama_c_kernel.Int_Base.t ->
  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.

val size_from_validity : 
  Frama_c_kernel.Base.validity ->
  Frama_c_kernel.Integer.t Frama_c_kernel.Lattice_bounds.or_bottom

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 =

| ReturnLeft
| ReturnRight
| ReturnConstant of v
| 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.