Frama-C:
Plug-ins:
Libraries:

Frama-C API - LocInfo

type map
type lmap =
  1. | Top
  2. | Map of map
  3. | 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
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 name : string

Unique name of the datatype.

Datatype descriptor.

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 : Stdlib.Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

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

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