Module RefUsage

module RefUsage: sig .. end

type var = 
| Result
| Cvar of Cil_types.varinfo
| Lvar of Cil_types.logic_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 = 
| L
| E of value
| Loc_var of Cil_types.varinfo
| Loc_shift of Cil_types.varinfo * value
| Val_var of var
| Val_shift of var * value
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