Module MemBytes.SigmaSource

Sourcetype chunk = Chunk.t
Sourcemodule Chunk : sig ... end
Sourcetype domain = Chunk.Set.t
Sourcetype t
Sourceval pretty : Format.formatter -> t -> unit
Sourceval create : unit -> t
Sourceval mem : t -> chunk -> bool
Sourceval get : t -> chunk -> Lang.F.var
Sourceval value : t -> chunk -> Lang.F.term
Sourceval copy : t -> t
Sourceval join : t -> t -> Passive.t
Sourceval assigned : pre:t -> post:t -> domain -> Lang.F.pred Frama_c_kernel.Bag.t
Sourceval choose : t -> t -> t
Sourceval merge : t -> t -> t * Passive.t * Passive.t
Sourceval merge_list : t list -> t * Passive.t list
Sourceval iter : (chunk -> Lang.F.var -> unit) -> t -> unit
Sourceval iter2 : (chunk -> Lang.F.var option -> Lang.F.var option -> unit) -> t -> t -> unit
Sourceval havoc_chunk : t -> chunk -> t
Sourceval havoc : t -> domain -> t
Sourceval havoc_any : call:bool -> t -> t
Sourceval remove_chunks : t -> domain -> t
Sourceval domain : t -> domain
Sourceval union : domain -> domain -> domain
Sourceval empty : domain
Sourceval writes : t Wp__Sigs.sequence -> domain