Add regression test of object size with incremental SMT solving

Author: thomasspriggs

regression/cbmc-incr-smt2/pointers/object_size.c

@@ -0,0 +1,17 @@
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdint.h>
+
+int main()
+{
+  uint16_t x;
+  uint32_t y;
+  bool nondet_bool1;
+  void *ptr = nondet_bool1 ? (&x) : (&y);
+  size_t size = __CPROVER_OBJECT_SIZE(ptr);
+  __CPROVER_assert(size == 2 || size == 4, "Expected int sizes.");
+  __CPROVER_assert(size == 2, "Size is always 2. (Can be disproved.)");
+  __CPROVER_assert(size == 4, "Size is always 4. (Can be disproved.)");
+  size_t null_size = __CPROVER_OBJECT_SIZE(NULL);
+  __CPROVER_assert(null_size == 254, "Size of NULL.");
+}

regression/cbmc-incr-smt2/pointers/object_size.desc

@@ -0,0 +1,17 @@
+CORE
+object_size.c
+--trace
+line 12 Expected int sizes\.: SUCCESS
+line 13 Size is always 2\. \(Can be disproved\.\): FAILURE
+line 14 Size is always 4\. \(Can be disproved\.\): FAILURE
+line 16 Size of NULL\.: FAILURE
+size=2ul
+size=4ul
+null_size=0ul
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that the model of object_size can take only the expected values in the case
+where the pointer it is given may point to one of two objects. Test that the
+size of the null object is zero.