Goblint_lib.MCPRegistrytype spec_modules = {name : string;dep : string list;spec : (module Analyses.MCPSpec);dom : (module Lattice.S);glob : (module Lattice.S);cont : (module Printable.S);var : (module Analyses.SpecSysVar);acc : (module Analyses.MCPA);}val activated : (int * spec_modules) list Prelude.Ana.refval activated_ctx_sens : (int * spec_modules) list Prelude.Ana.refval registered : (int, spec_modules) Goblint_lib.Prelude.Ana.Hashtbl.tval registered_name : (string, int) Goblint_lib.Prelude.Ana.Hashtbl.tval register_analysis : ?dep:string list -> (module Analyses.MCPSpec) -> unitval find_spec : int -> spec_modulestype unknown = Obj.tmodule type DomainListPrintableSpec = sig ... endmodule type DomainListSysVarSpec = sig ... endmodule type DomainListMCPASpec = sig ... endmodule type DomainListLatticeSpec = sig ... endmodule PrintableOfMCPASpec (D : DomainListMCPASpec) : DomainListPrintableSpecmodule DomListPrintable
(DLSpec : DomainListPrintableSpec) :
Printable.S with type t = (int * unknown) listmodule DomVariantPrintable
(DLSpec : DomainListPrintableSpec) :
Printable.S with type t = int * unknownmodule DomVariantSysVar
(DLSpec : DomainListSysVarSpec) :
Analyses.SpecSysVar with type t = int * unknownmodule DomListLattice
(DLSpec : DomainListLatticeSpec) :
Lattice.S with type t = (int * unknown) listmodule DomVariantLattice0
(DLSpec : DomainListLatticeSpec) :
Lattice.S with type t = int * unknownmodule DomVariantLattice (DLSpec : DomainListLatticeSpec) : sig ... endmodule LocalDomainListSpec : DomainListLatticeSpecmodule ContextListSpec : DomainListPrintableSpecmodule VarListSpec : DomainListSysVarSpecmodule AccListSpec : DomainListMCPASpec