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