sig
val configure : unit -> Wp.WpContext.rollback
val datatype : string
module State : State
type t
type state = Wp.MemVal.State.t
val null : Wp.MemVal.Value.t
val literal : eid:int -> Wp.Cstring.cst -> int * Wp.MemVal.Value.t
val cvar : Cil_types.varinfo -> Wp.MemVal.Value.t
val field : Wp.MemVal.Value.t -> Cil_types.fieldinfo -> Wp.MemVal.Value.t
val shift :
Wp.MemVal.Value.t ->
Wp.Ctypes.c_object -> Wp.Lang.F.term -> Wp.MemVal.Value.t
val base_addr : Wp.MemVal.Value.t -> Wp.MemVal.Value.t
val load :
Wp.MemVal.Value.state ->
Wp.MemVal.Value.t -> Wp.Ctypes.c_object -> Wp.MemVal.Value.t
val domain : Wp.MemVal.Value.t -> Base.t list
val offset : Wp.MemVal.Value.t -> Wp.Lang.F.term -> Wp.Lang.F.pred
val pretty : Stdlib.Format.formatter -> Wp.MemVal.Value.t -> unit
end