Frama-C API - Segmentation
type bound = Bound.tval pretty : Stdlib.Format.formatter -> t -> unitval hash : t -> intval hull : oracle:Abstract_memory.oracle -> t -> (bound * bound) Frama_c_kernel.Lattice_bounds.or_topval raw : t -> Abstract_memory.Bit.tval weak_erase : Abstract_memory.Bit.t -> t -> tval unify : oracle:Abstract_memory.bioracle -> (submemory -> submemory -> submemory) -> t -> t -> t Frama_c_kernel.Lattice_bounds.or_topval single : Abstract_memory.bit -> bound -> bound -> submemory -> tval read : oracle:Abstract_memory.oracle -> (submemory -> 'a) -> ('a -> 'a -> 'a) -> t -> bound -> bound -> 'aval update : oracle:Abstract_memory.oracle -> (submemory -> submemory Frama_c_kernel.Lattice_bounds.or_bottom) -> t -> bound -> bound -> t Frama_c_kernel.Lattice_bounds.or_top_bottomval incr_bound : oracle:Abstract_memory.oracle -> Frama_c_kernel.Cil_types.varinfo -> Frama_c_kernel.Z.t option -> t -> t Frama_c_kernel.Lattice_bounds.or_topval fold : (submemory -> 'a -> 'a) -> (Abstract_memory.bit -> 'b -> 'a) -> t -> 'b -> 'aval add_segmentation_bounds : oracle:Abstract_memory.oracle -> bound list -> t -> t