Check static array bounds of dynamic objects

Previously checking against malloc bounds and against statically-bounded arrays (e.g. int[2]) were mutually exclusive. This enables the static array bounds check even for dynamic objects.

Fixes diffblue#239.

Author: smowton

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -3,7 +3,7 @@ main.c
 --bounds-check --32
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILURE$
-^\*\* 1 of 9 failed (2 iterations)$
+array\.List dynamic object upper bound in p->List\[2\]: FAILURE
+\*\* 1 of 11 failed (2 iterations)
 --
 ^warning: ignoring

src/analyses/goto_check.cpp

@@ -1193,6 +1193,8 @@ void goto_checkt::bounds_check(
     }
   }
 
+  exprt type_matches_size=true_exprt();
+
   if(ode.root_object().id()==ID_dereference)
   {
     const exprt &pointer=
@@ -1218,13 +1220,18 @@ void goto_checkt::bounds_check(
 
     add_guarded_claim(
       precond,
-      name+" upper bound",
+      name+" dynamic object upper bound",
       "array bounds",
       expr.find_source_location(),
       expr,
       guard);
 
-    return;
+    exprt type_size=size_of_expr(ode.root_object().type(), ns);
+    if(type_size.is_not_nil())
+      type_matches_size=
+        equal_exprt(
+          size,
+          typecast_exprt(type_size, size.type()));
   }
 
   const exprt &size=array_type.id()==ID_array ?
@@ -1257,7 +1264,7 @@ void goto_checkt::bounds_check(
       inequality.op1().make_typecast(inequality.op0().type());
 
     add_guarded_claim(
-      inequality,
+      implies_exprt(type_matches_size, inequality),
       name+" upper bound",
       "array bounds",
       expr.find_source_location(),