sig
type initialization = SurelyInitialized | MaybeUninitialized
type bit =
Uninitialized
| Zero of Abstract_memory.initialization
| Any of Base.SetLattice.t * Abstract_memory.initialization
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
val is_any : Abstract_memory.Bit.t -> bool
val initialization :
Abstract_memory.Bit.t -> Abstract_memory.initialization
val pretty : Stdlib.Format.formatter -> Abstract_memory.Bit.t -> unit
val hash : Abstract_memory.Bit.t -> int
val equal : Abstract_memory.Bit.t -> Abstract_memory.Bit.t -> bool
val compare : Abstract_memory.Bit.t -> Abstract_memory.Bit.t -> int
val is_included :
Abstract_memory.Bit.t -> Abstract_memory.Bit.t -> bool
val join :
Abstract_memory.Bit.t ->
Abstract_memory.Bit.t -> Abstract_memory.Bit.t
end
type size = Integer.t
type side = Left | Right
type oracle = Cil_types.exp -> Int_val.t
type bioracle = Abstract_memory.side -> Abstract_memory.oracle
module type ProtoMemory =
sig
type t
type value
val pretty :
Stdlib.Format.formatter -> Abstract_memory.ProtoMemory.t -> unit
val pretty_root :
Stdlib.Format.formatter -> Abstract_memory.ProtoMemory.t -> unit
val hash : Abstract_memory.ProtoMemory.t -> int
val equal :
Abstract_memory.ProtoMemory.t ->
Abstract_memory.ProtoMemory.t -> bool
val compare :
Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t -> int
val of_raw : Abstract_memory.bit -> Abstract_memory.ProtoMemory.t
val raw : Abstract_memory.ProtoMemory.t -> Abstract_memory.bit
val of_value :
Cil_types.typ ->
Abstract_memory.ProtoMemory.value -> Abstract_memory.ProtoMemory.t
val to_value :
Cil_types.typ ->
Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.value
val to_singleton_int :
Abstract_memory.ProtoMemory.t -> Integer.t option
val weak_erase :
Abstract_memory.bit ->
Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t
val is_included :
Abstract_memory.ProtoMemory.t ->
Abstract_memory.ProtoMemory.t -> bool
val unify :
oracle:Abstract_memory.bioracle ->
(size:Abstract_memory.size ->
Abstract_memory.ProtoMemory.value ->
Abstract_memory.ProtoMemory.value ->
Abstract_memory.ProtoMemory.value) ->
Abstract_memory.ProtoMemory.t ->
Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t
val join :
oracle:Abstract_memory.bioracle ->
Abstract_memory.ProtoMemory.t ->
Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t
val smash :
oracle:Abstract_memory.oracle ->
Abstract_memory.ProtoMemory.t ->
Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t
val read :
oracle:Abstract_memory.oracle ->
(Cil_types.typ -> Abstract_memory.ProtoMemory.t -> 'a) ->
('a -> 'a -> 'a) ->
Abstract_offset.t -> Abstract_memory.ProtoMemory.t -> 'a
val update :
oracle:Abstract_memory.oracle ->
(weak:bool ->
Cil_types.typ ->
Abstract_memory.ProtoMemory.t ->
Abstract_memory.ProtoMemory.t Lattice_bounds.or_bottom) ->
weak:bool ->
Abstract_offset.t ->
Abstract_memory.ProtoMemory.t ->
Abstract_memory.ProtoMemory.t Lattice_bounds.or_bottom
val incr_bound :
oracle:Abstract_memory.oracle ->
Cil_types.varinfo ->
Integer.t option ->
Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t
val add_segmentation_bounds :
oracle:Abstract_memory.oracle ->
typ:Cil_types.typ ->
Cil_types.exp list ->
Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t
end
end