package frama-c

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Assigns.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
OCaml

Innovation. Community. Security.