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 is_nullable : Cil_types.varinfo -> bool

is_nullable vi returns true iff vi is a formal and has an attribute 'nullable'

val has_nullable : unit -> bool

has_nullable () return true iff there exists a variable that satisfies is_nullable

val print : Cil_types.varinfo -> access -> Stdlib.Format.formatter -> unit
val dump : unit -> unit
val compute : unit -> unit
val is_computed : unit -> bool