module Eva:Value
The glue between WP and EVA. *
val configure : unit -> WpContext.rollback
val datatype : string
module State:MemVal.State
type
t
abstract value *
typestate =
MemVal.State.t
val null : 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 literal : eid:int -> Cstring.cst -> int * t
cvar x
returns the abstract value corresponding to &x
. *
val cvar : Cil_types.varinfo -> t
val field : t -> Cil_types.fieldinfo -> t
field v fd
returns the value obtained by access to field fd
from v
. *
shift v obj k
returns the value obtained by access at an index k
with type obj
from v
. *
val shift : t -> Ctypes.c_object -> Lang.F.term -> t
base_addr v
returns the value corresponding to the base address
of v
. *
val base_addr : t -> t
val load : state -> t -> 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
. *
offset v
returns a function which when applied with a term returns
a predicate over v
's offset.
val offset : t -> Lang.F.term -> Lang.F.pred
val pretty : Stdlib.Format.formatter -> t -> unit