Module `Zero_alloc_utils.Assume_info`

The Assume_info module contains an instantiation of the abstract domain with trivial witnesses. It is used to propagate assume annotations from the front-end to the backend. The backend contains a different instantiation of the abstract domain where the witnesses contain actual information about allocations - see Checkmach.

type t

val none : Ocaml_utils.Zero_alloc_utils.Assume_info.t

val create : 
  strict:bool ->
  never_returns_normally:bool ->
  never_raises:bool ->
  inferred:bool ->
  Ocaml_utils.Zero_alloc_utils.Assume_info.t

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

val equal : 
  Ocaml_utils.Zero_alloc_utils.Assume_info.t ->
  Ocaml_utils.Zero_alloc_utils.Assume_info.t ->
  bool

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

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

val to_string : Ocaml_utils.Zero_alloc_utils.Assume_info.t -> string

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

val is_none : Ocaml_utils.Zero_alloc_utils.Assume_info.t -> bool

val is_inferred : Ocaml_utils.Zero_alloc_utils.Assume_info.t -> bool

module Witnesses : sig ... end

module V : sig ... end

module Value : sig ... end

val get_value : 
  Ocaml_utils.Zero_alloc_utils.Assume_info.t ->
  Ocaml_utils.Zero_alloc_utils.Assume_info.Value.t option

Module Zero_alloc_utils.Assume_info

Module `Zero_alloc_utils.Assume_info`