format_expr now prints bv-typed constants

This adds formatting for bv-type constants to format_expr.  As the bv type
does not have a numerical representation, the 0/1 bit pattern is printed,
starting with the bit with the highest index.

Author: kroening

src/util/format_expr.cpp

@@ -186,6 +186,19 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
     type == ID_unsignedbv || type == ID_signedbv || type == ID_c_bool ||
     type == ID_c_bit_field)
     return os << *numeric_cast<mp_integer>(src);
+  else if(type == ID_bv)
+  {
+    // These do not have a numerical interpretation.
+    // We'll print the 0/1 bit pattern, starting with the bit
+    // that has the highest index.
+    auto width = to_bv_type(src.type()).get_width();
+    std::string result;
+    result.reserve(width);
+    auto &value = src.get_value();
+    for(std::size_t i = 0; i < width; i++)
+      result += get_bvrep_bit(value, width, width - i - 1) ? '1' : '0';
+    return os << result;
+  }
   else if(type == ID_integer || type == ID_natural || type == ID_range)
     return os << src.get_value();
   else if(type == ID_string)

unit/util/format_expr.cpp

@@ -6,8 +6,10 @@
 
 \*******************************************************************/
 
-#include <util/expr.h>
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/format_expr.h>
+#include <util/std_expr.h>
 
 #include <testing-utils/use_catch.h>
 
@@ -23,3 +25,10 @@ TEST_CASE(
     });
   REQUIRE(format_to_string(exprt{custom_id}) == "output");
 }
+
+TEST_CASE("Format a bv-typed constant", "[core][util][format_expr]")
+{
+  auto value = make_bvrep(4, [](std::size_t index) { return index != 2; });
+  auto expr = constant_exprt{value, bv_typet{4}};
+  REQUIRE(format_to_string(expr) == "1011");
+}