package frama-c

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