Fix bounds checking for structs with flexible array members

The constraints did not make sure that the dynamic size (__CPROVER_malloc_size)
actually referred to the object we are looking at (__CPROVER_malloc_object).

Author: tautschnig

regression/cbmc/struct12/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct S
+{
+  int a;
+  char b[];
+};
+
+int main()
+{
+  struct S *s = malloc(sizeof(struct S) + 1);
+  // allocate an object that matches the fixed size of the struct, without the
+  // flexible member
+  int *p = malloc(sizeof(int));
+  s->b[0] = 0;
+  assert(s->b[0] == 0);
+}

regression/cbmc/struct12/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Our logic for constructing assertion over structs with flexible array members
+was wrong, because it could conflate dynamic allocation sizes across different
+objects.

src/analyses/goto_check.cpp

@@ -1333,8 +1333,17 @@ void goto_checkt::bounds_check(
     auto type_size_opt = size_of_expr(ode.root_object().type(), ns);
 
     if(type_size_opt.has_value())
-      type_matches_size =
-        equal_exprt(size, typecast_exprt(type_size_opt.value(), size.type()));
+    {
+      type_matches_size = if_exprt{
+        dynamic_object(pointer),
+        and_exprt{malloc_object(pointer, ns),
+                  equal_exprt{typecast_exprt::conditional_cast(
+                                dynamic_size(ns), type_size_opt->type()),
+                              *type_size_opt}},
+        equal_exprt{typecast_exprt::conditional_cast(
+                      object_size(pointer), type_size_opt->type()),
+                    *type_size_opt}};
+    }
   }
 
   const exprt &size=array_type.id()==ID_array ?