Module Binsec_symbolic.PathSource

Sourcetype ('state, 'model) partition =
  1. | False
    (*

    The condition is false.

    *)
  2. | True
    (*

    The condition is true.

    *)
  3. | Falsish of 'state
    (*

    The condition evaluates to false in the path models, but the given state may lead to true.

    *)
  4. | Trueish of 'state
    (*

    The condition evaluates to true in the path models, but the given state may lead to false.

    *)
  5. | Split of 'state * 'model list
    (*

    The condition evaluates to true in the path models, and evaluates to false in the given state and models.

    *)

Return type of the function S.partition.

Sourcemodule type S = sig ... end
Sourcemodule Make (_ : Metrics.S) (State : State.S) : sig ... end