package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

Dune Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (8)

Authors

Maintainers

Sources

goblint-2.2.1.tbz

sha256=ca24f72fa9a87d288affe97c411753f14b7802bab4ca3649b337276b89bf5674

sha512=394b3521ccda0da91540cebb2f433f7525763060be4bbe179edd3b952a3580a8e173c4e410fc6895dc67fe6d17e6699aeddfed600f4692858bec093dd912bf1e

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

Module `Goblint_lib.MCP`

MCP analysis specification.

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

type unknown = Obj.t

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)