sig
module type State =
sig
type t
val bottom : MemVal.State.t
val join : MemVal.State.t -> MemVal.State.t -> MemVal.State.t
val of_kinstr : Cil_types.kinstr -> MemVal.State.t
val of_stmt : Cil_types.stmt -> MemVal.State.t
val of_kf : Cil_types.kernel_function -> MemVal.State.t
val pretty : Stdlib.Format.formatter -> MemVal.State.t -> unit
end
module type Value =
sig
val configure : unit -> WpContext.rollback
val datatype : string
module State : State
type t
type state = MemVal.State.t
val null : MemVal.Value.t
val literal : eid:int -> Cstring.cst -> int * MemVal.Value.t
val cvar : Cil_types.varinfo -> MemVal.Value.t
val field : MemVal.Value.t -> Cil_types.fieldinfo -> MemVal.Value.t
val shift :
MemVal.Value.t -> Ctypes.c_object -> Lang.F.term -> MemVal.Value.t
val base_addr : MemVal.Value.t -> MemVal.Value.t
val load :
MemVal.Value.state ->
MemVal.Value.t -> Ctypes.c_object -> MemVal.Value.t
val domain : MemVal.Value.t -> Base.t list
val offset : MemVal.Value.t -> Lang.F.term -> Lang.F.pred
val pretty : Stdlib.Format.formatter -> MemVal.Value.t -> unit
end
module Make : functor (V : Value) -> Sigs.Model
module Eva : Value
end