Merge pull request #3252 from tautschnig/vs-no-to_integer

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

Author: kroening

src/ansi-c/padding.cpp

@@ -35,12 +35,15 @@ mp_integer alignment(const typet &type, const namespacet &ns)
   const exprt &given_alignment=
     static_cast<const exprt &>(type.find(ID_C_alignment));
 
-  mp_integer a_int;
+  mp_integer a_int = 0;
 
   // we trust it blindly, no matter how nonsensical
-  if(given_alignment.is_nil() ||
-     to_integer(given_alignment, a_int))
-    a_int=0;
+  if(given_alignment.is_not_nil())
+  {
+    const auto a = numeric_cast<mp_integer>(given_alignment);
+    if(a.has_value())
+      a_int = *a;
+  }
 
   // alignment but no packing
   if(a_int>0 && !type.get_bool(ID_C_packed))
@@ -402,17 +405,16 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
   }
 
   // any explicit alignment for the struct?
-  if(type.find(ID_C_alignment).is_not_nil())
+  const exprt &alignment =
+    static_cast<const exprt &>(type.find(ID_C_alignment));
+  if(alignment.is_not_nil())
   {
-    const exprt &alignment=
-      static_cast<const exprt &>(type.find(ID_C_alignment));
     if(alignment.id()!=ID_default)
     {
-      exprt tmp=alignment;
-      simplify(tmp, ns);
-      mp_integer tmp_i;
-      if(!to_integer(tmp, tmp_i) && tmp_i>max_alignment)
-        max_alignment=tmp_i;
+      const auto tmp_i = numeric_cast<mp_integer>(simplify_expr(alignment, ns));
+
+      if(tmp_i.has_value() && *tmp_i > max_alignment)
+        max_alignment = *tmp_i;
     }
   }
   // Is the struct packed, without any alignment specification?

src/ansi-c/type2name.cpp

@@ -178,14 +178,19 @@ static std::string type2name(
   }
   else if(type.id()==ID_array)
   {
-    const array_typet &t=to_array_type(type);
-    mp_integer size;
-    if(t.size().id()==ID_symbol)
-      result += "ARR" + id2string(to_symbol_expr(t.size()).get_identifier());
-    else if(to_integer(t.size(), size))
-      result+="ARR?";
+    const exprt &size = to_array_type(type).size();
+
+    if(size.id() == ID_symbol)
+      result += "ARR" + id2string(to_symbol_expr(size).get_identifier());
     else
-      result+="ARR"+integer2string(size);
+    {
+      const auto size_int = numeric_cast<mp_integer>(size);
+
+      if(!size_int.has_value())
+        result += "ARR?";
+      else
+        result += "ARR" + integer2string(*size_int);
+    }
   }
   else if(
     type.id() == ID_symbol_type || type.id() == ID_c_enum_tag ||

src/cpp/cpp_typecheck_constructor.cpp

@@ -395,13 +395,11 @@ void cpp_typecheckt::default_assignop_value(
         continue;
       }
 
-      mp_integer size;
-      bool to_int=to_integer(size_expr, size);
-      CHECK_RETURN(!to_int);
-      CHECK_RETURN(size>=0);
+      const auto size = numeric_cast<mp_integer>(size_expr);
+      CHECK_RETURN(!size.has_value());
+      CHECK_RETURN(*size >= 0);
 
-      exprt::operandst empty_operands;
-      for(mp_integer i=0; i < size; ++i)
+      for(mp_integer i = 0; i < *size; ++i)
         copy_array(source_location, mem_name, i, arg_name, block);
     }
     else

src/goto-symex/build_goto_trace.cpp

@@ -228,7 +228,11 @@ void build_goto_trace(
         exprt clock_value=prop_conv.get(
           symbol_exprt(partial_order_concurrencyt::rw_clock_id(it)));
 
-        to_integer(clock_value, current_time);
+        const auto cv = numeric_cast<mp_integer>(clock_value);
+        if(cv.has_value())
+          current_time = *cv;
+        else
+          current_time = 0;
       }
       else if(it->is_atomic_end() && current_time<0)
         current_time*=-1;

src/solvers/flattening/boolbv.cpp

@@ -323,17 +323,17 @@ bvt boolbvt::convert_lambda(const exprt &expr)
   const exprt &array_size=
     to_array_type(expr.type()).size();
 
-  mp_integer size;
+  const auto size = numeric_cast<mp_integer>(array_size);
 
-  if(to_integer(array_size, size))
+  if(!size.has_value())
     return conversion_failed(expr);
 
   typet counter_type=expr.op0().type();
 
   bvt bv;
   bv.resize(width);
 
-  for(mp_integer i=0; i<size; ++i)
+  for(mp_integer i = 0; i < *size; ++i)
   {
     exprt counter=from_integer(i, counter_type);
 
@@ -343,7 +343,7 @@ bvt boolbvt::convert_lambda(const exprt &expr)
     const bvt &tmp=convert_bv(expr_op1);
 
     INVARIANT(
-      size * tmp.size() == width,
+      *size * tmp.size() == width,
       "total bitvector width shall equal the number of operands times the size "
       "per operand");
 

src/solvers/flattening/boolbv_byte_update.cpp

@@ -38,11 +38,11 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 
   // see if the byte number is constant
 
-  mp_integer index;
-  if(!to_integer(offset_expr, index))
+  const auto index = numeric_cast<mp_integer>(offset_expr);
+  if(index.has_value())
   {
     // yes!
-    mp_integer offset=index*8;
+    const mp_integer offset = *index * 8;
 
     if(offset+update_width>mp_integer(bv.size()) || offset<0)
     {

src/solvers/flattening/boolbv_extractbit.cpp

@@ -28,7 +28,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
     if(index_as_integer < 0 || index_as_integer >= src_bv.size())
       return prop.new_variable(); // out of range!
     else
-      return src_bv[integer2size_t(index_as_integer)];
+      return src_bv[numeric_cast_v<std::size_t>(index_as_integer)];
   }
 
   if(

src/solvers/flattening/boolbv_width.cpp

@@ -128,16 +128,16 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     const array_typet &array_type=to_array_type(type);
     std::size_t sub_width=operator()(array_type.subtype());
 
-    mp_integer array_size;
+    const auto array_size = numeric_cast<mp_integer>(array_type.size());
 
-    if(to_integer(array_type.size(), array_size))
+    if(!array_size.has_value())
     {
       // we can still use the theory of arrays for this
       entry.total_width=0;
     }
     else
     {
-      mp_integer total=array_size*sub_width;
+      mp_integer total = *array_size * sub_width;
       if(total>(1<<30)) // realistic limit
         throw analysis_exceptiont("array too large for flattening");
 
@@ -149,21 +149,13 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     const vector_typet &vector_type=to_vector_type(type);
     std::size_t sub_width=operator()(vector_type.subtype());
 
-    mp_integer vector_size;
+    const auto vector_size = numeric_cast_v<mp_integer>(vector_type.size());
 
-    if(to_integer(vector_type.size(), vector_size))
-    {
-      // we can still use the theory of arrays for this
-      entry.total_width=0;
-    }
-    else
-    {
-      mp_integer total=vector_size*sub_width;
-      if(total>(1<<30)) // realistic limit
-        analysis_exceptiont("vector too large for flattening");
+    mp_integer total = vector_size * sub_width;
+    if(total > (1 << 30)) // realistic limit
+      analysis_exceptiont("vector too large for flattening");
 
-      entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
-    }
+    entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
   }
   else if(type_id==ID_complex)
   {

src/solvers/flattening/boolbv_with.cpp

@@ -125,9 +125,9 @@ void boolbvt::convert_with_array(
 
   const exprt &array_size=type.size();
 
-  mp_integer size;
+  const auto size = numeric_cast<mp_integer>(array_size);
 
-  if(to_integer(array_size, size))
+  if(!size.has_value())
   {
     error().source_location=type.source_location();
     error() << "convert_with_array expects constant array size" << eom;
@@ -136,7 +136,7 @@ void boolbvt::convert_with_array(
 
   const bvt &op2_bv=convert_bv(op2);
 
-  if(size*op2_bv.size()!=prev_bv.size())
+  if(*size * op2_bv.size() != prev_bv.size())
   {
     error().source_location=type.source_location();
     error() << "convert_with_array: unexpected operand 2 width" << eom;
@@ -150,7 +150,7 @@ void boolbvt::convert_with_array(
     // Yes, it is!
     next_bv=prev_bv;
 
-    if(op1_value>=0 && op1_value<size) // bounds check
+    if(op1_value >= 0 && op1_value < *size) // bounds check
     {
       const std::size_t offset =
         numeric_cast_v<std::size_t>(op1_value * op2_bv.size());

src/util/endianness_map.cpp

@@ -92,25 +92,23 @@ void endianness_mapt::build_big_endian(const typet &src)
     const array_typet &array_type=to_array_type(src);
 
     // array size constant?
-    mp_integer s;
-    if(!to_integer(array_type.size(), s))
+    auto s = numeric_cast<mp_integer>(array_type.size());
+    if(s.has_value())
     {
-      while(s>0)
+      while(*s > 0)
       {
         build_big_endian(array_type.subtype());
-        --s;
+        --(*s);
       }
     }
   }
   else if(src.id()==ID_vector)
   {
     const vector_typet &vector_type=to_vector_type(src);
 
-    mp_integer s;
-    if(to_integer(vector_type.size(), s))
-      CHECK_RETURN(false);
+    mp_integer s = numeric_cast_v<mp_integer>(vector_type.size());
 
-    while(s>0)
+    while(s > 0)
     {
       build_big_endian(vector_type.subtype());
       --s;