Module `Assume_info.V`

type t =
  Ocaml_utils.Zero_alloc_utils.Make_component(Ocaml_utils.Zero_alloc_utils.Assume_info.Witnesses).t =

| Top of Ocaml_utils.Zero_alloc_utils.Assume_info.Witnesses.t
| Safe
| Bot

val top : 
  Ocaml_utils.Zero_alloc_utils.Assume_info.Witnesses.t ->
  Ocaml_utils.Zero_alloc_utils.Assume_info.V.t

Property may not hold on some paths.

val safe : Ocaml_utils.Zero_alloc_utils.Assume_info.V.t

Property holds on all paths.

val bot : Ocaml_utils.Zero_alloc_utils.Assume_info.V.t

Not reachable.

val lessequal : 
  Ocaml_utils.Zero_alloc_utils.Assume_info.V.t ->
  Ocaml_utils.Zero_alloc_utils.Assume_info.V.t ->
  bool

Order of the abstract domain

val join : 
  Ocaml_utils.Zero_alloc_utils.Assume_info.V.t ->
  Ocaml_utils.Zero_alloc_utils.Assume_info.V.t ->
  Ocaml_utils.Zero_alloc_utils.Assume_info.V.t

val meet : 
  Ocaml_utils.Zero_alloc_utils.Assume_info.V.t ->
  Ocaml_utils.Zero_alloc_utils.Assume_info.V.t ->
  Ocaml_utils.Zero_alloc_utils.Assume_info.V.t

val compare : 
  Ocaml_utils.Zero_alloc_utils.Assume_info.V.t ->
  Ocaml_utils.Zero_alloc_utils.Assume_info.V.t ->
  int

Use compare for structural comparison of terms, for example to store them in a set. Use lessequal for checking fixed point of the abstract domain.

val print : 
  witnesses:bool ->
  Stdlib.Format.formatter ->
  Ocaml_utils.Zero_alloc_utils.Assume_info.V.t ->
  unit

Module Assume_info.V

Module `Assume_info.V`