Frama-C:
Plug-ins:
Libraries:

Frama-C API - DepsOrUnassigned

type t =
  1. | Unassigned
    (*

    Location has never been assigned

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

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

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