Module `Goblint_lib.MCPRegistry`

Registry of dynamically activatable analyses. Analysis specification modules for the dynamic product.

type 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 ref

val activated_ctx_sens : (int * spec_modules) list ref

val activated_path_sens : (int * spec_modules) list 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 = sig ... end

module type DomainListRepresentativeSpec = sig ... end

module type DomainListSysVarSpec = sig ... end

module type DomainListMCPASpec = sig ... end

module type DomainListLatticeSpec = sig ... end

module PrintableOfLatticeSpec
  (D : DomainListLatticeSpec) : 
  DomainListPrintableSpec

module PrintableOfRepresentativeSpec
  (D : DomainListRepresentativeSpec) : 
  DomainListPrintableSpec

module PrintableOfMCPASpec (D : DomainListMCPASpec) : DomainListPrintableSpec

module PrintableOfSysVarSpec
  (D : DomainListSysVarSpec) : 
  DomainListPrintableSpec

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

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

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

module DomListRepresentative
  (DLSpec : DomainListRepresentativeSpec) : 
  DisjointDomain.Representative
    with type t = (int * Obj.t) list
     and type elt = (int * Obj.t) list

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

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

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

module LocalDomainListSpec : DomainListLatticeSpec

module GlobalDomainListSpec : DomainListLatticeSpec

module ContextListSpec : DomainListPrintableSpec

module VarListSpec : DomainListSysVarSpec

module AccListSpec : DomainListMCPASpec

module PathListSpec : DomainListRepresentativeSpec

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/MCPRegistry/index.html

Module `Goblint_lib.MCPRegistry`

package goblint

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/MCPRegistry/index.html

Module Goblint_lib.MCPRegistry

dune-project
Dependency

Module `Goblint_lib.MCPRegistry`