sig
module type Config = sig val slice_limit : unit -> int end
module Bound :
sig
type t
exception UnsupportedBoundExpression
val of_exp : Cil_types.exp -> Segmentation.Bound.t
val of_integer : Integer.t -> Segmentation.Bound.t
val succ : Segmentation.Bound.t -> Segmentation.Bound.t
end
module type Segmentation =
sig
type bound = Segmentation.Bound.t
type submemory
type t
val pretty :
Stdlib.Format.formatter -> Segmentation.Segmentation.t -> unit
val hash : Segmentation.Segmentation.t -> int
val equal :
Segmentation.Segmentation.t -> Segmentation.Segmentation.t -> bool
val compare :
Segmentation.Segmentation.t -> Segmentation.Segmentation.t -> int
val hull :
oracle:Abstract_memory.oracle ->
Segmentation.Segmentation.t ->
(Segmentation.Segmentation.bound * Segmentation.Segmentation.bound)
Lattice_bounds.or_top
val raw : Segmentation.Segmentation.t -> Abstract_memory.Bit.t
val weak_erase :
Abstract_memory.Bit.t ->
Segmentation.Segmentation.t -> Segmentation.Segmentation.t
val is_included :
Segmentation.Segmentation.t -> Segmentation.Segmentation.t -> bool
val unify :
oracle:Abstract_memory.bioracle ->
(Segmentation.Segmentation.submemory ->
Segmentation.Segmentation.submemory ->
Segmentation.Segmentation.submemory) ->
Segmentation.Segmentation.t ->
Segmentation.Segmentation.t ->
Segmentation.Segmentation.t Lattice_bounds.or_top
val single :
Abstract_memory.bit ->
Segmentation.Segmentation.bound ->
Segmentation.Segmentation.bound ->
Segmentation.Segmentation.submemory -> Segmentation.Segmentation.t
val read :
oracle:Abstract_memory.oracle ->
(Segmentation.Segmentation.submemory -> 'a) ->
('a -> 'a -> 'a) ->
Segmentation.Segmentation.t ->
Segmentation.Segmentation.bound ->
Segmentation.Segmentation.bound -> 'a
val update :
oracle:Abstract_memory.oracle ->
(Segmentation.Segmentation.submemory ->
Segmentation.Segmentation.submemory Lattice_bounds.or_bottom) ->
Segmentation.Segmentation.t ->
Segmentation.Segmentation.bound ->
Segmentation.Segmentation.bound ->
Segmentation.Segmentation.t Lattice_bounds.or_top_bottom
val incr_bound :
oracle:Abstract_memory.oracle ->
Cil_types.varinfo ->
Integer.t option ->
Segmentation.Segmentation.t ->
Segmentation.Segmentation.t Lattice_bounds.or_top
val map :
(Segmentation.Segmentation.submemory ->
Segmentation.Segmentation.submemory) ->
Segmentation.Segmentation.t -> Segmentation.Segmentation.t
val fold :
(Segmentation.Segmentation.submemory -> 'a -> 'a) ->
(Abstract_memory.bit -> 'b -> 'a) ->
Segmentation.Segmentation.t -> 'b -> 'a
val add_segmentation_bounds :
oracle:Abstract_memory.oracle ->
Segmentation.Segmentation.bound list ->
Segmentation.Segmentation.t -> Segmentation.Segmentation.t
end
module Make :
functor (Config : Config) (M : Abstract_memory.ProtoMemory) ->
sig
type bound = Bound.t
type submemory = M.t
type t
val pretty : Format.formatter -> t -> unit
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val hull :
oracle:Abstract_memory.oracle ->
t -> (bound * bound) Lattice_bounds.or_top
val raw : t -> Abstract_memory.Bit.t
val weak_erase : Abstract_memory.Bit.t -> t -> t
val is_included : t -> t -> bool
val unify :
oracle:Abstract_memory.bioracle ->
(submemory -> submemory -> submemory) ->
t -> t -> t Lattice_bounds.or_top
val single : Abstract_memory.bit -> bound -> bound -> submemory -> t
val read :
oracle:Abstract_memory.oracle ->
(submemory -> 'a) -> ('a -> 'a -> 'a) -> t -> bound -> bound -> 'a
val update :
oracle:Abstract_memory.oracle ->
(submemory -> submemory Lattice_bounds.or_bottom) ->
t -> bound -> bound -> t Lattice_bounds.or_top_bottom
val incr_bound :
oracle:Abstract_memory.oracle ->
Cil_types.varinfo ->
Integer.t option -> t -> t Lattice_bounds.or_top
val map : (submemory -> submemory) -> t -> t
val fold :
(submemory -> 'a -> 'a) ->
(Abstract_memory.bit -> 'b -> 'a) -> t -> 'b -> 'a
val add_segmentation_bounds :
oracle:Abstract_memory.oracle -> bound list -> t -> t
end
end