sig
val are_typ_compatible : Cil_types.typ -> Cil_types.typ -> bool
module type Config =
sig
val deps : State.t list
val slice_limit : unit -> int
val disjunctive_invariants : unit -> bool
end
module type Value =
sig
type t
val name : string
val hash : Typed_memory.Value.t -> int
val equal : Typed_memory.Value.t -> Typed_memory.Value.t -> bool
val compare : Typed_memory.Value.t -> Typed_memory.Value.t -> int
val pretty : Stdlib.Format.formatter -> Typed_memory.Value.t -> unit
val of_bit :
typ:Cil_types.typ -> Abstract_memory.bit -> Typed_memory.Value.t
val to_bit : Typed_memory.Value.t -> Abstract_memory.bit
val to_integer : Typed_memory.Value.t -> Integer.t option
val is_included : Typed_memory.Value.t -> Typed_memory.Value.t -> bool
val join :
Typed_memory.Value.t -> Typed_memory.Value.t -> Typed_memory.Value.t
end
module Make :
functor (Config : Config) (Value : Value) ->
sig
type location = Abstract_offset.t
type value = Typed_memory.Value.t
type t
val hash : Typed_memory.Make.t -> int
val equal : Typed_memory.Make.t -> Typed_memory.Make.t -> bool
val compare : Typed_memory.Make.t -> Typed_memory.Make.t -> int
val top : Typed_memory.Make.t
val zero : Typed_memory.Make.t
val is_top : Typed_memory.Make.t -> bool
val get :
oracle:Abstract_memory.oracle ->
Typed_memory.Make.t ->
Typed_memory.Make.location -> Typed_memory.Make.value
val extract :
oracle:Abstract_memory.oracle ->
Typed_memory.Make.t ->
Typed_memory.Make.location -> Typed_memory.Make.t
val erase :
oracle:Abstract_memory.oracle ->
weak:bool ->
Typed_memory.Make.t ->
Typed_memory.Make.location ->
Abstract_memory.bit -> Typed_memory.Make.t
val set :
oracle:Abstract_memory.oracle ->
weak:bool ->
Typed_memory.Make.t ->
Typed_memory.Make.location ->
Typed_memory.Make.value -> Typed_memory.Make.t
val overwrite :
oracle:Abstract_memory.oracle ->
weak:bool ->
Typed_memory.Make.t ->
Typed_memory.Make.location ->
Typed_memory.Make.t -> Typed_memory.Make.t
val reinforce :
oracle:Abstract_memory.oracle ->
(Typed_memory.Make.value ->
Typed_memory.Make.value Lattice_bounds.or_bottom) ->
Typed_memory.Make.t ->
Typed_memory.Make.location ->
Typed_memory.Make.t Lattice_bounds.or_bottom
val is_included : Typed_memory.Make.t -> Typed_memory.Make.t -> bool
val join :
oracle:Abstract_memory.bioracle ->
Typed_memory.Make.t -> Typed_memory.Make.t -> Typed_memory.Make.t
val widen :
oracle:Abstract_memory.bioracle ->
(size:Abstract_memory.size ->
Typed_memory.Make.value ->
Typed_memory.Make.value -> Typed_memory.Make.value) ->
Typed_memory.Make.t -> Typed_memory.Make.t -> Typed_memory.Make.t
val incr_bound :
oracle:Abstract_memory.oracle ->
Cil_types.varinfo ->
Integer.t option -> Typed_memory.Make.t -> Typed_memory.Make.t
val pretty : Stdlib.Format.formatter -> Typed_memory.Make.t -> unit
val segmentation_hint :
oracle:Abstract_memory.oracle ->
Typed_memory.Make.t ->
Typed_memory.Make.location ->
Cil_types.exp list -> Typed_memory.Make.t
end
end