MCP (goblint.Goblint

include module type of struct include MCPRegistry end

type spec_modules = MCPRegistry.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);
path : (module DisjointDomain.Representative);

}

val activated : (int * spec_modules) list Batteries.ref

val activated_context_sens : (int * spec_modules) list Batteries.ref

val activated_path_sens : (int * spec_modules) list Batteries.ref

val registered : (int, spec_modules) Batteries.Hashtbl.t

val registered_name : (string, int) Batteries.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

module type DomainListPrintableSpec = MCPRegistry.DomainListPrintableSpec

module type DomainListRepresentativeSpec =
  MCPRegistry.DomainListRepresentativeSpec

module type DomainListSysVarSpec = MCPRegistry.DomainListSysVarSpec

module type DomainListMCPASpec = MCPRegistry.DomainListMCPASpec

module type DomainListLatticeSpec = MCPRegistry.DomainListLatticeSpec

module PrintableOfLatticeSpec = MCPRegistry.PrintableOfLatticeSpec

module PrintableOfRepresentativeSpec =
  MCPRegistry.PrintableOfRepresentativeSpec

module PrintableOfMCPASpec = MCPRegistry.PrintableOfMCPASpec

module PrintableOfSysVarSpec = MCPRegistry.PrintableOfSysVarSpec

module DomListPrintable = MCPRegistry.DomListPrintable

module DomVariantPrintable = MCPRegistry.DomVariantPrintable

module DomVariantSysVar = MCPRegistry.DomVariantSysVar

module DomListRepresentative = MCPRegistry.DomListRepresentative

module DomListLattice = MCPRegistry.DomListLattice

module DomVariantLattice0 = MCPRegistry.DomVariantLattice0

module DomVariantLattice = MCPRegistry.DomVariantLattice

module LocalDomainListSpec = MCPRegistry.LocalDomainListSpec

module GlobalDomainListSpec = MCPRegistry.GlobalDomainListSpec

module ContextListSpec = MCPRegistry.ContextListSpec

module VarListSpec = MCPRegistry.VarListSpec

module AccListSpec = MCPRegistry.AccListSpec

module PathListSpec = MCPRegistry.PathListSpec

module MCP2 : 
  Analyses.Spec
    with module D = DomListLattice(LocalDomainListSpec)
     and module G = DomVariantLattice(GlobalDomainListSpec)
     and module C = DomListPrintable(ContextListSpec)
     and module V = DomVariantSysVar(VarListSpec)
     and module P = DomListRepresentative(PathListSpec)