package goblint
Static analysis framework for C
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-2.5.0.tbz
sha256=452d8491527aea21f2cbb11defcc14ba0daf9fdb6bdb9fc0af73e56eac57b916
sha512=1993cd45c4c7fe124ca6e157f07d17ec50fab5611b270a434ed1b7fb2910aa85a8e6eaaa77dad770430710aafb2f6d676c774dd33942d921f23e2f9854486551
doc/cdomain_value.html
Library goblint.cdomain.value
This library is unwrapped and provides the following top-level modules. For better context, see Goblint_lib
which also documents these modules.
Domains
Analysis-specific
Value
Non-relational
Numeric
IntDomain
Abstract domains for C integers.FloatDomain
Abstract domains for C floating-point numbers.
Addresses
Mval
Domains for mvalues: simplified lvalues, which start with aGoblintCil.varinfo
. Mvalues are the result of resolving pointer dereferences in lvalues.Offset
Domains for variable offsets, i.e. array indices and struct fields.StringDomain
String literals domain.AddressDomain
Domains for addresses/pointers.
Complex
StructDomain
Abstract domains for C structs.UnionDomain
Abstract domains for C unions.ArrayDomain
Abstract domains for C arrays.NullByteSet
Abstract domains for trackingNULL
bytes in C arrays.JmpBufDomain
Domains forsetjmp
andlongjmp
analyses, andsetjmp
buffers.
Combined
ValueDomain
Domain for a singleBase
analysis value.ValueDomainQueries
Queries withinValueDomain
.
Concurrency
MutexAttrDomain
Mutex attribute type domain.ThreadIdDomain
Thread ID domains.ConcDomain
Domains for thread sets and their uniqueness.
Other
Lval
Domains forGoblintCil.lval
.
I/O
Witnesses
Invariant
Invariants for witnesses.InvariantCil
Invariant manipulation related to CIL transformations.
Utilities
Analysis-specific
PrecisionUtil
Integer and floating-point option and attribute handling.WideningThresholds
Widening threshold utilities.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page