Module `Ocaml_utils.Zero_alloc_utils`Source

Sourcemodule type WS = sig ... end

Abstract domain used in static analysis for checking @zero_alloc annotations. See backend/zero_alloc_checker for details of the analysis. See this module's .ml file for details about the translation of user-provided annotations to abstract values in this domain.

Sourcemodule type Component = sig ... end

Sourcemodule Make_component (Witnesses : WS) : sig ... end

Source

module Make_value
  (Witnesses : WS)
  (V : Component with type witnesses := Witnesses.t) : 
  sig ... end

Sourcemodule Assume_info : sig ... end

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.

Module Ocaml_utils.Zero_alloc_utilsSource

Module `Ocaml_utils.Zero_alloc_utils`Source