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.5.0.tbz

sha256=452d8491527aea21f2cbb11defcc14ba0daf9fdb6bdb9fc0af73e56eac57b916

sha512=1993cd45c4c7fe124ca6e157f07d17ec50fab5611b270a434ed1b7fb2910aa85a8e6eaaa77dad770430710aafb2f6d676c774dd33942d921f23e2f9854486551

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

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)