Module Wp.MemVal.Eva

module Eva: Value

The glue between WP and EVA. *

val configure : unit -> Wp.WpContext.rollback

val datatype : string

module State: Wp.MemVal.State

type t

abstract value *

type state = 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