package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/mthread/Mthread/Mt_shared_vars/Precise/ZoneMap/index.html

Module `Precise.ZoneMap`Source

type v = Set.t

type map

type lmap =

| Top
| Map of map
| Bottom

include Frama_c_kernel.Datatype.S with type t = lmap

include Frama_c_kernel.Datatype.S_no_copy with type t = lmap

include Frama_c_kernel.Datatype.Ty with type t = lmap

type t = lmap

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

include Frama_c_kernel.Lattice_type.Bounded_Join_Semi_Lattice with type t := t

include Frama_c_kernel.Lattice_type.Join_Semi_Lattice with type t := t

datatype of element of the lattice

include Frama_c_kernel.Datatype.S with type t := t

include Frama_c_kernel.Datatype.S_no_copy with type t := t

include Frama_c_kernel.Datatype.Ty with type t := t

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.

Sourceval pretty : Stdlib.Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

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

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.

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

val top : t

largest element

module LOffset : 
  Frama_c_kernel.Offsetmap_bitwise_sig.S
    with type v = v
     and type intervals = Frama_c_kernel.Int_Intervals.t

val is_empty : t -> bool

val is_bottom : t -> bool

val empty : t

val empty_map : map

val pretty_generic_printer : 
  ?pretty_v:v Frama_c_kernel.Pretty_utils.formatter ->
  ?skip_v:(v -> bool) ->
  sep:string ->
  unit ->
  t Frama_c_kernel.Pretty_utils.formatter

val pretty_debug : t Frama_c_kernel.Pretty_utils.formatter

val add_binding : exact:bool -> t -> Frama_c_kernel.Locations.Zone.t -> v -> t

val add_binding_loc : 
  exact:bool ->
  t ->
  Frama_c_kernel.Locations.location ->
  v ->
  t

val add_base : Frama_c_kernel.Base.t -> LOffset.t -> t -> t

val remove_base : Frama_c_kernel.Base.t -> t -> t

val find : 
  t ->
  Frama_c_kernel.Locations.Zone.t ->
  v Frama_c_kernel.Lattice_bounds.or_bottom

val filter_base : (Frama_c_kernel.Base.t -> bool) -> t -> t

Iterators

val map : (v -> v) -> t -> t

val fold : 
  (Frama_c_kernel.Locations.Zone.t -> v -> 'a -> 'a) ->
  map ->
  'a ->
  'a

The following fold_* functions, as well as map2 take arguments of type map to force their user to handle the cases Top and Bottom explicitly.

fold f m folds a function f on the bindings in m. Contiguous bits with the same value are merged into a single zone. Different bases are presented in different zones.

val fold_base : 
  (Frama_c_kernel.Base.t -> LOffset.t -> 'a -> 'a) ->
  map ->
  'a ->
  'a

val fold_fuse_same : 
  (Frama_c_kernel.Locations.Zone.t -> v -> 'a -> 'a) ->
  map ->
  'a ->
  'a

Same behavior as fold, except if two non-contiguous ranges r1 and r2 of a given base are mapped to the same value. fold will call its argument f on each range successively (hence, in our example, on r1 and r2 separately). Conversely, fold_fuse_same will call f directly on r1 U r2, U being the join on sets of intervals.

val fold_join_zone : 
  both:(Frama_c_kernel.Int_Intervals.t -> LOffset.t -> 'a) ->
  conv:(Frama_c_kernel.Base.t -> 'a -> 'b) ->
  empty_map:(Frama_c_kernel.Locations.Zone.t -> 'b) ->
  join:('b -> 'b -> 'b) ->
  empty:'b ->
  Frama_c_kernel.Locations.Zone.t ->
  map ->
  'b

fold_join_zone ~both ~conv ~empty_map ~join ~empty z m folds over the intervals present in z. When a base b is present in both z and m, and bound respectively to itvs and mb, both itvs mb is called. The results obtained for this base b are then converted using conv. If a sub-zone z' is present in z, but the corresponding bases are not bound in m, empty_map z' is called. All the sub-results (of type) 'b are joined using join. empty is used when an empty map or sub-zone is encountered. It must be a neutral element for join.

This function internally uses a cache, and must be partially applied to its named arguments. (This explains the somewhat contrived interface, in particular the fact that both and conv are not fused.)

val map2 : 
  cache:Frama_c_kernel.Hptmap_sig.cache_type ->
  symmetric:bool ->
  idempotent:bool ->
  empty_neutral:bool ->
  (LOffset.t -> LOffset.t -> LOffset.map2_decide) ->
  (v -> v -> v) ->
  map ->
  map ->
  map

'map'-like function between two interval maps, implemented as a simultaneous descent in both maps. map2 ~cache ~symmetric ~idempotent ~empty_neutral decide_fast f m1 m2 computes the map containing k |-> f v_1 v_2 for all the keys k present in either m1 or m2. When a key is present, v_i is the corresponding value in the map. When it is missing in one of the maps, a default value is generated. (See argument default to functor Make_bitwise below.)

symmetric, idempotent, empty_neutral and decide_fast are present for optimisation purposes, to avoid visiting some trees. If symmetric holds, f v1 v2 = f v2 v1 must also holds. If idempotent holds, f v v = v must also holds. Similarly, if empty_neutral holds, f v default = f default v = v must hold. decide_fast is called before visiting two subtrees, and can be used to stop the recursion early. See the documentation of Offsetmap_sig.map2_decide.

Depending on the value of cache, the results of this function will be cached.

Misc

val shape : 
  map ->
  LOffset.t Frama_c_kernel.Hptmap.Shape(Frama_c_kernel.Base.Base).t

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.

On This Page

Iterators
Misc