Module Wp.RefUsageSource

Sourcetype 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

Sourceval is_nullable : Frama_c_kernel.Cil_types.varinfo -> bool

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

Sourceval has_nullable : unit -> bool

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

Sourceval dump : unit -> unit
Sourceval compute : unit -> unit
Sourceval is_computed : unit -> bool