Introduce throwing bv_conversion expection

Remove suprisous namespace from bv_conversion_exceptions

Author: thk123

src/solvers/flattening/boolbv.cpp

@@ -152,6 +152,12 @@ bvt boolbvt::conversion_failed(const exprt &expr)
   return prop.new_variables(width);
 }
 
+/// TODO
+/// \param expr: TODO
+/// \return TODO
+/// \throws bitvector_conversion_exceptiont raised if converting byte_extraction
+/// goes wrong.
+/// TODO: extend for other types of conversion exception (diffblue/cbmc#2103).
 bvt boolbvt::convert_bitvector(const exprt &expr)
 {
   if(expr.type().id()==ID_bool)

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -11,10 +11,12 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/arith_tools.h>
-#include <util/std_expr.h>
 #include <util/byte_operators.h>
 #include <util/endianness_map.h>
+#include <util/std_expr.h>
 
+#include "bv_conversion_exceptions.h"
+#include "flatten_byte_extract_exceptions.h"
 #include "flatten_byte_operators.h"
 
 bvt map_bv(const endianness_mapt &map, const bvt &src)
@@ -42,8 +44,16 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   // if we extract from an unbounded array, call the flattening code
   if(is_unbounded_array(expr.op().type()))
   {
-    exprt tmp=flatten_byte_extract(expr, ns);
-    return convert_bv(tmp);
+    try
+    {
+      exprt tmp = flatten_byte_extract(expr, ns);
+      return convert_bv(tmp);
+    }
+    catch(const flatten_byte_extract_exceptiont &byte_extract_flatten_exception)
+    {
+      std::throw_with_nested(
+        bitvector_conversion_exceptiont("Can't convert byte_extraction", expr));
+    }
   }
 
   std::size_t width=boolbv_width(expr.type());

src/solvers/flattening/bv_conversion_exceptions.h

@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+Module: Bit vector conversion
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// \file
+/// Exceptions that can be raised in bv_conversion
+
+#ifndef CPROVER_SOLVERS_FLATTENING_BV_CONVERSION_EXCEPTIONS_H
+#define CPROVER_SOLVERS_FLATTENING_BV_CONVERSION_EXCEPTIONS_H
+
+#include <stdexcept>
+#include <string>
+
+#include <util/expr.h>
+
+class bitvector_conversion_exceptiont : public std::runtime_error
+{
+public:
+  bitvector_conversion_exceptiont(
+    const std::string &exception_message,
+    const exprt &bv_expr)
+    : runtime_error(exception_message), bv_expr(bv_expr)
+  {
+  }
+
+private:
+  exprt bv_expr;
+};
+
+#endif // CPROVER_SOLVERS_FLATTENING_BV_CONVERSION_EXCEPTIONS_H