Frama-C:
Plug-ins:
Libraries:

Frama-C API - M

type t
type value
val pretty : Stdlib.Format.formatter -> t -> unit
val pretty_root : Stdlib.Format.formatter -> t -> unit
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val of_raw : Abstract_memory.bit -> t
val raw : t -> Abstract_memory.bit
val of_value : Frama_c_kernel.Cil_types.typ -> value -> t
val to_value : Frama_c_kernel.Cil_types.typ -> t -> value
val to_singleton_int : t -> Frama_c_kernel.Z.t option
val weak_erase : Abstract_memory.bit -> t -> t
val is_included : t -> t -> bool
val unify : oracle:Abstract_memory.bioracle -> (size:Abstract_memory.size -> value -> value -> value) -> t -> t -> t
val join : oracle:Abstract_memory.bioracle -> t -> t -> t
val smash : oracle:Abstract_memory.oracle -> t -> t -> t
val read : oracle:Abstract_memory.oracle -> (Frama_c_kernel.Cil_types.typ -> t -> 'a) -> ('a -> 'a -> 'a) -> Abstract_offset.t -> t -> 'a
val add_segmentation_bounds : oracle:Abstract_memory.oracle -> typ:Frama_c_kernel.Cil_types.typ -> Eva_ast.exp list -> t -> t