package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

dune-project

Dependency

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

Authors

Maintainers

Sources

goblint-2.6.0.tbz

sha256=20d5b7332a9f6072ab9ba86c4a53b898eaf681286c56a8805c41850bbf3ddf41

sha512=7c7685cfcd9aa866bc40e813df2bfcb3c79b3d40e615d8d6d0939c5798b9d70dd7f2ba87a741f5ba0ce891e9d254627207fb28057f1f2f6611e4e0d128fd6a71

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_context_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 = 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)