package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install

Dune Dependency

Authors

Maintainers

Sources

goblint-2.4.0.tbz
sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6
sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af

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
val unique_count_args_from_config : string -> (module UniqueCountArgs)
module ThreadCreateUniqueCount = WrapperFunctionAnalysis0.ThreadCreateUniqueCount
module type WrapperArgs = sig ... end
module SpecBase (UniqueCount : Lattice.S with type t = int) (WrapperArgs : WrapperArgs) : sig ... end
OCaml

Innovation. Community. Security.