Initialize nondet locals in regression tests

[tautschnig]

Prepares for --uninitialized-check becoming a default check.

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 undefined behaviour in C that we used to tolerate in CBMC. Once we enable --uninitialized-check by default, however, those would have become (unwanted) verification failures.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

This PR updates CBMC regression tests to avoid relying on undefined behaviour from reading uninitialized locals as a shorthand for nondeterministic values, in preparation for --uninitialized-check becoming a default check.

Changes:

• Replace uninitialized scalar locals with explicit nondet initializers (e.g., __VERIFIER_nondet_int() / __VERIFIER_nondet__Bool()).
• Replace uninitialized aggregates (struct/union/arrays) with explicit initialization (often {0}) in tests where nondet contents aren’t required.
• Minor formatting adjustments in a few tests while applying the above.

Reviewed changes

Copilot reviewed 175 out of 175 changed files in this pull request and generated 12 comments.

Show a summary per file

File	Description
regression/cbmc/void_pointer3/main.c	Initialize previously-uninitialized offsets with nondet calls.
regression/cbmc/unwind_counters4/main.c	Initialize loop-control locals with nondet calls.
regression/cbmc/union3/main.c	Initialize previously-uninitialized scalar used as nondet.
regression/cbmc/union2/main.c	Zero-initialize union local.
regression/cbmc/union18/main.c	Zero-initialize union local.
regression/cbmc/union17/main.c	Initialize previously-uninitialized scalar used as nondet.
regression/cbmc/union14/main.c	Zero-initialize union locals used for representation punning.
regression/cbmc/union1/main.c	Zero-initialize union local.
regression/cbmc/union/union_member.c	Zero-initialize struct containing anonymous union.
regression/cbmc/union/union_large_array.c	Zero-initialize union local.
regression/cbmc/uninterpreted_function/uf2.c	Initialize previously-uninitialized scalars used as nondet.
regression/cbmc/uniform_array1/main.c	Initialize index variable with nondet.
regression/cbmc/Undefined_Shift1/main.c	Initialize shift operands with nondet.
regression/cbmc/Unbounded_Array5/main.c	Initialize loop/index scalars with nondet.
regression/cbmc/Unbounded_Array1/main.c	Initialize size/index scalars with nondet.
regression/cbmc/Typecast1/main.c	Initialize scalar used in assume with nondet.
regression/cbmc/sync_X_and_fetch-1/main.c	Initialize operand scalar with nondet (sync builtin test).
regression/cbmc/sync_val_compare-1/main.c	Initialize compare/swap operands with nondet.
regression/cbmc/sync_fetch_and_X-1/main.c	Initialize operand scalar with nondet (sync builtin test).
regression/cbmc/sync_bool_compare-1/main.c	Initialize compare/swap operands with nondet.
regression/cbmc/switch4/main.c	Initialize switch selector with nondet.
regression/cbmc/switch2/main.c	Initialize switch selector with nondet.
regression/cbmc/switch1/main.c	Initialize switch selector with nondet.
regression/cbmc/struct8/main.c	Initialize scalar locals with nondet.
regression/cbmc/struct7/main.c	Initialize scalar local with nondet.
regression/cbmc/struct3/main.c	Zero-initialize struct local.
regression/cbmc/struct1/main.c	Zero-initialize struct local.
regression/cbmc/Struct_Propagation1/main.c	Initialize boolean branch selector with nondet.
regression/cbmc/Struct_Initialization5/main.c	Zero-initialize struct local.
regression/cbmc/Struct_Initialization2/main.c	Initialize scalar used in designated init with nondet.
regression/cbmc/String8/main.c	Initialize boolean branch selector with nondet.
regression/cbmc/String_Abstraction22/main.c	Initialize boolean selector with nondet.
regression/cbmc/String_Abstraction21/strcpy2.c	Initialize length with nondet.
regression/cbmc/String_Abstraction18/strcpy.c	Initialize length with nondet.
regression/cbmc/String_Abstraction15/pass-in.c	Initialize length with nondet.
regression/cbmc/String_Abstraction14/pass-in-implicit.c	Initialize length with nondet.
regression/cbmc/simplify-array-size/main.c	Initialize size_t control value with nondet.
regression/cbmc/sat-solver-warning/test.c	Initialize scalar with nondet.
regression/cbmc/runtime-profiling/main.c	Initialize scalar with nondet.
regression/cbmc/return4/main.c	Initialize flag with nondet.
regression/cbmc/Recursion2/main.c	Initialize recursion depth with nondet.
regression/cbmc/r_w_ok7/main.c	Initialize size_t values with nondet.
regression/cbmc/r_w_ok1/main.c	Initialize allocation size with nondet.
regression/cbmc/Quantifiers-statement-expression3/main.c	Initialize scalar captured in quantifier expression with nondet.
regression/cbmc/Quantifiers-simplify/rewrite_exists.c	Initialize scalar used in quantified assume with nondet.
regression/cbmc/Quantifiers-expr-cleaning/main.c	Initialize boolean selector with nondet.
regression/cbmc/pragma_cprover2/main.c	Initialize scalar used in pragma-controlled region with nondet.
regression/cbmc/pragma_cprover1/main.c	Initialize scalar with nondet.
regression/cbmc/pragma_cprover_enable2/main.c	Initialize scalar used in pragma-controlled region with nondet.
regression/cbmc/pragma_cprover_enable1/main.c	Initialize scalar with nondet.
regression/cbmc/Pointer9/main.c	Initialize flag with nondet.
regression/cbmc/Pointer26/main.c	Initialize scalar used to build null pointer with nondet.
regression/cbmc/Pointer25/main.c	Initialize scalar with nondet.
regression/cbmc/Pointer15/main.c	Initialize scalar with nondet.
regression/cbmc/Pointer1/main.c	Initialize branch selector with nondet.
regression/cbmc/pointer-predicates/at_bounds1.c	Initialize allocation size with nondet.
regression/cbmc/Pointer_difference2/main.c	Initialize boolean selectors with nondet.
regression/cbmc/Pointer_comparison3/main.c	Initialize boolean selector with nondet.
regression/cbmc/Pointer_byte_extract4/main.c	Initialize boolean selector with nondet + formatting adjustments.
regression/cbmc/Pointer_array8/main.c	Initialize scalar with nondet.
regression/cbmc/Pointer_Arithmetic11/main.c	Initialize scalar with nondet.
regression/cbmc/overflow/signed_subtraction1.c	Initialize scalars with nondet.
regression/cbmc/overflow/signed_multiplication1.c	Initialize scalars with nondet.
regression/cbmc/overflow/leftshift_overflow.c	Initialize u32 with nondet.
regression/cbmc/null7/main.c	Initialize length with nondet.
regression/cbmc/no-propagation/main.c	Initialize scalar with nondet.
regression/cbmc/Mod2/main.c	Initialize scalars with nondet.
regression/cbmc/Minisat_Simp1/main.c	Initialize double with nondet.
regression/cbmc/Malloc9/main.c	Initialize boolean selector with nondet.
regression/cbmc/Malloc7/main.c	Initialize pointer local to null.
regression/cbmc/Malloc2/main.c	Initialize pointer local to null.
regression/cbmc/Malloc18/main.c	Initialize size with nondet.
regression/cbmc/Malloc17/main.c	Initialize sizes with nondet.
regression/cbmc/Malloc13/main.c	Initialize length with nondet.
regression/cbmc/Malloc11/main.c	Initialize scalar and boolean with nondet.
regression/cbmc/little-endian-array1/main.c	Initialize scalar with nondet.
regression/cbmc/lhs-pointer-aliases-constant/test.c	Initialize boolean selector with nondet.
regression/cbmc/inequality-with-constant-normalisation1/main.c	Initialize booleans with nondet.
regression/cbmc/inequality-with-constant-normalisation/main.c	Initialize scalar with nondet.
regression/cbmc/if4/main.c	Initialize scalar with nondet.
regression/cbmc/if1/main.c	Initialize scalar with nondet.
regression/cbmc/havoc_object1/main.c	Initialize boolean selector with nondet.
regression/cbmc/guard1/main.c	Initialize scalars with nondet + formatting adjustments.
regression/cbmc/goto2/main.c	Initialize scalar with nondet.
regression/cbmc/goto1/main.c	Initialize scalars with nondet.
regression/cbmc/gcc_vector3/main.c	Zero-initialize union locals used for vector/byte access.
regression/cbmc/gcc_vector1/main.c	Zero-initialize union locals used for vector/byte access.
regression/cbmc/gcc_switch_case_range2/main.c	Initialize scalar with nondet.
regression/cbmc/gcc_switch_case_range1/main.c	Initialize scalar with nondet.
regression/cbmc/Function4/main.c	Initialize return value with nondet.
regression/cbmc/Function1/main.c	Initialize scalar with nondet + minor formatting adjustments.
regression/cbmc/Function_Pointer6/main.c	Initialize scalar with nondet.
regression/cbmc/Function_Pointer2/main.c	Initialize boolean selector with nondet.
regression/cbmc/Function_Pointer10/main.c	Initialize scalar with nondet.
regression/cbmc/Float8/main.c	Initialize scalar with nondet.
regression/cbmc/Float6/main.c	Initialize floats with nondet.
regression/cbmc/Float5/main.c	Initialize float with nondet.
regression/cbmc/Float4/main.c	Initialize double with nondet.
regression/cbmc/Float23/main.c	Initialize floats with nondet.
regression/cbmc/Float22/main.c	Zero-initialize unions used for field access; formatting adjustments.
regression/cbmc/Float20/main.c	Initialize float/double values with nondet.
regression/cbmc/Float12/main.c	Initialize float and char with nondet.
regression/cbmc/Float-zero-sum1/main.c	Zero-initialize union used for float/int view.
regression/cbmc/Float-rounding2/main.c	Initialize double(s) with nondet.
regression/cbmc/Float-no-simp5/main.c	Initialize doubles with nondet; zero-init unions.
regression/cbmc/Float-no-simp4/main.c	Initialize doubles with nondet.
regression/cbmc/Float-no-simp2/main.c	Initialize double with nondet.
regression/cbmc/Float-flags-simp1/main.c	Initialize double with nondet.
regression/cbmc/Float-flags-no-simp1/main.c	Initialize double with nondet.
regression/cbmc/Float-equality2/main.c	Initialize floats with nondet.
regression/cbmc/Float-equality1/main.c	Initialize doubles with nondet.
regression/cbmc/Fixedbv6/main.c	Zero-initialize fixedbv locals (changed semantics).
regression/cbmc/Fixedbv5/main.c	Zero-initialize fixedbv locals (changed semantics).
regression/cbmc/Fixedbv4/main.c	Zero-initialize fixedbv local.
regression/cbmc/field-sensitivity16/main.c	Initialize scalar with nondet; zero-init union.
regression/cbmc/field-sensitivity15/main.c	Initialize scalar with nondet; zero-init union.
regression/cbmc/exit1/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_union3/main.c	Zero-init union local; initialize scalar with nondet; formatting adjustments.
regression/cbmc/equality_through_union2/main.c	Zero-init union local; initialize scalar with nondet; formatting adjustments.
regression/cbmc/equality_through_union1/main.c	Zero-init union local; initialize scalar with nondet; formatting adjustments.
regression/cbmc/equality_through_struct4/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_struct3/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_struct2/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_struct1/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_struct_containing_arrays2/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_struct_containing_arrays1/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_array6/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_array5/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_array4/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_array3/main.c	Initialize scalars with nondet.
regression/cbmc/equality_through_array2/main.c	Initialize scalars with nondet.
regression/cbmc/equality_through_array1/main.c	Initialize scalars with nondet.
regression/cbmc/equality_through_array_of_struct4/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_array_of_struct3/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_array_of_struct2/main.c	Initialize scalar with nondet.
regression/cbmc/equality_through_array_of_struct1/main.c	Initialize scalar with nondet.
regression/cbmc/enum9/main.c	Initialize scalar with nondet; set enum/struct initial values.
regression/cbmc/enum3/main.c	Initialize enum local to a concrete value.
regression/cbmc/Endianness8/main.c	Zero-initialize union local.
regression/cbmc/End_thread1/main.c	Initialize scalar with nondet.
regression/cbmc/Empty_struct1/main.c	Initialize booleans with nondet.
regression/cbmc/Ellipsis2/main.c	Initialize scalar locals with nondet.
regression/cbmc/dynamic_sizeof1/main.c	Initialize scalar with nondet.
regression/cbmc/dynamic_size1/stack_object.c	Initialize size with nondet.
regression/cbmc/divide-by-one-simplify/main.c	Initialize float with nondet.
regression/cbmc/condition-propagation-4/test.c	Initialize scalar with nondet.
regression/cbmc/Computed-Goto1/main.c	Initialize scalar with nondet.
regression/cbmc/clang_builtins/rotate.c	Initialize one builtin operand (others remain uninitialized).
regression/cbmc/clang_builtins/bitreverse.c	Initialize one builtin operand (others remain uninitialized).
regression/cbmc/byte_update18/main.c	Initialize scalar with nondet.
regression/cbmc/byte_update17/main.c	Initialize scalar with nondet.
regression/cbmc/byte_update16/main.c	Initialize scalar with nondet.
regression/cbmc/byte_update15/main.c	Initialize scalar with nondet.
regression/cbmc/byte_update12/main.c	Initialize scalar with nondet.
regression/cbmc/byte_update11/main.c	Initialize scalar with nondet.
regression/cbmc/BV_Arithmetic6/main.c	Initialize select scalars with nondet.
regression/cbmc/bounds_check2/main.c	Zero-initialize array local.
regression/cbmc/bounds_check1/main.c	Initialize index locals with nondet.
regression/cbmc/Boolean_Guards1/main.c	Initialize scalars with nondet; zero-init array.
regression/cbmc/Bitfields2/main.c	Zero-initialize union local.
regression/cbmc/Bitfields1/main.c	Zero-initialize bitfield struct local.
regression/cbmc/big-endian-array1/main.c	Initialize scalar with nondet.
regression/cbmc/aws-byte-buf-regression/main.c	Initialize scalar with nondet.
regression/cbmc/atomic_X_fetch-1/main.c	Initialize operand scalar with nondet (atomic builtin test).
regression/cbmc/atomic_fetch_X-1/main.c	Initialize operand scalar with nondet (atomic builtin test).
regression/cbmc/Associativity1/main.c	Initialize scalar with nondet + formatting adjustments.
regression/cbmc/array-tests/zero-sized.c	Initialize index scalar with nondet.
regression/cbmc/array-tests/uf-always.c	Initialize scalar locals with nondet.
regression/cbmc/Array_UF2/main.c	Initialize scalars with nondet.
regression/cbmc/Array_UF1/main.c	Initialize scalars with nondet.
regression/cbmc/Array_Pointer3/main.c	Initialize globals/locals with nondet (includes file-scope init change).
regression/cbmc/Array_operations4/main.c	Initialize scalar with nondet.
regression/cbmc/Array_operations2/main.c	Initialize scalar with nondet.
regression/cbmc/Array_operations1/main.c	Initialize scalar with nondet.
regression/cbmc/ACSL/operators.c	Initialize scalars/booleans with nondet for ACSL operator checks.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.47%. Comparing base (cd64a96) to head (b85ff5f).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8956   +/-   ##
========================================
  Coverage    80.47%   80.47%           
========================================
  Files         1704     1704           
  Lines       188762   188762           
  Branches        73       73           
========================================
+ Hits        151908   151910    +2     
+ Misses       36854    36852    -2     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.