Module Datascope.InitSid.LM

module LM: Lmap_bitwise.Make_bitwise(Datascope.StmtSetLattice)

type y 
include Datatype.S
include Lattice_type.Bounded_Join_Semi_Lattice
include Lattice_type.With_Top
module LOffset: sig .. end
val empty : t
val is_empty : t -> bool
val is_bottom : t -> bool
val pretty_generic_printer : y Pretty_utils.formatter ->
string -> t Pretty_utils.formatter
val add_binding : exact:bool ->
t -> Locations.Zone.t -> y -> t
val map_and_merge : (y -> y) ->
t -> t -> t
map_and_merge f m1 m2 maps f on values in m1 and add_exact all elements of the mapped m1 to m2
val filter_base : (Base.t -> bool) -> t -> t
val find : t -> Locations.Zone.t -> y
val find_base : t -> Locations.Zone.t -> LOffset.t
exception Cannot_fold
val uninitialize : Cil_types.varinfo list -> t -> t
binds the given variables to bottom, keeps the other unchanged.
val fold : (Locations.Zone.t -> bool * y -> 'a -> 'a) ->
t -> 'a -> 'a
fold f m folds a function f on bindings in m. Each binding associates to a zone a boolean representing the possibility that the zone was not modified, and a value of type y. May raise Cannot_fold.
val fold_base : (Base.t -> LOffset.t -> 'a -> 'a) ->
t -> 'a -> 'a
val fold_fuse_same : (Locations.Zone.t -> bool * y -> 'a -> 'a) ->
t -> 'a -> 'a
Same behavior as fold, except if two disjoint ranges r1 and r2 of a given base are mapped to the same value and boolean. In this case, fold will call its argument f on r1, then on r2. fold_fuse_same will call it directly on r1 U r2, where U is the join on sets of intervals.

May raise Cannot_fold.

val map2 : ((bool * y) option ->
(bool * y) option ->
bool * y) ->
t -> t -> t
like for fold, the boolean in bool * y indicates if it is possible that the zone was not modified
val copy_paste : f:(bool * y ->
bool * y) ->
Locations.location -> Locations.location -> t -> t
This function takes a function f to be applied to each bit of the read slice. Otherwise, it has the same specification as copy_paste for Location_map.copy_paste. It may raise Bitwise_cannot_copy. Precondition : the two locations must have the same size
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.