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 =
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