Frama-C API - Eva
The glue between WP and EVA. *
val configure : unit -> WpContext.rollback
type state = State.t
val null : t
val literal : eid:int -> 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 : Frama_c_kernel.Cil_types.varinfo -> t
cvar x
returns the abstract value corresponding to &x
. *
val field : t -> Frama_c_kernel.Cil_types.fieldinfo -> t
field v fd
returns the value obtained by access to field fd
from v
. *
val shift : t -> Ctypes.c_object -> Lang.F.term -> t
shift v obj k
returns the value obtained by access at an index k
with type obj
from v
. *
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 -> Frama_c_kernel.Base.t list
domain v
returns a list of all possible concrete bases of v
. *
val offset : t -> Lang.F.term -> 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