sig
type size = Integer.t
type bit = Uninitialized | Zero | Any of Base.SetLattice.t
module Bit :
sig
type t = Abstract_memory.bit
val uninitialized : Abstract_memory.Bit.t
val zero : Abstract_memory.Bit.t
val numerical : Abstract_memory.Bit.t
val top : Abstract_memory.Bit.t
end
module type Value =
sig
type t
val name : string
val hash : Abstract_memory.Value.t -> int
val equal : Abstract_memory.Value.t -> Abstract_memory.Value.t -> bool
val compare : Abstract_memory.Value.t -> Abstract_memory.Value.t -> int
val pretty : Stdlib.Format.formatter -> Abstract_memory.Value.t -> unit
val of_bit : Abstract_memory.bit -> Abstract_memory.Value.t
val to_bit : Abstract_memory.Value.t -> Abstract_memory.bit
val is_included :
Abstract_memory.Value.t -> Abstract_memory.Value.t -> bool
val join :
Abstract_memory.Value.t ->
Abstract_memory.Value.t -> Abstract_memory.Value.t
end
module type Config = sig val deps : State.t list end
module type T =
sig
type location
type value
type t
val hash : Abstract_memory.T.t -> int
val equal : Abstract_memory.T.t -> Abstract_memory.T.t -> bool
val compare : Abstract_memory.T.t -> Abstract_memory.T.t -> int
val top : Abstract_memory.T.t
val zero : Abstract_memory.T.t
val is_top : Abstract_memory.T.t -> bool
val get :
Abstract_memory.T.t ->
Abstract_memory.T.location -> Abstract_memory.T.value
val extract :
Abstract_memory.T.t ->
Abstract_memory.T.location -> Abstract_memory.T.t
val erase :
weak:bool ->
Abstract_memory.T.t ->
Abstract_memory.T.location ->
Abstract_memory.bit -> Abstract_memory.T.t
val set :
weak:bool ->
Abstract_memory.T.t ->
Abstract_memory.T.location ->
Abstract_memory.T.value -> Abstract_memory.T.t
val overwrite :
weak:bool ->
Abstract_memory.T.t ->
Abstract_memory.T.location ->
Abstract_memory.T.t -> Abstract_memory.T.t
val reinforce :
(Abstract_memory.T.value -> Abstract_memory.T.value) ->
Abstract_memory.T.t ->
Abstract_memory.T.location -> Abstract_memory.T.t
val is_included : Abstract_memory.T.t -> Abstract_memory.T.t -> bool
val join :
Abstract_memory.T.t -> Abstract_memory.T.t -> Abstract_memory.T.t
val widen :
(size:Abstract_memory.size ->
Abstract_memory.T.value ->
Abstract_memory.T.value -> Abstract_memory.T.value) ->
Abstract_memory.T.t -> Abstract_memory.T.t -> Abstract_memory.T.t
val pretty : Stdlib.Format.formatter -> Abstract_memory.T.t -> unit
end
module Make :
functor (Config : Config) (Value : Value) ->
sig
type location = Abstract_offset.typed_offset
type value = Value.t
type t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val top : t
val zero : t
val is_top : t -> bool
val get : t -> location -> value
val extract : t -> location -> t
val erase : weak:bool -> t -> location -> bit -> t
val set : weak:bool -> t -> location -> value -> t
val overwrite : weak:bool -> t -> location -> t -> t
val reinforce : (value -> value) -> t -> location -> t
val is_included : t -> t -> bool
val join : t -> t -> t
val widen : (size:size -> value -> value -> value) -> t -> t -> t
val pretty : Format.formatter -> t -> unit
end
end