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

include module type of struct include WrapperFunctionAnalysis0 end

module type UniqueCountArgs = WrapperFunctionAnalysis0.UniqueCountArgs

module MakeUniqueCount = WrapperFunctionAnalysis0.MakeUniqueCount

val unique_count_args_from_config : string -> (module UniqueCountArgs)

module MallocUniqueCount = WrapperFunctionAnalysis0.MallocUniqueCount

module ThreadCreateUniqueCount =
  WrapperFunctionAnalysis0.ThreadCreateUniqueCount

module NodeFlatLattice = WrapperFunctionAnalysis0.NodeFlatLattice

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