Module `Goblint_lib.MCPRegistry`

type spec_modules = {

}

val activated : (int * spec_modules) list Prelude.Ana.ref

val activated_ctx_sens : (int * spec_modules) list Prelude.Ana.ref

val registered : (int, spec_modules) Goblint_lib.Prelude.Ana.Hashtbl.t

val registered_name : (string, int) Goblint_lib.Prelude.Ana.Hashtbl.t

val register_analysis : ?dep:string list -> (module Analyses.MCPSpec) -> unit

val find_spec : int -> spec_modules

val find_spec_name : int -> string

val find_id : string -> int

type unknown = Obj.t

module type DomainListPrintableSpec = sig ... end

module type DomainListSysVarSpec = sig ... end

module type DomainListMCPASpec = sig ... end

module type DomainListLatticeSpec = sig ... end

module PrintableOfLatticeSpec
  (D : DomainListLatticeSpec) : 
  DomainListPrintableSpec

module PrintableOfMCPASpec (D : DomainListMCPASpec) : DomainListPrintableSpec

module PrintableOfSysVarSpec
  (D : DomainListSysVarSpec) : 
  DomainListPrintableSpec

module DomListPrintable
  (DLSpec : DomainListPrintableSpec) : 
  Printable.S with type t = (int * unknown) list

module DomVariantPrintable
  (DLSpec : DomainListPrintableSpec) : 
  Printable.S with type t = int * unknown

module DomVariantSysVar
  (DLSpec : DomainListSysVarSpec) : 
  Analyses.SpecSysVar with type t = int * unknown

module DomListLattice
  (DLSpec : DomainListLatticeSpec) : 
  Lattice.S with type t = (int * unknown) list

module DomVariantLattice0
  (DLSpec : DomainListLatticeSpec) : 
  Lattice.S with type t = int * unknown

module DomVariantLattice (DLSpec : DomainListLatticeSpec) : sig ... end

module LocalDomainListSpec : DomainListLatticeSpec

module GlobalDomainListSpec : DomainListLatticeSpec

module ContextListSpec : DomainListPrintableSpec

module VarListSpec : DomainListSysVarSpec

module AccListSpec : DomainListMCPASpec

Install