Merge pull request #3096 from diffblue/hex-bitvectors

Daniel Kroening · web-flow · commit 35ee8759f0a1 · 2018-10-04T17:39:57.000+01:00
introduce integer2bv and bv2integer
diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
@@ -86,7 +86,7 @@ static const std::string get_thread_block_identifier(
 {
   PRECONDITION(f_code.arguments().size() == 1);
   const exprt &expr = f_code.arguments()[0];
-  mp_integer lbl_id = binary2integer(expr.op0().get_string(ID_value), false);
+  mp_integer lbl_id = bv2integer(expr.op0().get_string(ID_value), false);
   return integer2string(lbl_id);
 }
 
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -1813,7 +1813,7 @@ std::string expr2ct::convert_constant(
 
     bool is_signed=c_enum_type.subtype().id()==ID_signedbv;
 
-    mp_integer int_value=binary2integer(id2string(value), is_signed);
+    mp_integer int_value = bv2integer(id2string(value), is_signed);
     mp_integer i=0;
 
     irep_idt int_value_string=integer2string(int_value);
@@ -1849,8 +1849,8 @@ std::string expr2ct::convert_constant(
           type.id()==ID_c_bit_field ||
           type.id()==ID_c_bool)
   {
-    mp_integer int_value=
-      binary2integer(id2string(value), type.id()==ID_signedbv);
+    mp_integer int_value =
+      bv2integer(id2string(value), type.id() == ID_signedbv);
 
     const irep_idt &c_type=
       type.id()==ID_c_bit_field?type.subtype().get(ID_C_c_type):
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
@@ -566,7 +566,7 @@ int linker_script_merget::ls_data2instructions(
     symbol_exprt lhs(d["sym"].value, pointer_type(char_type()));
 
     constant_exprt rhs(
-      integer2binary(
+      integer2bv(
         string2integer(id2string(symbol_value)),
         unsigned_int_type().get_width()),
       unsigned_int_type());
@@ -632,8 +632,8 @@ int linker_script_merget::ls_data2instructions(
     symbol_exprt lhs(d["sym"].value, pointer_type(char_type()));
 
     constant_exprt rhs;
-    rhs.set_value(integer2binary(string2integer(d["val"].value),
-          unsigned_int_type().get_width()));
+    rhs.set_value(integer2bv(
+      string2integer(d["val"].value), unsigned_int_type().get_width()));
     rhs.type()=unsigned_int_type();
 
     exprt rhs_tc(rhs);
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
@@ -1834,8 +1834,8 @@ bool goto_convertt::get_string_constant(
       forall_operands(it, index_op)
         if(it->is_constant())
         {
-          unsigned long i=integer2ulong(
-            binary2integer(id2string(to_constant_expr(*it).get_value()), true));
+          unsigned long i = integer2ulong(
+            bv2integer(id2string(to_constant_expr(*it).get_value()), true));
 
           if(i!=0) // to skip terminating 0
             result+=static_cast<char>(i);
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
@@ -137,7 +137,7 @@ numeric_representation(const exprt &expr, const trace_optionst &options)
   if(options.hex_representation)
   {
     mp_integer value_int =
-      binary2integer(id2string(to_constant_expr(expr).get_value()), false);
+      bv2integer(id2string(to_constant_expr(expr).get_value()), false);
     result = integer2string(value_int, 16);
     prefix = "0x";
   }
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
@@ -382,7 +382,7 @@ void interpretert::evaluate(
     else if(expr.type().id()==ID_c_bool)
     {
       const irep_idt &value=to_constant_expr(expr).get_value();
-      dest.push_back(binary2integer(id2string(value), false));
+      dest.push_back(bv2integer(id2string(value), false));
       return;
     }
     else if(expr.type().id()==ID_bool)
@@ -981,16 +981,16 @@ void interpretert::evaluate(
       }
       else if(expr.type().id()==ID_signedbv)
       {
-        const std::string s=
-          integer2binary(value, to_signedbv_type(expr.type()).get_width());
-        dest.push_back(binary2integer(s, true));
+        const std::string s =
+          integer2bv(value, to_signedbv_type(expr.type()).get_width());
+        dest.push_back(bv2integer(s, true));
         return;
       }
       else if(expr.type().id()==ID_unsignedbv)
       {
-        const std::string s=
-          integer2binary(value, to_unsignedbv_type(expr.type()).get_width());
-        dest.push_back(binary2integer(s, false));
+        const std::string s =
+          integer2bv(value, to_unsignedbv_type(expr.type()).get_width());
+        dest.push_back(bv2integer(s, false));
         return;
       }
       else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
@@ -43,30 +43,30 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
   }
   else if(type_id==ID_unsignedbv)
   {
-    int_value=binary2integer(id2string(value), false);
+    int_value = bv2integer(id2string(value), false);
     return false;
   }
   else if(type_id==ID_signedbv)
   {
-    int_value=binary2integer(id2string(value), true);
+    int_value = bv2integer(id2string(value), true);
     return false;
   }
   else if(type_id==ID_c_bool)
   {
-    int_value=binary2integer(id2string(value), false);
+    int_value = bv2integer(id2string(value), false);
     return false;
   }
   else if(type_id==ID_c_enum)
   {
     const typet &subtype=to_c_enum_type(type).subtype();
     if(subtype.id()==ID_signedbv)
     {
-      int_value=binary2integer(id2string(value), true);
+      int_value = bv2integer(id2string(value), true);
       return false;
     }
     else if(subtype.id()==ID_unsignedbv)
     {
-      int_value=binary2integer(id2string(value), false);
+      int_value = bv2integer(id2string(value), false);
       return false;
     }
   }
@@ -75,12 +75,12 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
     const typet &subtype=type.subtype();
     if(subtype.id()==ID_signedbv)
     {
-      int_value=binary2integer(id2string(value), true);
+      int_value = bv2integer(id2string(value), true);
       return false;
     }
     else if(subtype.id()==ID_unsignedbv)
     {
-      int_value=binary2integer(id2string(value), false);
+      int_value = bv2integer(id2string(value), false);
       return false;
     }
   }
@@ -123,28 +123,28 @@ constant_exprt from_integer(
   else if(type_id==ID_unsignedbv)
   {
     std::size_t width=to_unsignedbv_type(type).get_width();
-    return constant_exprt(integer2binary(int_value, width), type);
+    return constant_exprt(integer2bv(int_value, width), type);
   }
   else if(type_id==ID_bv)
   {
     std::size_t width=to_bv_type(type).get_width();
-    return constant_exprt(integer2binary(int_value, width), type);
+    return constant_exprt(integer2bv(int_value, width), type);
   }
   else if(type_id==ID_signedbv)
   {
     std::size_t width=to_signedbv_type(type).get_width();
-    return constant_exprt(integer2binary(int_value, width), type);
+    return constant_exprt(integer2bv(int_value, width), type);
   }
   else if(type_id==ID_c_enum)
   {
     const std::size_t width =
       to_c_enum_type(type).subtype().get_size_t(ID_width);
-    return constant_exprt(integer2binary(int_value, width), type);
+    return constant_exprt(integer2bv(int_value, width), type);
   }
   else if(type_id==ID_c_bool)
   {
     std::size_t width=to_c_bool_type(type).get_width();
-    return constant_exprt(integer2binary(int_value, width), type);
+    return constant_exprt(integer2bv(int_value, width), type);
   }
   else if(type_id==ID_bool)
   {
@@ -162,7 +162,7 @@ constant_exprt from_integer(
   else if(type_id==ID_c_bit_field)
   {
     std::size_t width=to_c_bit_field_type(type).get_width();
-    return constant_exprt(integer2binary(int_value, width), type);
+    return constant_exprt(integer2bv(int_value, width), type);
   }
   else if(type_id==ID_fixedbv)
   {
diff --git a/src/util/bv_arithmetic.cpp b/src/util/bv_arithmetic.cpp
@@ -84,7 +84,7 @@ mp_integer bv_arithmetict::pack() const
 
 exprt bv_arithmetict::to_expr() const
 {
-  return constant_exprt(integer2binary(value, spec.width), spec.to_type());
+  return constant_exprt(integer2bv(value, spec.width), spec.to_type());
 }
 
 bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)
@@ -184,5 +184,5 @@ void bv_arithmetict::from_expr(const exprt &expr)
 {
   PRECONDITION(expr.is_constant());
   spec=bv_spect(expr.type());
-  value=binary2integer(expr.get_string(ID_value), spec.is_signed);
+  value = bv2integer(expr.get_string(ID_value), spec.is_signed);
 }
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
@@ -245,7 +245,7 @@ bool exprt::is_one() const
     }
     else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
     {
-      mp_integer int_value=binary2integer(value, false);
+      mp_integer int_value = bv2integer(value, false);
       if(int_value==1)
         return true;
     }
diff --git a/src/util/fixedbv.cpp b/src/util/fixedbv.cpp
@@ -26,7 +26,7 @@ fixedbvt::fixedbvt(const constant_exprt &expr)
 void fixedbvt::from_expr(const constant_exprt &expr)
 {
   spec=fixedbv_spect(to_fixedbv_type(expr.type()));
-  v=binary2integer(id2string(expr.get_value()), true);
+  v = bv2integer(id2string(expr.get_value()), true);
 }
 
 void fixedbvt::from_integer(const mp_integer &i)
@@ -46,7 +46,7 @@ constant_exprt fixedbvt::to_expr() const
   type.set_width(spec.width);
   type.set_integer_bits(spec.integer_bits);
   PRECONDITION(spec.width != 0);
-  return constant_exprt(integer2binary(v, spec.width), type);
+  return constant_exprt(integer2bv(v, spec.width), type);
 }
 
 void fixedbvt::round(const fixedbv_spect &dest_spec)
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
@@ -696,7 +696,7 @@ void ieee_floatt::divide_and_round(
 
 constant_exprt ieee_floatt::to_expr() const
 {
-  return constant_exprt(integer2binary(pack(), spec.width()), spec.to_type());
+  return constant_exprt(integer2bv(pack(), spec.width()), spec.to_type());
 }
 
 ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)
@@ -1062,7 +1062,7 @@ void ieee_floatt::change_spec(const ieee_float_spect &dest_spec)
 void ieee_floatt::from_expr(const constant_exprt &expr)
 {
   spec=ieee_float_spect(to_floatbv_type(expr.type()));
-  unpack(binary2integer(id2string(expr.get_value()), false));
+  unpack(bv2integer(id2string(expr.get_value()), false));
 }
 
 mp_integer ieee_floatt::to_integer() const
diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp
@@ -185,6 +185,18 @@ const mp_integer binary2integer(const std::string &n, bool is_signed)
   #endif
 }
 
+/// convert an integer to bit-vector representation with given width
+const std::string integer2bv(const mp_integer &src, std::size_t width)
+{
+  return integer2binary(src, width);
+}
+
+/// convert a bit-vector representation (possibly signed) to integer
+const mp_integer bv2integer(const std::string &src, bool is_signed)
+{
+  return binary2integer(src, is_signed);
+}
+
 mp_integer::ullong_t integer2ulong(const mp_integer &n)
 {
   PRECONDITION(n.is_ulong());
diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h
@@ -52,6 +52,12 @@ const mp_integer string2integer(const std::string &, unsigned base=10);
 const std::string integer2binary(const mp_integer &, std::size_t width);
 const mp_integer binary2integer(const std::string &, bool is_signed);
 
+/// convert an integer to bit-vector representation with given width
+const std::string integer2bv(const mp_integer &, std::size_t width);
+
+/// convert a bit-vector representation (possibly signed) to integer
+const mp_integer bv2integer(const std::string &, bool is_signed);
+
 /// \deprecated use numeric_cast_v<unsigned long long> instead
 DEPRECATED("Use numeric_cast_v<unsigned long long> instead")
 mp_integer::ullong_t integer2ulong(const mp_integer &);
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
@@ -677,7 +677,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
          expr_type_id==ID_signedbv ||
          expr_type_id==ID_floatbv)
       {
-        mp_integer int_value=binary2integer(id2string(value), false);
+        mp_integer int_value = bv2integer(id2string(value), false);
         expr=from_integer(int_value, expr_type);
         return false;
       }
@@ -832,8 +832,9 @@ bool simplify_exprt::simplify_if_implies(
       else if(type_id==ID_unsignedbv)
       {
         const mp_integer i1, i2;
-        if(binary2integer(cond.op1().get_string(ID_value), false)>=
-           binary2integer(expr.op1().get_string(ID_value), false))
+        if(
+          bv2integer(cond.op1().get_string(ID_value), false) >=
+          bv2integer(expr.op1().get_string(ID_value), false))
         {
           new_truth = true;
           return false;
@@ -842,8 +843,9 @@ bool simplify_exprt::simplify_if_implies(
       else if(type_id==ID_signedbv)
       {
         const mp_integer i1, i2;
-        if(binary2integer(cond.op1().get_string(ID_value), true)>=
-           binary2integer(expr.op1().get_string(ID_value), true))
+        if(
+          bv2integer(cond.op1().get_string(ID_value), true) >=
+          bv2integer(expr.op1().get_string(ID_value), true))
         {
           new_truth = true;
           return false;
@@ -868,8 +870,9 @@ bool simplify_exprt::simplify_if_implies(
       else if(type_id==ID_unsignedbv)
       {
         const mp_integer i1, i2;
-        if(binary2integer(cond.op1().get_string(ID_value), false)<=
-           binary2integer(expr.op1().get_string(ID_value), false))
+        if(
+          bv2integer(cond.op1().get_string(ID_value), false) <=
+          bv2integer(expr.op1().get_string(ID_value), false))
         {
           new_truth = true;
           return false;
@@ -878,8 +881,9 @@ bool simplify_exprt::simplify_if_implies(
       else if(type_id==ID_signedbv)
       {
         const mp_integer i1, i2;
-        if(binary2integer(cond.op1().get_string(ID_value), true)<=
-           binary2integer(expr.op1().get_string(ID_value), true))
+        if(
+          bv2integer(cond.op1().get_string(ID_value), true) <=
+          bv2integer(expr.op1().get_string(ID_value), true))
         {
           new_truth = true;
           return false;
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
@@ -821,7 +821,7 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
     }
     else if(expr.id()==ID_bitxor)
     {
-      constant_exprt new_op(integer2binary(0, width), expr.type());
+      constant_exprt new_op(integer2bv(0, width), expr.type());
       expr.swap(new_op);
       return false;
     }
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
@@ -387,7 +387,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
     else
     {
       // this is a pointer, we can't use to_integer
-      mp_integer number=binary2integer(id2string(c_ptr.get_value()), false);
+      mp_integer number = bv2integer(id2string(c_ptr.get_value()), false);
       // a null pointer would have been caught above, return value 0
       // will indicate that conversion failed
       if(number==0)

Original file line number	Diff line number	Diff line change
`@@ -86,7 +86,7 @@ static const std::string get_thread_block_identifier(`
`86`	`86`	`{`
`87`	`87`	`PRECONDITION(f_code.arguments().size() == 1);`
`88`	`88`	`const exprt &expr = f_code.arguments()[0];`
`89`		`- mp_integer lbl_id = binary2integer(expr.op0().get_string(ID_value), false);`
	`89`	`+ mp_integer lbl_id = bv2integer(expr.op0().get_string(ID_value), false);`
`90`	`90`	`return integer2string(lbl_id);`
`91`	`91`	`}`
`92`	`92`
Original file line number	Diff line number	Diff line change
`@@ -137,7 +137,7 @@ numeric_representation(const exprt &expr, const trace_optionst &options)`
`137`	`137`	`if(options.hex_representation)`
`138`	`138`	`{`
`139`	`139`	`mp_integer value_int =`
`140`		`- binary2integer(id2string(to_constant_expr(expr).get_value()), false);`
	`140`	`+ bv2integer(id2string(to_constant_expr(expr).get_value()), false);`
`141`	`141`	`result = integer2string(value_int, 16);`
`142`	`142`	`prefix = "0x";`
`143`	`143`	`}`
Original file line number	Diff line number	Diff line change
`@@ -382,7 +382,7 @@ void interpretert::evaluate(`
`382`	`382`	`else if(expr.type().id()==ID_c_bool)`
`383`	`383`	`{`
`384`	`384`	`const irep_idt &value=to_constant_expr(expr).get_value();`
`385`		`- dest.push_back(binary2integer(id2string(value), false));`
	`385`	`+ dest.push_back(bv2integer(id2string(value), false));`
`386`	`386`	`return;`
`387`	`387`	`}`
`388`	`388`	`else if(expr.type().id()==ID_bool)`
`@@ -981,16 +981,16 @@ void interpretert::evaluate(`
`981`	`981`	`}`
`982`	`982`	`else if(expr.type().id()==ID_signedbv)`
`983`	`983`	`{`
`984`		`- const std::string s=`
`985`		`- integer2binary(value, to_signedbv_type(expr.type()).get_width());`
`986`		`- dest.push_back(binary2integer(s, true));`
	`984`	`+ const std::string s =`
	`985`	`+ integer2bv(value, to_signedbv_type(expr.type()).get_width());`
	`986`	`+ dest.push_back(bv2integer(s, true));`
`987`	`987`	`return;`
`988`	`988`	`}`
`989`	`989`	`else if(expr.type().id()==ID_unsignedbv)`
`990`	`990`	`{`
`991`		`- const std::string s=`
`992`		`- integer2binary(value, to_unsignedbv_type(expr.type()).get_width());`
`993`		`- dest.push_back(binary2integer(s, false));`
	`991`	`+ const std::string s =`
	`992`	`+ integer2bv(value, to_unsignedbv_type(expr.type()).get_width());`
	`993`	`+ dest.push_back(bv2integer(s, false));`
`994`	`994`	`return;`
`995`	`995`	`}`
`996`	`996`	`else if((expr.type().id()==ID_bool) \|\| (expr.type().id()==ID_c_bool))`
Original file line number	Diff line number	Diff line change
`@@ -43,30 +43,30 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)`
`43`	`43`	`}`
`44`	`44`	`else if(type_id==ID_unsignedbv)`
`45`	`45`	`{`
`46`		`- int_value=binary2integer(id2string(value), false);`
	`46`	`+ int_value = bv2integer(id2string(value), false);`
`47`	`47`	`return false;`
`48`	`48`	`}`
`49`	`49`	`else if(type_id==ID_signedbv)`
`50`	`50`	`{`
`51`		`- int_value=binary2integer(id2string(value), true);`
	`51`	`+ int_value = bv2integer(id2string(value), true);`
`52`	`52`	`return false;`
`53`	`53`	`}`
`54`	`54`	`else if(type_id==ID_c_bool)`
`55`	`55`	`{`
`56`		`- int_value=binary2integer(id2string(value), false);`
	`56`	`+ int_value = bv2integer(id2string(value), false);`
`57`	`57`	`return false;`
`58`	`58`	`}`
`59`	`59`	`else if(type_id==ID_c_enum)`
`60`	`60`	`{`
`61`	`61`	`const typet &subtype=to_c_enum_type(type).subtype();`
`62`	`62`	`if(subtype.id()==ID_signedbv)`
`63`	`63`	`{`
`64`		`- int_value=binary2integer(id2string(value), true);`
	`64`	`+ int_value = bv2integer(id2string(value), true);`
`65`	`65`	`return false;`
`66`	`66`	`}`
`67`	`67`	`else if(subtype.id()==ID_unsignedbv)`
`68`	`68`	`{`
`69`		`- int_value=binary2integer(id2string(value), false);`
	`69`	`+ int_value = bv2integer(id2string(value), false);`
`70`	`70`	`return false;`
`71`	`71`	`}`
`72`	`72`	`}`
`@@ -75,12 +75,12 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)`
`75`	`75`	`const typet &subtype=type.subtype();`
`76`	`76`	`if(subtype.id()==ID_signedbv)`
`77`	`77`	`{`
`78`		`- int_value=binary2integer(id2string(value), true);`
	`78`	`+ int_value = bv2integer(id2string(value), true);`
`79`	`79`	`return false;`
`80`	`80`	`}`
`81`	`81`	`else if(subtype.id()==ID_unsignedbv)`
`82`	`82`	`{`
`83`		`- int_value=binary2integer(id2string(value), false);`
	`83`	`+ int_value = bv2integer(id2string(value), false);`
`84`	`84`	`return false;`
`85`	`85`	`}`
`86`	`86`	`}`
`@@ -123,28 +123,28 @@ constant_exprt from_integer(`
`123`	`123`	`else if(type_id==ID_unsignedbv)`
`124`	`124`	`{`
`125`	`125`	`std::size_t width=to_unsignedbv_type(type).get_width();`
`126`		`- return constant_exprt(integer2binary(int_value, width), type);`
	`126`	`+ return constant_exprt(integer2bv(int_value, width), type);`
`127`	`127`	`}`
`128`	`128`	`else if(type_id==ID_bv)`
`129`	`129`	`{`
`130`	`130`	`std::size_t width=to_bv_type(type).get_width();`
`131`		`- return constant_exprt(integer2binary(int_value, width), type);`
	`131`	`+ return constant_exprt(integer2bv(int_value, width), type);`
`132`	`132`	`}`
`133`	`133`	`else if(type_id==ID_signedbv)`
`134`	`134`	`{`
`135`	`135`	`std::size_t width=to_signedbv_type(type).get_width();`
`136`		`- return constant_exprt(integer2binary(int_value, width), type);`
	`136`	`+ return constant_exprt(integer2bv(int_value, width), type);`
`137`	`137`	`}`
`138`	`138`	`else if(type_id==ID_c_enum)`
`139`	`139`	`{`
`140`	`140`	`const std::size_t width =`
`141`	`141`	`to_c_enum_type(type).subtype().get_size_t(ID_width);`
`142`		`- return constant_exprt(integer2binary(int_value, width), type);`
	`142`	`+ return constant_exprt(integer2bv(int_value, width), type);`
`143`	`143`	`}`
`144`	`144`	`else if(type_id==ID_c_bool)`
`145`	`145`	`{`
`146`	`146`	`std::size_t width=to_c_bool_type(type).get_width();`
`147`		`- return constant_exprt(integer2binary(int_value, width), type);`
	`147`	`+ return constant_exprt(integer2bv(int_value, width), type);`
`148`	`148`	`}`
`149`	`149`	`else if(type_id==ID_bool)`
`150`	`150`	`{`
`@@ -162,7 +162,7 @@ constant_exprt from_integer(`
`162`	`162`	`else if(type_id==ID_c_bit_field)`
`163`	`163`	`{`
`164`	`164`	`std::size_t width=to_c_bit_field_type(type).get_width();`
`165`		`- return constant_exprt(integer2binary(int_value, width), type);`
	`165`	`+ return constant_exprt(integer2bv(int_value, width), type);`
`166`	`166`	`}`
`167`	`167`	`else if(type_id==ID_fixedbv)`
`168`	`168`	`{`
Original file line number	Diff line number	Diff line change
`@@ -84,7 +84,7 @@ mp_integer bv_arithmetict::pack() const`
`84`	`84`
`85`	`85`	`exprt bv_arithmetict::to_expr() const`
`86`	`86`	`{`
`87`		`- return constant_exprt(integer2binary(value, spec.width), spec.to_type());`
	`87`	`+ return constant_exprt(integer2bv(value, spec.width), spec.to_type());`
`88`	`88`	`}`
`89`	`89`
`90`	`90`	`bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)`
`@@ -184,5 +184,5 @@ void bv_arithmetict::from_expr(const exprt &expr)`
`184`	`184`	`{`
`185`	`185`	`PRECONDITION(expr.is_constant());`
`186`	`186`	`spec=bv_spect(expr.type());`
`187`		`- value=binary2integer(expr.get_string(ID_value), spec.is_signed);`
	`187`	`+ value = bv2integer(expr.get_string(ID_value), spec.is_signed);`
`188`	`188`	`}`
Original file line number	Diff line number	Diff line change
`@@ -245,7 +245,7 @@ bool exprt::is_one() const`
`245`	`245`	`}`
`246`	`246`	`else if(type_id==ID_unsignedbv \|\| type_id==ID_signedbv)`
`247`	`247`	`{`
`248`		`- mp_integer int_value=binary2integer(value, false);`
	`248`	`+ mp_integer int_value = bv2integer(value, false);`
`249`	`249`	`if(int_value==1)`
`250`	`250`	`return true;`
`251`	`251`	`}`
Original file line number	Diff line number	Diff line change
`@@ -26,7 +26,7 @@ fixedbvt::fixedbvt(const constant_exprt &expr)`
`26`	`26`	`void fixedbvt::from_expr(const constant_exprt &expr)`
`27`	`27`	`{`
`28`	`28`	`spec=fixedbv_spect(to_fixedbv_type(expr.type()));`
`29`		`- v=binary2integer(id2string(expr.get_value()), true);`
	`29`	`+ v = bv2integer(id2string(expr.get_value()), true);`
`30`	`30`	`}`
`31`	`31`
`32`	`32`	`void fixedbvt::from_integer(const mp_integer &i)`
`@@ -46,7 +46,7 @@ constant_exprt fixedbvt::to_expr() const`
`46`	`46`	`type.set_width(spec.width);`
`47`	`47`	`type.set_integer_bits(spec.integer_bits);`
`48`	`48`	`PRECONDITION(spec.width != 0);`
`49`		`- return constant_exprt(integer2binary(v, spec.width), type);`
	`49`	`+ return constant_exprt(integer2bv(v, spec.width), type);`
`50`	`50`	`}`
`51`	`51`
`52`	`52`	`void fixedbvt::round(const fixedbv_spect &dest_spec)`