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-project

Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.0-Nickel.tar.gz

sha256=29612882330ecb6eddd0b4ca3afc0492b70d0feb3379a1b8e893194c6e173983

doc/frama-c.kernel/Frama_c_kernel/Function_Froms/Memory/index.html

Module `Function_Froms.Memory`

include Lmap_bitwise.Location_map_bitwise with type v = DepsOrUnassigned.t

type v = DepsOrUnassigned.t

type map

type lmap =

| Top
| Map of map
| Bottom

include Datatype.S with type t = lmap

include Datatype.S_no_copy with type t = lmap

include Datatype.Ty with type t = lmap

type t = lmap

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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 ty : t Type.t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.(=).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val pretty : 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
Plug-in Development Guide

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.

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

module LOffset : 
  Offsetmap_bitwise_sig.S with type v = v and type intervals = 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 Pretty_utils.formatter ->
  ?skip_v:(v -> bool) ->
  sep:string ->
  unit ->
  t Pretty_utils.formatter

val pretty_debug : t Pretty_utils.formatter

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

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

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

Iterators

val fold : (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 : (Base.t -> LOffset.t -> 'a -> 'a) -> map -> 'a -> 'a

val fold_fuse_same : (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:(Int_Intervals.t -> LOffset.t -> 'a) ->
  conv:(Base.t -> 'a -> 'b) ->
  empty_map:(Locations.Zone.t -> 'b) ->
  join:('b -> 'b -> 'b) ->
  empty:'b ->
  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: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 Hptmap.Shape(Base.Base).t

val imprecise_write_msg : string ref

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.

val pretty_ind_data : Format.formatter -> t -> unit

Prints the detail of address and data dependencies, as opposed to pretty that prints the backwards-compatible union of them

val find : t -> Locations.Zone.t -> Locations.Zone.t

Imprecise version of find, in which data and indirect dependencies are not distinguished

val find_precise : t -> Locations.Zone.t -> Deps.t

Precise version of find

val add_binding : exact:bool -> t -> Locations.Zone.t -> Deps.t -> t

val add_binding_loc : exact:bool -> t -> Locations.location -> Deps.t -> t

val add_binding_precise_loc : 
  exact:bool ->
  Locations.access ->
  t ->
  Precise_locs.precise_location ->
  Deps.t ->
  t

val bind_var : Cil_types.varinfo -> Deps.t -> t -> t

val unbind_var : Cil_types.varinfo -> t -> t

val map : (DepsOrUnassigned.t -> DepsOrUnassigned.t) -> t -> t

val compose : t -> t -> t

Sequential composition. See DepsOrUnassigned.compose.

val substitute : t -> Deps.t -> Deps.t

substitute m d applies m to d so that any dependency in d is expressed using the dependencies already present in m. For example, substitute 'x From y' 'x' returns 'y'.

Dependencies for \result.

type return = Deps.t

val default_return : return

Default value to use for storing the dependencies of \result

val top_return : return

Completely imprecise return

val top_return_size : Int_Base.t -> return

Completely imprecise return of the given size

val add_to_return : 
  ?start:int ->
  size:Int_Base.t ->
  ?m:return ->
  Deps.t ->
  return

Add some dependencies to \result, between bits start and start+size-1, to the Deps.t value; default value for start is 0. If m is specified, the dependencies are added to it. Otherwise, default_return is used.

val collapse_return : return -> Deps.t