Frama-C:
Plug-ins:
Libraries:

Frama-C API - DepsOrUnassigned

type t =
  1. | DepsBottom
    (*

    Bottom of the lattice, never bound inside a memory state at a valid location. (May appear for bases for which the validity does not start at 0, currently only NULL.)

    *)
  2. | Unassigned
    (*

    Location has never been assigned

    *)
  3. | AssignedFrom of Deps.t
    (*

    Location guaranteed to have been overwritten, its contents depend on the Deps.t value

    *)
  4. | MaybeAssignedFrom of Deps.t
    (*

    Location may or may not have been overwritten

    *)

The lattice is DepsBottom <= Unassigned, DepsBottom <= AssignedFrom z, Unassigned <= MaybeAssignedFrom and AssignedFrom z <= MaybeAssignedFrom z.

val top : t
val equal : t -> t -> bool
val may_be_unassigned : t -> bool