Module Wp.RefUsage

module RefUsage: sig .. end

type access = 
| NoAccess (*
Never used
*)
| ByRef (*
Only used as "*x", equals to load(shift(load(&x),0))
*)
| ByArray (*
Only used as "x[_]", equals to load(shift(load(&x),_))
*)
| ByValue (*
Only used as "x", equals to load(&x)
*)
| ByAddr (*
Widely used, potentially up to "&x"
*)
By lattice order of usage
val get : ?kf:Cil_types.kernel_function ->
?init:bool -> Cil_types.varinfo -> access
val iter : ?kf:Cil_types.kernel_function ->
?init:bool -> (Cil_types.varinfo -> access -> unit) -> unit
val print : Cil_types.varinfo -> access -> Format.formatter -> unit
val dump : unit -> unit
val compute : unit -> unit