Module `Zero_alloc_utils.Assume_info`Source

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.

Sourcetype t

Sourceval none : t

Source

val create : 
  strict:bool ->
  never_returns_normally:bool ->
  never_raises:bool ->
  inferred:bool ->
  t

Sourceval compare : t -> t -> int

Sourceval equal : t -> t -> bool

Sourceval join : t -> t -> t

Sourceval meet : t -> t -> t

Sourceval to_string : t -> string

Sourceval print : Format.formatter -> t -> unit

Sourceval is_none : t -> bool

Sourceval is_inferred : t -> bool

Sourcemodule Witnesses : sig ... end

Sourcemodule V : sig ... end

Sourcemodule Value : sig ... end

Sourceval get_value : t -> Value.t option

Module Zero_alloc_utils.Assume_infoSource

Module `Zero_alloc_utils.Assume_info`Source