replace instances of to_unsigned_integer by numeric_cast

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1069,12 +1069,12 @@ 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");
-      targets.insert(target);
+      auto target = numeric_cast<unsigned>(to_constant_expr(i_it->args[0]));
+      DATA_INVARIANT(
+        target.has_value(), "target expected to be unsigned integer");
+      targets.insert(target.value());
 
-      a_entry.first->second.successors.push_back(target);
+      a_entry.first->second.successors.push_back(target.value());
 
       if(i_it->statement=="jsr" ||
          i_it->statement=="jsr_w")
@@ -1094,11 +1094,11 @@ 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");
-          targets.insert(target);
-          a_entry.first->second.successors.push_back(target);
+          auto target = numeric_cast<unsigned>(to_constant_expr(arg));
+          DATA_INVARIANT(
+            target.has_value(), "target expected to be unsigned integer");
+          targets.insert(target.value());
+          a_entry.first->second.successors.push_back(target.value());
         }
         is_label=!is_label;
       }

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -193,8 +193,9 @@ 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);
+    auto v = numeric_cast<unsigned>(to_constant_expr(arg));
+    CHECK_RETURN(v.has_value());
+    storeslotidx = v.value();
   }
   else
   {

src/solvers/refinement/string_constraint_generator_format.cpp

@@ -482,16 +482,18 @@ 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;
+    auto c = numeric_cast<unsigned>(to_constant_expr(arr.operands()[i]));
+    INVARIANT(c.has_value(), "constant should be convertible to unsigned");
+    out[i] = c.value();
   }
+
   return utf16_native_endian_to_java(out);
 }
 
@@ -520,12 +522,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