Initialize nondet locals in regression tests

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

@@ -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,8 @@ struct bft {
 };
 
 int main() {
-  struct bft bf;
+  struct bft nondet_bft(void);
+  struct bft bf = nondet_bft();
 
   assert(bf.a<=7);
   assert(bf.b<=1);

regression/cbmc/Bitfields2/main.c

@@ -40,7 +40,8 @@ unsigned foo(union U u, struct S0 s)
 int main()
 {
   struct S0 main_s = { 0, 1, 2, 3, 4, 5, 6, 7, 8 };
-  union U main_u;
+  union U nondet_U(void);
+  union U main_u = nondet_U();
 
   assert(8==foo(main_u, main_s));
 

regression/cbmc/Boolean_Guards1/main.c

@@ -1,18 +1,20 @@
-int main() {
-  unsigned x;
-  int i;
+int main()
+{
+  unsigned x = __VERIFIER_nondet_unsigned();
+  int i = __VERIFIER_nondet_int();
   int a[100];
+  __CPROVER_havoc_object(a);
 
   // this is guaranteed not to be a buffer overflow
-  if(x<100 && a[x])
+  if(x < 100 && a[x])
   {
     i++;
   }
 
-  __CPROVER_assume(i<100);
+  __CPROVER_assume(i < 100);
 
   // this is guaranteed not to be a buffer underflow
-  if(i>=0 && a[i])
+  if(i >= 0 && a[i])
   {
     i++;
   }

regression/cbmc/Computed-Goto1/main.c

@@ -1,7 +1,7 @@
 int main()
 {
   static void *table[] = {&&l0, &&l1, &&l2};
-  int in, out;
+  int in = __VERIFIER_nondet_int(), out;
 
   if(in>=0 && in<=2)
   {

regression/cbmc/Ellipsis2/main.c

@@ -7,8 +7,8 @@ int foo(int a, ...)
 
 int main()
 {
-  char c;
-  long l;
+  char c = __VERIFIER_nondet_char();
+  long l = __VERIFIER_nondet_long();
 
   if(c<l)
     l=foo(c, c);

regression/cbmc/Empty_struct1/main.c

@@ -7,7 +7,7 @@ struct empty
 int main()
 {
   struct empty e1, e2, e3;
-  _Bool b, c=b;
+  _Bool b = __VERIFIER_nondet__Bool(), c = b;
   e1=e2;
   if(b)
     e3=e2;

regression/cbmc/End_thread1/main.c

@@ -10,7 +10,7 @@ void pthread_exit(void *value_ptr);
 
 int main()
 {
-  int i;
+  int i = __VERIFIER_nondet_int();
 
   if(i == 100)
   {

regression/cbmc/Fixedbv4/main.c

@@ -4,7 +4,8 @@ typedef __CPROVER_fixedbv[32][16] fbvt;
 
 int main()
 {
-  fbvt f;
+  fbvt nondet_fbvt(void);
+  fbvt f = nondet_fbvt();
 
   // addition
   assert(100.0+10==110);

regression/cbmc/Fixedbv5/main.c

@@ -1,11 +1,12 @@
 int main()
 {
   typedef __CPROVER_fixedbv[32][16] ft;
-  ft a, b;
+  ft nondet_ft(void);
+  ft a = nondet_ft(), b;
 
-  __CPROVER_assume(a==1 || a==(ft)0.5 || a==2 || a==3 || a==(ft)0.25);
-  b=a;
-  a/=2;
-  a*=2;
-  __CPROVER_assert(a==b, "fixedbv div works");
+  __CPROVER_assume(a == 1 || a == (ft)0.5 || a == 2 || a == 3 || a == (ft)0.25);
+  b = a;
+  a /= 2;
+  a *= 2;
+  __CPROVER_assert(a == b, "fixedbv div works");
 }

regression/cbmc/Fixedbv6/main.c

@@ -23,7 +23,8 @@ int main()
   assert(!((fbvt)-2.0>=(fbvt)-1.0));
 
   // variables
-  fbvt a, b, _a=a, _b=b;
+  fbvt nondet_fbvt(void);
+  fbvt a = nondet_fbvt(), b = nondet_fbvt(), _a = a, _b = b;
   __CPROVER_assume(a==1 && b==2);
 
   assert(a!=b);

regression/cbmc/Float-equality1/main.c

@@ -2,7 +2,8 @@
 
 void main()
 {
-  double a, b, c;
+  double a = __VERIFIER_nondet_double(), b = __VERIFIER_nondet_double(),
+         c = __VERIFIER_nondet_double();
   __CPROVER_assume(a + b > c);
 #ifdef EQUALITY
   double x = a, y = b, z = c;

regression/cbmc/Float-equality2/main.c

@@ -3,8 +3,8 @@
 
 int main()
 {
-  float a;
-  float b;
+  float a = __VERIFIER_nondet_float();
+  float b = __VERIFIER_nondet_float();
   // We could do "if (isnormal(a) && isnormal(b))", but __CPROVER_isnanf(a+b)
   // will permit solving this entirely via the simplifier, if, and only if, the
   // equality is successfully simplified (despite the different order of

regression/cbmc/Float-flags-no-simp1/main.c

@@ -4,7 +4,7 @@
 
 int main()
 {
-  double d;
+  double d = __VERIFIER_nondet_double();
 
 #ifndef _MSC_VER
 

regression/cbmc/Float-flags-simp1/main.c

@@ -4,7 +4,7 @@
 
 int main()
 {
-  double d;
+  double d = __VERIFIER_nondet_double();
 
 #ifndef _MSC_VER
 

regression/cbmc/Float-no-simp2/main.c

@@ -1,6 +1,6 @@
 int main()
 {
-  double f, f2;
+  double f, f2 = __VERIFIER_nondet_double();
   // the following rely on f not being a NaN
   __CPROVER_assume(!__CPROVER_isnand(f2));
   __CPROVER_assume(__CPROVER_isfinited(f2));

regression/cbmc/Float-no-simp4/main.c

@@ -2,33 +2,33 @@
 
 int main()
 {
-  double d1, _d1;
+  double d1, _d1 = __VERIFIER_nondet_double();
   d1=_d1;
   __CPROVER_assume(__CPROVER_isnormald(d1));
   assert(!__CPROVER_isnand(d1));
   assert(!__CPROVER_isinfd(d1));
   assert(__CPROVER_isfinited(d1));
 
-  double d2, _d2;
+  double d2, _d2 = __VERIFIER_nondet_double();
   d2=_d2;
   __CPROVER_assume(__CPROVER_isinfd(d2));
   assert(!__CPROVER_isnormald(d2));
   assert(!__CPROVER_isnand(d2));
 
-  double d3, _d3;
+  double d3, _d3 = __VERIFIER_nondet_double();
   d3=_d3;
   __CPROVER_assume(__CPROVER_isnand(d3));
   assert(!__CPROVER_isnormald(d3));
   assert(!__CPROVER_isinfd(d3));
   assert(d3!=d3);
 
-  double d4, _d4;
+  double d4, _d4 = __VERIFIER_nondet_double();
   d4=_d4;
   __CPROVER_assume(__CPROVER_isfinited(d4));
   assert(!__CPROVER_isnand(d4));
   assert(!__CPROVER_isinfd(d4));
 
-  double d5, _d5;
+  double d5, _d5 = __VERIFIER_nondet_double();
   d5=_d5;
   __CPROVER_assume(!__CPROVER_isnand(d5) && !__CPROVER_isinfd(d5));
   assert(__CPROVER_isfinited(d5));

regression/cbmc/Float-no-simp5/main.c

@@ -1,6 +1,6 @@
 int main()
 {
-  double a, b;
+  double a = __VERIFIER_nondet_double(), b = __VERIFIER_nondet_double();
 
   union {
     double f;

regression/cbmc/Float-rounding2/main.c

@@ -6,7 +6,7 @@ int main()
   // examples of constants that previously exhibited wrong behaviour
   union U
   {
-    double d;
+    double d = __VERIFIER_nondet_double();
     uint64_t b;
   };
   union U u = {
@@ -15,7 +15,7 @@ int main()
     .b = 0b0000000000000000000000000000001111111111111111111111111000000000};
   double d = u.d;
 #else
-  double d;
+  double d = __VERIFIER_nondet_double();
 #endif
   float f;
   if(d > 0.0 && d < 1.0)

regression/cbmc/Float12/main.c

@@ -1,8 +1,8 @@
 int main()
 {
-  float f;
+  float f = __VERIFIER_nondet_float();
   double d;
-  unsigned char x;
+  unsigned char x = __VERIFIER_nondet_char();
 
   d=f;
 

regression/cbmc/Float20/main.c

@@ -42,13 +42,13 @@ void bugCasting (double d) {
 }
 
 int main (void) {
-  float f;
+  float f = __VERIFIER_nondet_float();
   bug(f);
 
-  float g;
+  float g = __VERIFIER_nondet_float();
   bugBrokenOut(g);
 
-  double d;
+  double d = __VERIFIER_nondet_double();
   bugCasting(d);
 
   return 1;