sig
module type Config = sig val deps : State.t list end
module type Structure =
sig
type t
type submemory
val pretty :
Stdlib.Format.formatter -> Abstract_structure.Structure.t -> unit
val hash : Abstract_structure.Structure.t -> int
val equal :
Abstract_structure.Structure.t ->
Abstract_structure.Structure.t -> bool
val compare :
Abstract_structure.Structure.t ->
Abstract_structure.Structure.t -> int
val raw : Abstract_structure.Structure.t -> Abstract_memory.Bit.t
val of_raw : Abstract_memory.Bit.t -> Abstract_structure.Structure.t
val weak_erase :
Abstract_memory.Bit.t ->
Abstract_structure.Structure.t -> Abstract_structure.Structure.t
val is_included :
Abstract_structure.Structure.t ->
Abstract_structure.Structure.t -> bool
val unify :
(Abstract_structure.Structure.submemory ->
Abstract_structure.Structure.submemory ->
Abstract_structure.Structure.submemory) ->
Abstract_structure.Structure.t ->
Abstract_structure.Structure.t -> Abstract_structure.Structure.t
val read :
Abstract_structure.Structure.t ->
Cil_types.fieldinfo -> Abstract_structure.Structure.submemory
val update :
(Abstract_structure.Structure.submemory ->
Abstract_structure.Structure.submemory Lattice_bounds.or_bottom) ->
Abstract_structure.Structure.t ->
Cil_types.fieldinfo ->
Abstract_structure.Structure.t Lattice_bounds.or_bottom
val map :
(Abstract_structure.Structure.submemory ->
Abstract_structure.Structure.submemory) ->
Abstract_structure.Structure.t -> Abstract_structure.Structure.t
end
module Make :
functor (Config : Config) (M : Abstract_memory.ProtoMemory) ->
sig
type t
type submemory = M.t
val pretty : Format.formatter -> t -> unit
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val raw : t -> Abstract_memory.Bit.t
val of_raw : Abstract_memory.Bit.t -> t
val weak_erase : Abstract_memory.Bit.t -> t -> t
val is_included : t -> t -> bool
val unify : (submemory -> submemory -> submemory) -> t -> t -> t
val read : t -> Cil_types.fieldinfo -> submemory
val update :
(submemory -> submemory Lattice_bounds.or_bottom) ->
t -> Cil_types.fieldinfo -> t Lattice_bounds.or_bottom
val map : (submemory -> submemory) -> t -> t
end
module type Disjunction =
sig
type t
type submemory
type structure
val pretty :
Stdlib.Format.formatter -> Abstract_structure.Disjunction.t -> unit
val hash : Abstract_structure.Disjunction.t -> int
val equal :
Abstract_structure.Disjunction.t ->
Abstract_structure.Disjunction.t -> bool
val compare :
Abstract_structure.Disjunction.t ->
Abstract_structure.Disjunction.t -> int
val raw : Abstract_structure.Disjunction.t -> Abstract_memory.Bit.t
val of_raw :
Cil_types.compinfo ->
Abstract_memory.Bit.t -> Abstract_structure.Disjunction.t
val of_struct :
Cil_types.compinfo ->
Abstract_structure.Disjunction.structure ->
Abstract_structure.Disjunction.t
val to_struct :
oracle:Abstract_memory.oracle ->
Abstract_structure.Disjunction.t ->
Abstract_structure.Disjunction.structure
val weak_erase :
Cil_types.compinfo ->
Abstract_memory.Bit.t ->
Abstract_structure.Disjunction.t -> Abstract_structure.Disjunction.t
val is_included :
Abstract_structure.Disjunction.t ->
Abstract_structure.Disjunction.t -> bool
val unify :
oracle:Abstract_memory.bioracle ->
(Abstract_structure.Disjunction.submemory ->
Abstract_structure.Disjunction.submemory ->
Abstract_structure.Disjunction.submemory) ->
Abstract_structure.Disjunction.t ->
Abstract_structure.Disjunction.t -> Abstract_structure.Disjunction.t
val read :
(Abstract_structure.Disjunction.submemory -> 'a) ->
('a -> 'a -> 'a) ->
Abstract_structure.Disjunction.t -> Cil_types.fieldinfo -> 'a
val update :
oracle:Abstract_memory.oracle ->
(Abstract_structure.Disjunction.submemory ->
Abstract_structure.Disjunction.submemory Lattice_bounds.or_bottom) ->
Abstract_structure.Disjunction.t ->
Cil_types.fieldinfo ->
Abstract_structure.Disjunction.t Lattice_bounds.or_bottom
val map :
(Abstract_structure.Disjunction.submemory ->
Abstract_structure.Disjunction.submemory) ->
Abstract_structure.Disjunction.t -> Abstract_structure.Disjunction.t
end
module Disjunction :
functor (M : Abstract_memory.ProtoMemory)
(S : sig
type t
type submemory = M.t
val pretty : Format.formatter -> t -> unit
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val raw : t -> Abstract_memory.Bit.t
val of_raw : Abstract_memory.Bit.t -> t
val weak_erase : Abstract_memory.Bit.t -> t -> t
val is_included : t -> t -> bool
val unify : (submemory -> submemory -> submemory) -> t -> t -> t
val read : t -> Cil_types.fieldinfo -> submemory
val update :
(submemory -> submemory Lattice_bounds.or_bottom) ->
t -> Cil_types.fieldinfo -> t Lattice_bounds.or_bottom
val map : (submemory -> submemory) -> t -> t
end)
->
sig
type t
type submemory = M.t
type structure = S.t
val pretty : Format.formatter -> t -> unit
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val raw : t -> Abstract_memory.Bit.t
val of_raw : Cil_types.compinfo -> Abstract_memory.Bit.t -> t
val of_struct : Cil_types.compinfo -> structure -> t
val to_struct : oracle:Abstract_memory.oracle -> t -> structure
val weak_erase :
Cil_types.compinfo -> Abstract_memory.Bit.t -> t -> t
val is_included : t -> t -> bool
val unify :
oracle:Abstract_memory.bioracle ->
(submemory -> submemory -> submemory) -> t -> t -> t
val read :
(submemory -> 'a) ->
('a -> 'a -> 'a) -> t -> Cil_types.fieldinfo -> 'a
val update :
oracle:Abstract_memory.oracle ->
(submemory -> submemory Lattice_bounds.or_bottom) ->
t -> Cil_types.fieldinfo -> t Lattice_bounds.or_bottom
val map : (submemory -> submemory) -> t -> t
end
end