Use numeric_cast<mp_integer> instead of deprecated to_integer(exprt), part 2

This further reduces the number of warnings flagged, in particular in
Visual-Studio builds. Also turn tests of the size of ID_vector types being
constants into invariants as was already done in some places.

Author: tautschnig

jbmc/src/java_bytecode/expr2java.cpp

@@ -191,41 +191,33 @@ std::string expr2javat::convert_constant(
     std::string dest;
     dest.reserve(char_representation_length);
 
-    mp_integer int_value;
-    if(to_integer(src, int_value))
-      UNREACHABLE;
+    const wchar_t int_value = numeric_cast_v<wchar_t>(src);
 
     // Character literals in Java have type 'char', thus no cast is needed.
     // This is different from C, where charater literals have type 'int'.
-    dest += '\'' + utf16_native_endian_to_java(int_value.to_long()) + '\'';
+    dest += '\'' + utf16_native_endian_to_java(int_value) + '\'';
     return dest;
   }
   else if(src.type()==java_byte_type())
   {
     // No byte-literals in Java, so just cast:
-    mp_integer int_value;
-    if(to_integer(src, int_value))
-      UNREACHABLE;
+    const mp_integer int_value = numeric_cast_v<mp_integer>(src);
     std::string dest="(byte)";
     dest+=integer2string(int_value);
     return dest;
   }
   else if(src.type()==java_short_type())
   {
     // No short-literals in Java, so just cast:
-    mp_integer int_value;
-    if(to_integer(src, int_value))
-      UNREACHABLE;
+    const mp_integer int_value = numeric_cast_v<mp_integer>(src);
     std::string dest="(short)";
     dest+=integer2string(int_value);
     return dest;
   }
   else if(src.type()==java_long_type())
   {
     // long integer literals must have 'L' at the end
-    mp_integer int_value;
-    if(to_integer(src, int_value))
-      UNREACHABLE;
+    const mp_integer int_value = numeric_cast_v<mp_integer>(src);
     std::string dest=integer2string(int_value);
     dest+='L';
     return dest;

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -210,12 +210,8 @@ const exprt java_bytecode_convert_methodt::variable(
   size_t address,
   java_bytecode_convert_methodt::variable_cast_argumentt do_cast)
 {
-  mp_integer number;
-  bool ret=to_integer(to_constant_expr(arg), number);
-  CHECK_RETURN(!ret);
-
-  std::size_t number_int=integer2size_t(number);
   typet t=java_type_from_char(type_char);
+  const std::size_t number_int = numeric_cast_v<std::size_t>(arg);
   variablest &var_list=variables[number_int];
 
   // search variable in list for correct frame / address if necessary
@@ -1332,19 +1328,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="goto" || statement=="goto_w")
     {
       PRECONDITION(op.empty() && results.empty());
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg0), number);
-      INVARIANT(!ret, "goto argument should be an integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       code_gotot code_goto(label(integer2string(number)));
       c=code_goto;
     }
     else if(statement=="jsr" || statement=="jsr_w")
     {
       // As 'goto', except we must also push the subroutine return address:
       PRECONDITION(op.empty() && results.size() == 1);
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg0), number);
-      INVARIANT(!ret, "jsr argument should be an integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       code_gotot code_goto(label(integer2string(number)));
       c=code_goto;
       results[0]=
@@ -1386,9 +1378,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("if_?cmp??"))
     {
       PRECONDITION(op.size() == 2 && results.empty());
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg0), number);
-      INVARIANT(!ret, "if_?cmp?? argument should be an integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       c = convert_if_cmp(
         address_map, statement, op, number, i_it->source_location);
     }
@@ -1405,25 +1395,19 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       INVARIANT(!id.empty(), "unexpected bytecode-if");
       PRECONDITION(op.size() == 1 && results.empty());
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg0), number);
-      INVARIANT(!ret, "if?? argument should be an integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       c = convert_if(address_map, op, id, number, i_it->source_location);
     }
     else if(statement==patternt("ifnonnull"))
     {
       PRECONDITION(op.size() == 1 && results.empty());
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg0), number);
-      INVARIANT(!ret, "ifnonnull argument should be an integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       c = convert_ifnonull(address_map, op, number, i_it->source_location);
     }
     else if(statement==patternt("ifnull"))
     {
       PRECONDITION(op.size() == 1 && results.empty());
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg0), number);
-      INVARIANT(!ret, "ifnull argument should be an integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       c = convert_ifnull(address_map, op, number, i_it->source_location);
     }
     else if(statement=="iinc")
@@ -1620,10 +1604,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       // The first argument is the type, the second argument is the number of
       // dimensions.  The size of each dimension is on the stack.
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg1), number);
-      INVARIANT(!ret, "multianewarray argument should be an integer");
-      std::size_t dimension=integer2size_t(number);
+      const std::size_t dimension = numeric_cast_v<std::size_t>(arg1);
 
       op=pop(dimension);
       assert(results.size()==1);
@@ -1954,9 +1935,7 @@ codet java_bytecode_convert_methodt::convert_switch(
       code_switch_caset code_case;
       code_case.add_source_location() = location;
 
-      mp_integer number;
-      bool ret = to_integer(to_constant_expr(*a_it), number);
-      DATA_INVARIANT(!ret, "case label expected to be integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(*a_it);
       // The switch case does not contain any code, it just branches via a GOTO
       // to the jump target of the tableswitch/lookupswitch case at
       // hand. Therefore we consider this code to belong to the source bytecode
@@ -2074,9 +2053,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
     ieee_floatt value(spec);
     if(arg0.type().id() != ID_floatbv)
     {
-      mp_integer number;
-      bool ret = to_integer(to_constant_expr(arg0), number);
-      DATA_INVARIANT(!ret, "failed to convert constant");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       value.from_integer(number);
     }
     else
@@ -2086,9 +2063,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
   }
   else
   {
-    mp_integer value;
-    bool ret = to_integer(to_constant_expr(arg0), value);
-    DATA_INVARIANT(!ret, "failed to convert constant");
+    const mp_integer value = numeric_cast_v<mp_integer>(arg0);
     const typet type = java_type_from_char(statement[0]);
     results[0] = from_integer(value, type);
   }

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -90,9 +90,7 @@ refined_string_exprt make_refined_string_exprt(const array_string_exprt &arr)
 /// \return the corresponding index set
 std::set<exprt> full_index_set(const array_string_exprt &s)
 {
-  PRECONDITION(s.length().is_constant());
-  mp_integer n;
-  to_integer(s.length(), n);
+  const mp_integer n = numeric_cast_v<mp_integer>(s.length());
   std::set<exprt> ret;
   for(mp_integer i=0; i<n; ++i)
     ret.insert(from_integer(i));

src/analyses/goto_check.cpp

@@ -1110,13 +1110,9 @@ void goto_checkt::bounds_check(
     }
     else
     {
-      mp_integer i;
+      const auto i = numeric_cast<mp_integer>(index);
 
-      if(!to_integer(index, i) && i>=0)
-      {
-        // ok
-      }
-      else
+      if(!i.has_value() || *i < 0)
       {
         exprt effective_offset=ode.offset();
 

src/analyses/goto_rw.cpp

@@ -181,18 +181,15 @@ void rw_range_sett::get_objects_shift(
 
   range_spect src_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
 
-  mp_integer dist;
-  if(range_start==-1 ||
-     size==-1 ||
-     src_size==-1 ||
-     to_integer(simp_distance, dist))
+  const auto dist = numeric_cast<mp_integer>(simp_distance);
+  if(range_start == -1 || size == -1 || src_size == -1 || !dist.has_value())
   {
     get_objects_rec(mode, shift.op(), -1, -1);
     get_objects_rec(mode, shift.distance(), -1, -1);
   }
   else
   {
-    range_spect dist_r=to_range_spect(dist);
+    const range_spect dist_r = to_range_spect(*dist);
 
     // not sure whether to worry about
     // config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN
@@ -284,22 +281,17 @@ void rw_range_sett::get_objects_index(
 
   const exprt simp_index=simplify_expr(expr.index(), ns);
 
-  mp_integer index;
-  if(to_integer(simp_index, index))
-  {
+  const auto index = numeric_cast<mp_integer>(simp_index);
+  if(!index.has_value())
     get_objects_rec(get_modet::READ, expr.index());
-    index=-1;
-  }
 
-  if(range_start==-1 ||
-     sub_size==-1 ||
-     index==-1)
+  if(range_start == -1 || sub_size == -1 || !index.has_value())
     get_objects_rec(mode, expr.array(), -1, size);
   else
     get_objects_rec(
       mode,
       expr.array(),
-      range_start+to_range_spect(index*sub_size),
+      range_start + to_range_spect(*index * sub_size),
       size);
 }
 

src/analyses/interval_domain.cpp

@@ -252,8 +252,7 @@ void interval_domaint::assume_rec(
 
     if(is_int(lhs.type()) && is_int(rhs.type()))
     {
-      mp_integer tmp;
-      to_integer(rhs, tmp);
+      mp_integer tmp = numeric_cast_v<mp_integer>(rhs);
       if(id==ID_lt)
         --tmp;
       integer_intervalt &ii=int_map[lhs_identifier];
@@ -278,8 +277,7 @@ void interval_domaint::assume_rec(
 
     if(is_int(lhs.type()) && is_int(rhs.type()))
     {
-      mp_integer tmp;
-      to_integer(lhs, tmp);
+      mp_integer tmp = numeric_cast_v<mp_integer>(lhs);
       if(id==ID_lt)
         ++tmp;
       integer_intervalt &ii=int_map[rhs_identifier];

src/analyses/invariant_set.cpp

@@ -123,10 +123,9 @@ std::string inv_object_storet::build_string(const exprt &expr) const
       if(expr.get(ID_value)==ID_NULL)
         return "0";
 
-    mp_integer i;
-
-    if(!to_integer(expr, i))
-      return integer2string(i);
+    const auto i = numeric_cast<mp_integer>(expr);
+    if(i.has_value())
+      return integer2string(*i);
   }
 
   // we also like "address_of" and "reference_to"
@@ -455,25 +454,24 @@ void invariant_sett::strengthen_rec(const exprt &expr)
        get_object(expr.op1(), p.second))
       return;
 
-    mp_integer i0, i1;
-    bool have_i0=!to_integer(expr.op0(), i0);
-    bool have_i1=!to_integer(expr.op1(), i1);
+    const auto i0 = numeric_cast<mp_integer>(expr.op0());
+    const auto i1 = numeric_cast<mp_integer>(expr.op1());
 
     if(expr.id()==ID_le)
     {
-      if(have_i0)
-        add_bounds(p.second, lower_interval(i0));
-      else if(have_i1)
-        add_bounds(p.first, upper_interval(i1));
+      if(i0.has_value())
+        add_bounds(p.second, lower_interval(*i0));
+      else if(i1.has_value())
+        add_bounds(p.first, upper_interval(*i1));
       else
         add_le(p);
     }
     else if(expr.id()==ID_lt)
     {
-      if(have_i0)
-        add_bounds(p.second, lower_interval(i0+1));
-      else if(have_i1)
-        add_bounds(p.first, upper_interval(i1-1));
+      if(i0.has_value())
+        add_bounds(p.second, lower_interval(*i0 + 1));
+      else if(i1.has_value())
+        add_bounds(p.first, upper_interval(*i1 - 1));
       else
       {
         add_le(p);
@@ -553,12 +551,12 @@ void invariant_sett::strengthen_rec(const exprt &expr)
        get_object(expr.op1(), p.second))
       return;
 
-    mp_integer i;
-
-    if(!to_integer(expr.op0(), i))
-      add_bounds(p.second, boundst(i));
-    else if(!to_integer(expr.op1(), i))
-      add_bounds(p.first, boundst(i));
+    const auto i0 = numeric_cast<mp_integer>(expr.op0());
+    const auto i1 = numeric_cast<mp_integer>(expr.op1());
+    if(i0.has_value())
+      add_bounds(p.second, boundst(*i0));
+    else if(i1.has_value())
+      add_bounds(p.first, boundst(*i1));
 
     s=p;
     std::swap(s.first, s.second);
@@ -685,10 +683,10 @@ void invariant_sett::get_bounds(unsigned a, boundst &bounds) const
 
   {
     const exprt &e_a=object_store->get_expr(a);
-    mp_integer tmp;
-    if(!to_integer(e_a, tmp))
+    const auto tmp = numeric_cast<mp_integer>(e_a);
+    if(tmp.has_value())
     {
-      bounds=boundst(tmp);
+      bounds = boundst(*tmp);
       return;
     }
 
@@ -858,8 +856,7 @@ exprt invariant_sett::get_constant(const exprt &expr) const
 
         if(e.is_constant())
         {
-          mp_integer value;
-          assert(!to_integer(e, value));
+          mp_integer value = numeric_cast_v<mp_integer>(e);
 
           if(expr.type().id()==ID_pointer)
           {

src/ansi-c/expr2c.cpp

@@ -618,9 +618,7 @@ std::string expr2ct::convert_rec(
   {
     const vector_typet &vector_type=to_vector_type(src);
 
-    mp_integer size_int;
-    to_integer(vector_type.size(), size_int);
-
+    const mp_integer size_int = numeric_cast_v<mp_integer>(vector_type.size());
     std::string dest="__gcc_v"+integer2string(size_int);
 
     std::string tmp=convert(vector_type.subtype());

src/cpp/cpp_typecheck_initializer.cpp

@@ -225,10 +225,7 @@ void cpp_typecheckt::zero_initializer(
     if(size_expr.id()==ID_infinity)
       return; // don't initialize
 
-    mp_integer size;
-
-    bool to_int=to_integer(size_expr, size);
-    CHECK_RETURN(!to_int);
+    const mp_integer size = numeric_cast_v<mp_integer>(size_expr);
     CHECK_RETURN(size>=0);
 
     exprt::operandst empty_operands;

src/goto-programs/goto_trace.cpp

@@ -203,9 +203,9 @@ std::string trace_numeric_value(
     }
     else if(type.id()==ID_integer)
     {
-      mp_integer i;
-      if(!to_integer(expr, i) && i>=0)
-        return integer2string(i, 2);
+      const auto i = numeric_cast<mp_integer>(expr);
+      if(i.has_value() && *i >= 0)
+        return integer2string(*i, 2);
     }
   }
   else if(expr.id()==ID_array)