package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
include Lmap_bitwise.Location_map_bitwise with type v = DepsOrUnassigned.t
type map
type lmap =
  1. | Top
  2. | Map of map
  3. | 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
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
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 pretty : Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

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

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

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