Add test covering size of two differently sized arrays

Author: thomasspriggs

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

@@ -0,0 +1,15 @@
+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.