Separate the parsing of object-bits

So that the parsing can be kept with the data structure. So the length
of `configt::set` can be marginally reduced. So that this functionality
can be documented.

Author: thomasspriggs

src/util/Makefile

@@ -4,6 +4,7 @@ SRC = allocate_objects.cpp \
       array_name.cpp \
       base_type.cpp \
       bv_arithmetic.cpp \
+      bv_encoding.cpp \
       byte_operators.cpp \
       c_types.cpp \
       cmdline.cpp \

src/util/bv_encoding.cpp

@@ -0,0 +1,31 @@
+/*******************************************************************\
+
+Module: bv_encoding configuration
+
+Author: Diffblue Ltd
+
+\*******************************************************************/
+
+#include "bv_encoding.h"
+
+#include "exception_utils.h"
+#include "string2int.h"
+
+bv_encodingt parse_object_bits_encoding(
+  const std::string &argument,
+  const std::size_t pointer_width)
+{
+  const unsigned int object_bits = unsafe_string2unsigned(argument);
+  if(object_bits <= 0 || object_bits >= pointer_width)
+  {
+    throw invalid_command_line_argument_exceptiont(
+      "object-bits must be positive and less than the pointer width (" +
+        std::to_string(pointer_width) + ") ",
+      "--object_bits");
+  }
+
+  bv_encodingt bv_encoding;
+  bv_encoding.object_bits = object_bits;
+  bv_encoding.is_object_bits_default = false;
+  return bv_encoding;
+}

src/util/bv_encoding.h

@@ -10,6 +10,7 @@ Author: Diffblue Ltd
 #define CPROVER_UTIL_BV_ENCODING_H
 
 #include <cstddef>
+#include <string>
 
 struct bv_encodingt final
 {
@@ -18,4 +19,15 @@ struct bv_encodingt final
   bool is_object_bits_default = true;
 };
 
+/// \brief Parses the `object_bits` argument from the command line arguments.
+/// \param argument The command line argument to parse the `object_bits` from.
+/// \param pointer_width The width of a pointer in bits. This is used to check
+///   the value of object_bits is within the valid range.
+/// \return A `bv_encodingt` on successful parsing. In the case where an invalid
+///    argument is specified, an `invalid_command_line_argument_exceptiont` will
+///    be thrown.
+bv_encodingt parse_object_bits_encoding(
+  const std::string &argument,
+  const std::size_t pointer_width);
+
 #endif // CPROVER_UTIL_BV_ENCODING_H

src/util/config.cpp

@@ -1074,19 +1074,8 @@ bool configt::set(const cmdlinet &cmdline)
 
   if(cmdline.isset("object-bits"))
   {
-    bv_encoding.object_bits=
-      unsafe_string2unsigned(cmdline.get_value("object-bits"));
-
-    if(!(0<bv_encoding.object_bits &&
-         bv_encoding.object_bits<ansi_c.pointer_width))
-    {
-      throw invalid_command_line_argument_exceptiont(
-        "object-bits must be positive and less than the pointer width (" +
-          std::to_string(ansi_c.pointer_width) + ") ",
-        "--object_bits");
-    }
-
-    bv_encoding.is_object_bits_default = false;
+    bv_encoding = parse_object_bits_encoding(
+      cmdline.get_value("object-bits"), ansi_c.pointer_width);
   }
 
   if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null"))