Module Wp.RefUsage

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 iter : ?kf:Frama_c_kernel.Cil_types.kernel_function -> ?init:bool -> ( Frama_c_kernel.Cil_types.varinfo -> access -> unit ) -> unit
val is_nullable : Frama_c_kernel.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 : Frama_c_kernel.Cil_types.varinfo -> access -> Stdlib.Format.formatter -> unit
val dump : unit -> unit
val compute : unit -> unit
val is_computed : unit -> bool