Merge pull request #7108 from thomasspriggs/tas/fix_address_of_zero_test

Add non-determinism to array_address_of test

Author: thomasspriggs

regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.c

@@ -0,0 +1,19 @@
+int main()
+{
+  int example_array1[10000];
+  char example_array2[20000];
+  void *foo;
+  __CPROVER_bool choice = nondet___CPROVER_bool();
+  if(choice)
+    foo = example_array1;
+  else
+    foo = example_array2;
+  __CPROVER_assert(
+    foo != example_array1 || __CPROVER_OBJECT_SIZE(foo) == 40000,
+    "Array condition 1");
+  __CPROVER_assert(__CPROVER_OBJECT_SIZE(foo) == 40000, "Array condition 2");
+  __CPROVER_assert(
+    foo != example_array2 || __CPROVER_OBJECT_SIZE(foo) == 20000,
+    "Array condition 3");
+  __CPROVER_assert(__CPROVER_OBJECT_SIZE(foo) == 20000, "Array condition 4");
+}

regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.desc

@@ -0,0 +1,17 @@
+CORE
+address_of_two_array_sizes.c
+--verbosity 10
+Passing problem to incremental SMT2 solving
+address_of\(main\:\:1\:\:example_array1\!0\@1\[0\]\)
+address_of\(main\:\:1\:\:example_array2\!0\@1\[0\]\)
+line \d+ Array condition 1: SUCCESS
+line \d+ Array condition 2: FAILURE
+line \d+ Array condition 3: SUCCESS
+line \d+ Array condition 4: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that __CPROVER_OBJECT_SIZE returns the expected results in the case where
+the pointer passed to it may point to one of 2 arrays, where each array has a
+different size.

regression/cbmc-incr-smt2/arrays/array_address_of.c

@@ -1,8 +1,13 @@
 int main()
 {
-  int example_array[10000];
-  __CPROVER_assert(
-    __CPROVER_OBJECT_SIZE(example_array) == 40000, "Array condition 1");
-  __CPROVER_assert(
-    __CPROVER_OBJECT_SIZE(example_array) == 40001, "Array condition 2");
+  int example_array1[10000];
+  int example_array2[10000];
+  int *foo;
+  int choice;
+  if(choice)
+    foo = example_array1;
+  else
+    foo = example_array2;
+  __CPROVER_assert(__CPROVER_OBJECT_SIZE(foo) == 40000, "Array condition 1");
+  __CPROVER_assert(__CPROVER_OBJECT_SIZE(foo) == 40001, "Array condition 2");
 }

regression/cbmc-incr-smt2/arrays/array_address_of.desc

@@ -1,7 +1,9 @@
 CORE
 array_address_of.c
-
+--verbosity 10
 Passing problem to incremental SMT2 solving
+address_of\(main\:\:1\:\:example_array1\!0\@1\[0\]\)
+address_of\(main\:\:1\:\:example_array2\!0\@1\[0\]\)
 line \d+ Array condition 1: SUCCESS
 line \d+ Array condition 2: FAILURE
 ^EXIT=10$