sig
type delta = Dload | Dfield | Dshift of int list
val apply :
VarUsage.Model.value -> VarUsage.Context.delta -> VarUsage.Model.value
val eval : VarUsage.Context.delta list -> VarUsage.Model.value
type target =
Memory
| Validity
| Fcall of Cil_types.kernel_function * Cil_types.varinfo
| Logic of Cil_types.logic_info * Cil_types.logic_var
type t = VarUsage.Context.target * VarUsage.Context.delta list
val epsilon : VarUsage.Context.t
val assigned : VarUsage.Context.t
val validity : VarUsage.Context.t
val load :
'a * VarUsage.Context.delta list -> 'a * VarUsage.Context.delta list
val shift :
Cil_types.typ ->
'a * VarUsage.Context.delta list -> 'a * VarUsage.Context.delta list
val cast :
Cil_types.typ ->
Cil_types.typ ->
'a * VarUsage.Context.delta list -> 'a * VarUsage.Context.delta list
val function_param :
Cil_types.kernel_function ->
Cil_types.varinfo -> VarUsage.Context.target * 'a list
val logic_param :
Cil_types.logic_info ->
Cil_types.logic_var -> VarUsage.Context.target * 'a list
val in_spec : bool Pervasives.ref
val on_spec : 'a -> 'a Cil.visitAction
val pp_target : Format.formatter -> VarUsage.Context.target -> unit
val pp_access : Format.formatter -> VarUsage.Context.delta list -> unit
end