From 443d4f0663fb6c3b8d8c7cdfd34255b6f6b6710d Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 7 Sep 2022 17:00:35 +0100
Subject: [PATCH 1/2] Add non-determinism to array_address_of test

This test is intended to cover incremental SMT decision procedure
support expressions of the form `address_of(array[0])`. These occur as
part of the conversion from array to pointer, which may be implicitly
introduced by applying `__CPROVER_OBJECT_SIZE` to an array. The existing
test is not actually checking this conversion due to it being simplified
away during constant propagation. The introduction of non-determinism in
this commit prevents constant propagation from removing expressions of
this form, so that their conversion will actually be tested.
---
 .../cbmc-incr-smt2/arrays/array_address_of.c      | 15 ++++++++++-----
 .../cbmc-incr-smt2/arrays/array_address_of.desc   |  4 +++-
 2 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/regression/cbmc-incr-smt2/arrays/array_address_of.c b/regression/cbmc-incr-smt2/arrays/array_address_of.c
index 91c0935edad..47ad2310f7a 100644
--- a/regression/cbmc-incr-smt2/arrays/array_address_of.c
+++ b/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");
 }
diff --git a/regression/cbmc-incr-smt2/arrays/array_address_of.desc b/regression/cbmc-incr-smt2/arrays/array_address_of.desc
index 61907cb03f6..6e5c016fdf5 100644
--- a/regression/cbmc-incr-smt2/arrays/array_address_of.desc
+++ b/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$

From 1b5fa34e9a015c67f2588d204eb1e896df0ddc9e Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Thu, 8 Sep 2022 14:15:50 +0100
Subject: [PATCH 2/2] Add test covering size of two differently sized arrays

---
 .../arrays/address_of_two_array_sizes.c       | 19 +++++++++++++++++++
 .../arrays/address_of_two_array_sizes.desc    | 17 +++++++++++++++++
 2 files changed, 36 insertions(+)
 create mode 100644 regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.c
 create mode 100644 regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.desc

diff --git a/regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.c b/regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.c
new file mode 100644
index 00000000000..642f8a7933a
--- /dev/null
+++ b/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");
+}
diff --git a/regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.desc b/regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.desc
new file mode 100644
index 00000000000..61ce18f498f
--- /dev/null
+++ b/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.