Module VarUsage.Context

module Context: sig .. end

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