Module Wp.RefUsage

type access =
  1. | NoAccess
    (*

    Never used

    *)
  2. | ByRef
    (*

    Only used as "*x", equals to load(shift(load(&x),0))

    *)
  3. | ByArray
    (*

    Only used as "x[_]", equals to load(shift(load(&x),_))

    *)
  4. | ByValue
    (*

    Only used as "x", equals to load(&x)

    *)
  5. | 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