module RefUsage: sig
.. end
type
var =
module Var: sig
.. end
type
access =
| |
NoAccess |
| |
ByAddr |
| |
ByValue |
| |
ByArray |
| |
ByRef |
module Access: sig
.. end
module E: sig
.. end
type
value = E.t
type
model =
val vcup : E.t -> E.t -> model
val fcup : ('a -> E.t) -> 'a list -> model
val value : model -> value
val cvar : Cil_types.varinfo -> model
val shift : model -> value -> model
val field : model -> model
val load : model -> model
val reference : model -> value
type
cast =
| |
Identity |
| |
Convert |
| |
Cast |
val cast : cast -> model -> model
val cast_obj : Ctypes.c_object -> Ctypes.c_object -> cast
val cast_ctyp : Cil_types.typ -> Cil_types.typ -> cast
val cast_ltyp : Cil_types.typ -> Cil_types.logic_type -> cast
val param : access -> model -> value
val call : E.t -> var list -> model list -> E.t
type
context = {
|
mutable locals : Cil_datatype.Logic_var.Set.t ; |
|
mutable logic : E.t Cil_datatype.Logic_info.Map.t ; |
|
mutable spec : E.t Kernel_function.Map.t ; |
|
mutable code : E.t Kernel_function.Map.t ; |
|
mutable w_kf : Kernel_function.Set.t ; |
|
mutable w_lg : Cil_datatype.Logic_info.Set.t ; |
}
val call_kf : context ->
Kernel_function.Set.elt -> model list -> E.t
val call_lg : context ->
Cil_datatype.Logic_info.Set.elt -> model list -> E.t
val vexpr : Cil_types.exp -> value
val expr : Cil_types.exp -> model
val lvalue : Cil_types.lval -> model
val host : Cil_types.lhost -> model
val offset : model -> Cil_types.offset -> model
val vterm : context -> Cil_types.term -> value
val vtermopt : context -> Cil_types.term option -> value
val term : context -> Cil_types.term -> model
val term_lval : context -> Cil_types.term_lval -> model
val term_indices : context -> model -> Cil_types.term_offset -> model
val term_offset : context -> model -> Cil_types.term_offset -> model
val addr_lval : context -> Cil_types.term_lval -> model
val pred : context -> Cil_types.predicate Cil_types.named -> E.t