Avoid invalid shift caused by excessive object bits

src/cprover/bv_pointers_wide.cpp

@@ -850,14 +850,16 @@ bvt bv_pointers_widet::add_addr(const exprt &expr)
 
   const pointer_typet type = pointer_type(expr.type());
   const std::size_t object_bits = get_object_width(type);
-  const std::size_t max_objects = std::size_t(1) << object_bits;
+  const mp_integer max_objects = power(2, object_bits);
 
-  if(a == max_objects)
+  if(a >= max_objects)
+  {
     throw analysis_exceptiont(
       "too many addressed objects: maximum number of objects is set to 2^n=" +
-      std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
+      integer2string(max_objects) + " (with n=" + std::to_string(object_bits) +
       "); " +
       "use the `--object-bits n` option to increase the maximum number");
+  }
 
   return encode(a, type);
 }

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -877,21 +877,24 @@ static smt_termt convert_expr_to_smt(
     "Objects should be tracked before converting their address to SMT terms");
   const std::size_t object_id = object->second.unique_id;
   const std::size_t object_bits = config.bv_encoding.object_bits;
-  const std::size_t max_objects = std::size_t(1) << object_bits;
+  const mp_integer max_objects = power(2, object_bits);
   if(object_id >= max_objects)
   {
     throw analysis_exceptiont{
       "too many addressed objects: maximum number of objects is set to 2^n=" +
-      std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
+      integer2string(max_objects) + " (with n=" + std::to_string(object_bits) +
       "); " +
       "use the `--object-bits n` option to increase the maximum number"};
   }
   const smt_termt object_bit_vector =
     smt_bit_vector_constant_termt{object_id, object_bits};
-  INVARIANT(
-    type->get_width() > object_bits,
-    "Pointer should be wider than object_bits in order to allow for offset "
-    "encoding.");
+  if(type->get_width() <= object_bits)
+  {
+    throw analysis_exceptiont{
+      "pointer width " + std::to_string(type->get_width()) +
+      " must be greater than object_bits (" + std::to_string(object_bits) +
+      ") to allow for offset encoding"};
+  }
   const size_t offset_bits = type->get_width() - object_bits;
   if(expr_try_dynamic_cast<symbol_exprt>(address_of.object()))
   {