Frama-C:
Plug-ins:
Libraries:

Frama-C API - Equality

Equalities between syntactic lvalues and expressions.

type 'a trivial =
  1. | Trivial
  2. | NonTrivial of 'a
type 'a tree =
  1. | Empty
  2. | Leaf of 'a
  3. | Node of 'a tree * 'a tree
type elt = Hcexprs.HCE.t

The type of the equality elements.

module Equality : sig ... end

Representation of an equality between a set of elements. The signatures is roughly a subset of Ocaml's Set.S. An equality always contains at least two elements; operations that break this invariant return Trivial.

type equality = Equality.t
module Set : sig ... end

Sets of equalities.