Initialize nondet locals in regression tests

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.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

regression/cbmc/ACSL/operators.c

@@ -1,6 +1,6 @@
 void boolean()
 {
-  __CPROVER_bool a, b;
+  __CPROVER_bool a = __VERIFIER_nondet__Bool(), b = __VERIFIER_nondet__Bool();
   __CPROVER_assert((a ≡ b) == (a == b), "≡");
   __CPROVER_assert((a ≢ b) == (a != b), "≢");
   __CPROVER_assert((a ⇒ b) == (!a || b), "⇒");
@@ -13,7 +13,7 @@ void boolean()
 
 void relations()
 {
-  int a, b;
+  int a = __VERIFIER_nondet_int(), b = __VERIFIER_nondet_int();
   __CPROVER_assert((a ≥ b) == (a >= b), "≥");
   __CPROVER_assert((a ≤ b) == (a <= b), "≤");
   __CPROVER_assert((a ≡ b) == (a == b), "≡");

regression/cbmc/Array_Pointer3/main.c

@@ -1,4 +1,4 @@
-int x, y;
+int x = __VERIFIER_nondet_int(), y = __VERIFIER_nondet_int();
 
 int z[10];
 
@@ -62,7 +62,7 @@ int f(int j, int k)
 
 int main()
 {
-  int x, y;
+  int x = __VERIFIER_nondet_int(), y = __VERIFIER_nondet_int();
   __CPROVER_assume(x > y);
   __CPROVER_assume(x >= 0);
   __CPROVER_assume((y > 15) && (y < 18));

regression/cbmc/Array_UF1/main.c

@@ -1,7 +1,8 @@
 int main()
 {
   int a[10], b[10];
-  int x, y, z;
+  int x = __VERIFIER_nondet_int(), y = __VERIFIER_nondet_int(),
+      z = __VERIFIER_nondet_int();
   __CPROVER_assume(2 <= y && y <= 4);
   __CPROVER_assume(6 <= z && z <= 8);
   b[y] = x;

regression/cbmc/Array_UF2/main.c

@@ -1,7 +1,8 @@
 int main()
 {
   int a[4], b[4];
-  int x, y, z;
+  int x = __VERIFIER_nondet_int(), y = __VERIFIER_nondet_int(),
+      z = __VERIFIER_nondet_int();
   __CPROVER_assume(1 <= y && y <= 3);
   __CPROVER_assume(0 <= z && z <= 2);
   b[y] = x;

regression/cbmc/Array_operations1/main.c

@@ -2,7 +2,7 @@ void test_equal()
 {
   char array1[100], array2[100];
   _Bool cmp;
-  int index;
+  int index = __VERIFIER_nondet_int();
 
   cmp = __CPROVER_array_equal(array1, array2);
 

regression/cbmc/Array_operations2/main.c

@@ -11,7 +11,7 @@ int main()
 {
   my_struct arr[3] = {0};
   char *ptr = &(arr[1].c[2]);
-  int offset;
+  int offset = __VERIFIER_nondet_int();
   __CPROVER_assume(offset < 1 && offset > -1);
   void *ptr_plus = ptr + offset;
   char nondet[3];

regression/cbmc/Array_operations4/main.c

@@ -3,7 +3,7 @@ int main()
   char source[8];
   int int_source[2];
   int target[4];
-  int n;
+  int n = __VERIFIER_nondet_int();
   if(n >= 0 && n < 3)
   {
     __CPROVER_array_replace(&target[n], source);

regression/cbmc/Associativity1/main.c

@@ -1,11 +1,12 @@
 #include <assert.h>
 
 int main (void) {
-	int x;
+  int x = __VERIFIER_nondet_int();
 
-	while ((x + 1) -x != 1) {
-		assert(0);
-	}
+  while((x + 1) - x != 1)
+  {
+    assert(0);
+  }
 
-	return 0;
+  return 0;
 }

regression/cbmc/BV_Arithmetic6/main.c

@@ -1,7 +1,7 @@
 int main()
 {
   {
-    unsigned i, j, k, l;
+    unsigned i, j, k = __VERIFIER_nondet_unsigned(), l;
 
     j=k;
     i=j/2;
@@ -15,7 +15,7 @@ int main()
   }
 
   {
-    signed int i, j, k, l;
+    signed int i, j, k = __VERIFIER_nondet_signed_int(), l;
 
     // shifting rounds into the wrong direction
     __CPROVER_assume(!(k&1));

regression/cbmc/Bitfields1/main.c

@@ -30,7 +30,7 @@ struct bft {
 };
 
 int main() {
-  struct bft bf;
+  struct bft bf = {0};
 
   assert(bf.a<=7);
   assert(bf.b<=1);