Module `MemBytes.Sigma`Source

Sourcetype chunk = Chunk.t

Sourcemodule Chunk : sig ... end

Sourcetype domain = Chunk.Set.t

Sourcetype t

Sourceval pretty : Stdlib.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

val 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

Install