Frama-C API - `Disjunction`

Parameters

module M : Abstract_memory.ProtoMemory

module S : Structure with type submemory = M.t

Signature

type t

type submemory = M.t

type structure = S.t

val pretty : Stdlib.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 : Frama_c_kernel.Cil_types.compinfo -> Abstract_memory.Bit.t -> t

val of_struct : Frama_c_kernel.Cil_types.compinfo -> structure -> t

val to_struct : oracle:Abstract_memory.oracle -> t -> structure

val weak_erase : Frama_c_kernel.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 -> Frama_c_kernel.Cil_types.fieldinfo -> 'a

val update : oracle:Abstract_memory.oracle -> (submemory -> submemory Frama_c_kernel.Lattice_bounds.or_bottom) -> t -> Frama_c_kernel.Cil_types.fieldinfo -> t Frama_c_kernel.Lattice_bounds.or_bottom

val map : (submemory -> submemory) -> t -> t

Frama-C API - Disjunction

Parameters

Signature

Frama-C API - `Disjunction`