Draft
Conversation
kroening
force-pushed
the
uninitialized-check
branch
2 times, most recently
from
7c56ed4 to
a8069ba
Compare
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8545 +/- ##
===========================================
- Coverage 78.38% 78.27% -0.12%
===========================================
Files 1729 1729
Lines 200151 200453 +302
Branches 18244 18316 +72
===========================================
+ Hits 156883 156895 +12
- Misses 43268 43558 +290 ☔ View full report in Codecov by Sentry. |
Collaborator
|
Good to see this PR coming. What is your soundness argument? Does this check always detect all cases of uninitialized variables? Are there cases where it is known to miss? What are they? |
kroening
force-pushed
the
uninitialized-check
branch
from
a8069ba to
1059ee7
Compare
tautschnig
force-pushed
the
uninitialized-check
branch
from
1059ee7 to
09908d0
Compare
Replace bare uninitialized local variable declarations with explicit initialization in ~175 regression test files. These tests use uninitialized locals as a shorthand for nondeterministic values (e.g., int x; __CPROVER_assume(x > 0);). This is valid C but triggers --uninitialized-check when enabled globally. Prepares for --uninitialized-check becoming a default check. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
28 test cases covering scalar locals, struct/union/array members, nested structs, per-element array tracking, symbolic indices, heap allocation, pointer aliasing, goto across initialization, and various control flow patterns. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Shadow boolean tracking for detecting reads of uninitialized local variables (C11 §6.3.2.1p2 undefined behavior). The standard scopes UB to objects that "could have been declared with the register storage class (never had its address taken)" — address-taken locals yield merely indeterminate values, not UB. Design: for each tracked local variable, a shadow boolean $init is added to the symbol table. The first pass inserts DECL + init=false after each tracked variable's DECL. The assignment handler sets init=true on writes, and check_rec asserts init==true on reads. Features: - Per-member tracking for struct components (recursive, arbitrary depth) - Per-element tracking for constant-size arrays (up to 64 elements) - Symbolic array index handling (conjunction of all element flags) - Heap allocation tracking via pointer init flags - Heap aliasing via shared flag symbols - Union/byte_extract write handling - Function call return value tracking - DECL+ASSIGN optimization (skip variables initialized at declaration) - Skip address-taken (dirty) variables (not UB per C11 §6.3.2.1p2) - Skip compiler-generated temporaries Unifies goto-instrument --uninitialized-check to use the same goto_check_c implementation, removing the old uninitializedt. Includes documentation in properties.md and man pages. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Extend uninitialized variable checking to also cover address-taken (dirty) local variables using CBMC's shadow memory subsystem. While reading uninitialized dirty locals is NOT undefined behavior per C11 §6.3.2.1p2 (the value is merely indeterminate), it often indicates a bug. This check is therefore separate from the C UB check (--uninitialized-check). The GOTO transformation pass (uninitialized_precise.cpp): 1. Adds shadow memory built-in symbols and empty function bodies 2. Inserts __CPROVER_field_decl_local in __CPROVER_initialize 3. After each write (direct or through pointer), inserts set_field 4. Before each read of a tracked dirty local, inserts get_field+assert 5. Skips address_of subtrees (taking address is not a read) Symex resolves pointer aliasing and interprocedural writes precisely via the value set, giving full precision at 0-20% overhead. Includes documentation in properties.md and man pages, comparison test suite, and regression tests for dirty variable patterns. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
uninitialized-check
branch
from
09908d0 to
3961467
Compare
kroening
commented
Apr 11, 2026
| | `--undefined-shift-check` | add range checks for shift distances | | ||
| | `--nan-check` | add floating-point NaN checks | | ||
| | `--uninitialized-check` | add checks for uninitialized locals (experimental) | | ||
| | `--uninitialized-check` | add checks for reads of uninitialized locals (C11 UB) | |
Collaborator
Author
There was a problem hiding this comment.
This makes it sound like uninitalized local reads have been UB only since C11 -- my understanding is that this was UB since C90.
kroening
commented
Apr 11, 2026
| - Heap allocations (via pointer init flags) | ||
|
|
||
| **What is not checked (by design, per C11 §6.3.2.1p2):** | ||
| - Variables whose address has been taken ("dirty" variables) — reading |
Collaborator
Author
There was a problem hiding this comment.
This should say "local variables". There is talk about heap allocated variables above.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Uninitialized local or dynamically allocated variables have an indeterminate initial value.
Reading an indeterminate value may be undefined behavior, or may yield an unspecific value.
This adds a check for uninitialized local variables. The check is not added as a standard check.