module type Value =sig
..end
val configure : unit -> Wp.WpContext.rollback
val datatype : string
module State:Wp.MemVal.State
type
t
abstract value *
typestate =
Wp.MemVal.State.t
val null : t
val literal : eid:int -> Wp.Cstring.cst -> int * t
literal eid cstr
returns the pair of base identifier and abstract value
corresponding to the concrete string constant cstr
of unique expression
identifier eid
. eid
should be a valid identifier for cstr
. *
val cvar : Cil_types.varinfo -> t
cvar x
returns the abstract value corresponding to &x
. *
val field : t -> Cil_types.fieldinfo -> t
field v fd
returns the value obtained by access to field fd
from v
. *
val shift : t ->
Wp.Ctypes.c_object -> Wp.Lang.F.term -> t
shift v obj k
returns the value obtained by access at an index k
with type obj
from v
. *
val base_addr : t -> t
base_addr v
returns the value corresponding to the base address
of v
. *
val load : state ->
t -> Wp.Ctypes.c_object -> t
load s v obj
returns the value at the location given by v
with type
obj
within the state s
. *
val domain : t -> Base.t list
domain v
returns a list of all possible concrete bases of v
. *
val offset : t -> Wp.Lang.F.term -> Wp.Lang.F.pred
offset v
returns a function which when applied with a term returns
a predicate over v
's offset.
val pretty : Stdlib.Format.formatter -> t -> unit