Merge pull request #8514 from diffblue/format-expr-bv

Format bit-vectors with `[` ... `]` vector notation

Author: kroening

src/util/format_expr.cpp

@@ -190,13 +190,16 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
   {
     // These do not have a numerical interpretation.
     // We'll print the 0/1 bit pattern, starting with the bit
-    // that has the highest index.
+    // that has the highest index. We use vector notation
+    // [...] to avoid confusion with decimal numbers.
     auto width = to_bv_type(src.type()).get_width();
     std::string result;
-    result.reserve(width);
+    result.reserve(width + 2);
     auto &value = src.get_value();
+    result += '[';
     for(std::size_t i = 0; i < width; i++)
       result += get_bvrep_bit(value, width, width - i - 1) ? '1' : '0';
+    result += ']';
     return os << result;
   }
   else if(type == ID_integer || type == ID_natural || type == ID_range)

unit/util/format_expr.cpp

@@ -30,5 +30,5 @@ 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");
+  REQUIRE(format_to_string(expr) == "[1011]");
 }