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 : '-> 'Cil.visitAction
  val pp_target : Format.formatter -> VarUsage.Context.target -> unit
  val pp_access : Format.formatter -> VarUsage.Context.delta list -> unit
end