Merge pull request #3065 from diffblue/to_unsigned_integer

remove instances of to_unsigned_integer

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1069,9 +1069,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       PRECONDITION(!i_it->args.empty());
 
-      unsigned target;
-      bool ret=to_unsigned_integer(to_constant_expr(i_it->args[0]), target);
-      DATA_INVARIANT(!ret, "target expected to be unsigned integer");
+      auto target = numeric_cast_v<unsigned>(to_constant_expr(i_it->args[0]));
       targets.insert(target);
 
       a_entry.first->second.successors.push_back(target);
@@ -1094,9 +1092,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       {
         if(is_label)
         {
-          unsigned target;
-          bool ret=to_unsigned_integer(to_constant_expr(arg), target);
-          DATA_INVARIANT(!ret, "target expected to be unsigned integer");
+          auto target = numeric_cast_v<unsigned>(to_constant_expr(arg));
           targets.insert(target);
           a_entry.first->second.successors.push_back(target);
         }

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -193,8 +193,7 @@ static bool is_store_to_slot(
   {
     // Store with an argument:
     const auto &arg=inst.args[0];
-    bool ret=to_unsigned_integer(to_constant_expr(arg), storeslotidx);
-    CHECK_RETURN(!ret);
+    storeslotidx = numeric_cast_v<unsigned>(to_constant_expr(arg));
   }
   else
   {

src/solvers/refinement/string_constraint_generator_format.cpp

@@ -482,16 +482,14 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
 std::string
 utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
 {
+  for(const auto &op : arr.operands())
+    PRECONDITION(op.id() == ID_constant);
+
   std::wstring out(length, '?');
-  unsigned int c;
+
   for(std::size_t i=0; i<arr.operands().size() && i<length; i++)
-  {
-    PRECONDITION(arr.operands()[i].id()==ID_constant);
-    bool conversion_failed=to_unsigned_integer(
-      to_constant_expr(arr.operands()[i]), c);
-    INVARIANT(!conversion_failed, "constant should be convertible to unsigned");
-    out[i]=c;
-  }
+    out[i] = numeric_cast_v<unsigned>(to_constant_expr(arr.operands()[i]));
+
   return utf16_native_endian_to_java(out);
 }
 
@@ -520,12 +518,11 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
   const array_string_exprt res =
     char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
   const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
-  unsigned int length;
 
-  if(s1.length().id()==ID_constant &&
-     s1.content().id()==ID_array &&
-     !to_unsigned_integer(to_constant_expr(s1.length()), length))
+  if(s1.length().id() == ID_constant && s1.content().id() == ID_array)
   {
+    const auto length =
+      numeric_cast_v<std::size_t>(to_constant_expr(s1.length()));
     std::string s=utf16_constant_array_to_java(
       to_array_expr(s1.content()), length);
     // List of arguments after s

src/util/arith_tools.h

@@ -29,6 +29,7 @@ bool to_integer(const exprt &expr, mp_integer &int_value);
 bool to_integer(const constant_exprt &expr, mp_integer &int_value);
 
 // returns 'true' on error
+DEPRECATED("Use numeric_cast<unsigned>(e) instead")
 bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value);
 
 /// Numerical cast provides a unified way of converting from one numerical type