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 a GoblintCil.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 tracking NULL bytes in C arrays.
• JmpBufDomain Domains for setjmp and longjmp analyses, and setjmp buffers.

Combined

• ValueDomain Domain for a single Base analysis value.
• ValueDomainQueries Queries within ValueDomain.

Concurrency

• MutexAttrDomain Mutex attribute type domain.
• ThreadIdDomain Thread ID domains.
• ConcDomain Domains for thread sets and their uniqueness.

Other

• Lval Domains for GoblintCil.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.