package frama-c

  1. Overview
  2. Docs
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

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. N
    Nicolas Bellec
  6. T
    Thibaut Benjamin
  7. A
    Allan Blanchard
  8. L
    Lionel Blatter
  9. F
    François Bobot
  10. R
    Richard Bonichon
  11. V
    Vincent Botbol
  12. Q
    Quentin Bouillaguet
  13. D
    David Bühler
  14. Z
    Zakaria Chihani
  15. L
    Loïc Correnson
  16. J
    Julien Crétin
  17. P
    Pascal Cuoq
  18. Z
    Zaynah Dargaye
  19. B
    Basile Desloges
  20. J
    Jean-Christophe Filliâtre
  21. P
    Philippe Herrmann
  22. M
    Maxime Jacquemin
  23. F
    Florent Kirchner
  24. A
    Alexander Kogtenkov
  25. R
    Remi Lazarini
  26. T
    Tristan Le Gall
  27. J
    Jean-Christophe Léchenet
  28. M
    Matthieu Lemerre
  29. D
    Dara Ly
  30. D
    David Maison
  31. C
    Claude Marché
  32. A
    André Maroneze
  33. T
    Thibault Martin
  34. F
    Fonenantsoa Maurica
  35. M
    Melody Méaulle
  36. B
    Benjamin Monate
  37. Y
    Yannick Moy
  38. P
    Pierre Nigron
  39. A
    Anne Pacalet
  40. V
    Valentin Perrelle
  41. G
    Guillaume Petiot
  42. D
    Dario Pinto
  43. V
    Virgile Prevosto
  44. A
    Armand Puccetti
  45. F
    Félix Ridoux
  46. V
    Virgile Robles
  47. J
    Jan Rochel
  48. M
    Muriel Roger
  49. J
    Julien Signoles
  50. N
    Nicolas Stouls
  51. K
    Kostyantyn Vorobyov
  52. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c.kernel/Frama_c_kernel/Lmap_bitwise/Make_bitwise/LOffset/index.html

Module Make_bitwise.LOffset

type v = v

Type of the values stored in the offsetmap

Datatype for the offsetmap

include Datatype.S
include Datatype.S_no_copy
include Datatype.Ty
type 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 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.

type intervals = Int_Intervals.t

Pretty-printing

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

Join and inclusion testing

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

Finding values

val find : Int_Intervals_sig.itv -> t -> v
val find_iset : validity:Base.validity -> intervals -> t -> v

Adding values

val add_binding_intervals : validity:Base.validity -> exact:bool -> intervals -> v -> t -> t Lattice_bounds.or_bottom
val add_binding_ival : validity:Base.validity -> exact:bool -> Ival.t -> size:Int_Base.t -> v -> t -> t Lattice_bounds.or_bottom

Creating an offsetmap

val create : size: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 : 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 -> (Int_Intervals_sig.itv -> v -> 'a -> 'a) -> Int_Intervals_sig.itv -> t -> 'a -> 'a

See documentation of Offsetmap_sig.fold_between.

val fold_join_itvs : cache:Hptmap_sig.cache_type -> (Integer.t -> 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.