Merge pull request #7879 from esteffin/esteffin/fix-shadow-memory-regressions

Fix many shadow memory regressions

Author: Enrico Steffinlongo

regression/cbmc-shadow-memory/constchar-param1/test.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 main.c
 --unwind 11
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-^Generated 11 VCC\(s\), 0 remaining after simplification$
+^Generated \d+ VCC\(s\), 0 remaining after simplification$
 --
 ^warning: ignoring

regression/cbmc-shadow-memory/global1/main.c

@@ -155,7 +155,7 @@ void dynamically_allocated_structs()
   assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 2);
   assert(__CPROVER_get_field(&(p->B1[2]), "field1") == 0);
 
-  q = &(p->B1[2]);
+  int *q = &(p->B1[2]);
   assert(__CPROVER_get_field(q, "field1") == 0);
   __CPROVER_set_field(q, "field1", 7);
   assert(__CPROVER_get_field(q, "field1") == 7);
@@ -187,7 +187,7 @@ void arrays_of_structs_and_pointers_into_them()
   assert(__CPROVER_get_field(&(n[1].B1[1]), "field2") == 3);
   assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 4);
 
-  q = &(n[1].x1);
+  int *q = &(n[1].x1);
   assert(__CPROVER_get_field(q, "field1") == 1);
   __CPROVER_set_field(q, "field1", 5);
   assert(__CPROVER_get_field(q, "field1") == 5);
@@ -197,6 +197,8 @@ void arrays_of_structs_and_pointers_into_them()
   __CPROVER_set_field(q, "field2", 6);
   assert(__CPROVER_get_field(q, "field2") == 6);
 
+  int k;
+  __CPROVER_assume(0 <= k && k < 3);
   int x;
   __CPROVER_assume(0 <= x && x < 3);
   __CPROVER_set_field(&(n[k].B1[x]), "field1", 46);
@@ -226,7 +228,7 @@ void dynamically_allocated_arrays_of_structs()
   assert(__CPROVER_get_field(&(u[1].B1[1]), "field2") == 3);
   assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 4);
 
-  q = &(u[1].x1);
+  int *q = &(u[1].x1);
   assert(__CPROVER_get_field(q, "field1") == 1);
   __CPROVER_set_field(q, "field1", 5);
   assert(__CPROVER_get_field(q, "field1") == 5);
@@ -236,6 +238,8 @@ void dynamically_allocated_arrays_of_structs()
   __CPROVER_set_field(q, "field2", 6);
   assert(__CPROVER_get_field(q, "field2") == 6);
 
+  int k;
+  __CPROVER_assume(0 <= k && k < 3);
   int t;
   __CPROVER_assume(0 <= t && t < 3);
   __CPROVER_set_field(&(u[k].B1[t]), "field1", 46);

regression/cbmc-shadow-memory/global1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc-shadow-memory/local1/main.c

@@ -53,7 +53,7 @@ void arrays_and_pointers_into_arrays()
 {
   int A[5];
 
-  z = &(A[4]);
+  int *z = &(A[4]);
 
   assert(__CPROVER_get_field(z, "field1") == 0);
   assert(__CPROVER_get_field(z, "field2") == 0);
@@ -111,7 +111,7 @@ void structs_and_pointers_into_structs()
   __CPROVER_set_field(&(m.B1[j]), "field1", 44);
   assert(__CPROVER_get_field(&(m.B1[j]), "field1") == 44);
 
-  z = &(m.B1[j]);
+  int *z = &(m.B1[j]);
   __CPROVER_set_field(z, "field1", 45);
   assert(__CPROVER_get_field(z, "field1") == 45);
 }
@@ -123,7 +123,7 @@ void arrays_of_structs_and_pointers_into_them()
   assert(__CPROVER_get_field(&(n[1].x1), "field1") == 0);
   assert(__CPROVER_get_field(&(n[1].B1[1]), "field2") == 0);
 
-  p = &(n[2]);
+  struct STRUCTNAME *p = &(n[2]);
 
   __CPROVER_set_field(&(n[1].x1), "field1", 1);
   __CPROVER_set_field(&(p->x1), "field1", 2);
@@ -135,7 +135,7 @@ void arrays_of_structs_and_pointers_into_them()
   assert(__CPROVER_get_field(&(n[1].B1[1]), "field2") == 3);
   assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 4);
 
-  q = &(n[1].x1);
+  int *q = &(n[1].x1);
   assert(__CPROVER_get_field(q, "field1") == 1);
   __CPROVER_set_field(q, "field1", 5);
   assert(__CPROVER_get_field(q, "field1") == 5);
@@ -147,10 +147,12 @@ void arrays_of_structs_and_pointers_into_them()
 
   int k;
   __CPROVER_assume(0 <= k && k < 3);
+  int j;
+  __CPROVER_assume(0 <= j && j < 3);
   __CPROVER_set_field(&(n[k].B1[j]), "field1", 46);
   assert(__CPROVER_get_field(&(n[k].B1[j]), "field1") == 46);
 
-  z = &(n[k].B1[j]);
+  int *z = &(n[k].B1[j]);
   __CPROVER_set_field(z, "field1", 47);
   assert(__CPROVER_get_field(z, "field1") == 47);
 }

regression/cbmc-shadow-memory/local1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc-shadow-memory/param1/main.c

@@ -103,7 +103,7 @@ void f_int_local(int rec, int value)
 
 int main()
 {
-  __CPROVER_field_decl_local("field1", (char)0);
+  __CPROVER_field_decl_local("field1", (unsigned char)0);
   int x;
   __CPROVER_set_field(&x, "field1", 255);
   f_int_val(x);

regression/cbmc-shadow-memory/param1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc-shadow-memory/var-assign1/main.c

@@ -2,9 +2,9 @@
 
 int main()
 {
-  __CPROVER_field_decl_local("field", (_Bool)0);
+  __CPROVER_field_decl_local("field", (char)0);
 
-  _Bool z;
+  char z;
   int x;
   __CPROVER_set_field(&x, "field", z);
   assert(__CPROVER_get_field(&x, "field") == z);

regression/cbmc-shadow-memory/var-assign1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$