Ocaml_utils.Zero_alloc_utilsmodule type WS = sig ... endAbstract domain used in static analysis for checking
module type Component = sig ... endmodule Make_component (Witnesses : WS) : sig ... endmodule Make_value
(Witnesses : WS)
(V : Component with type witnesses := Witnesses.t) :
sig ... endmodule Assume_info : sig ... endThe 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.