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/WrapperFunctionAnalysis/index.html

Module `Goblint_lib.WrapperFunctionAnalysis`

Family of analyses which provide symbolic locations for special library functions. Provides symbolic heap locations for dynamic memory allocations and symbolic thread identifiers for thread creation (mallocWrapper, threadCreateWrapper).

Provided heap locations are based on the node and thread ID. Provided thread identifiers are based solely the node. Considers wrapper functions and a number of unique heap locations or thread identifiers for additional precision.

module Q = Queries

module type UniqueCountArgs = sig ... end

module MakeUniqueCount (UniqueCountArgs : sig ... end) : sig ... end

val unique_count_args_from_config : string -> (module UniqueCountArgs)

module MallocUniqueCount : sig ... end

module ThreadCreateUniqueCount : sig ... end

module NodeFlatLattice : sig ... end

module type WrapperArgs = sig ... end

module SpecBase
  (UniqueCount : Lattice.S with type t = int)
  (WrapperArgs : WrapperArgs) : 
  sig ... end

module MallocWrapper : Analyses.MCPSpec

module ThreadCreateWrapper : Analyses.MCPSpec