bitvector_typet: set width from mp_integer

This adds C-style getter/setter methods to bitvector_typet for the width of
the vector.

The setter takes an mp_integer, which checks that the width fits within
std::size_t.  This removes the burden of performing this check from the
caller, and allows callers to avoid potential arithmetic overflows by using
mp_integer.

Author: kroening

src/ansi-c/c_typecheck_type.cpp

@@ -1496,7 +1496,7 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
         << "bit field width is negative";
     }
 
-    type.set_width(numeric_cast_v<std::size_t>(i));
+    type.width(i);
     type.remove(ID_size);
   }
 

src/util/std_types.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "std_types.h"
 
+#include "arith_tools.h"
 #include "c_types.h"
 #include "namespace.h"
 #include "std_expr.h"
@@ -154,6 +155,16 @@ bool is_rvalue_reference(const typet &type)
          type.get_bool(ID_C_rvalue_reference);
 }
 
+std::size_t bitvector_typet::width() const
+{
+  return get_size_t(ID_width);
+}
+
+void bitvector_typet::width(const mp_integer &width)
+{
+  set_width(numeric_cast_v<std::size_t>(width));
+}
+
 void range_typet::set_from(const mp_integer &from)
 {
   set(ID_from, integer2string(from));

src/util/std_types.h

@@ -917,16 +917,25 @@ class bitvector_typet : public typet
     set_width(width);
   }
 
+  bitvector_typet(const irep_idt &_id, mp_integer _width) : typet(_id)
+  {
+    width(_width);
+  }
+
   std::size_t get_width() const
   {
     return get_size_t(ID_width);
   }
 
+  std::size_t width() const;
+
   void set_width(std::size_t width)
   {
     set_size_t(ID_width, width);
   }
 
+  void width(const mp_integer &);
+
   static void check(
     const typet &type,
     const validation_modet vm = validation_modet::INVARIANT)