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

Author: tautschnig

src/util/endianness_map.cpp

@@ -92,28 +92,27 @@ 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);
+    auto s = numeric_cast<mp_integer>(vector_type.size());
+    CHECK_RETURN(s.has_value());
 
-    while(s>0)
+    while(*s > 0)
     {
       build_big_endian(vector_type.subtype());
-      --s;
+      --*s;
     }
   }
   else

src/util/expr_initializer.cpp

@@ -144,8 +144,6 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       exprt tmpval =
         expr_initializer_rec(array_type.subtype(), source_location);
 
-      mp_integer array_size;
-
       if(array_type.size().id()==ID_infinity)
       {
         if(nondet)
@@ -159,7 +157,10 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
         value.add_source_location()=source_location;
         return value;
       }
-      else if(to_integer(array_type.size(), array_size))
+
+      auto array_size = numeric_cast<mp_integer>(array_type.size());
+
+      if(!array_size.has_value())
       {
         if(nondet)
         {
@@ -175,10 +176,10 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       }
 
       DATA_INVARIANT(
-        array_size >= 0, "array should not have negative size");
+        *array_size >= 0, "array should not have negative size");
 
       array_exprt value(array_type);
-      value.operands().resize(integer2size_t(array_size), tmpval);
+      value.operands().resize(numeric_cast_v<std::size_t>(*array_size), tmpval);
       value.add_source_location()=source_location;
       return value;
     }
@@ -189,9 +190,9 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
 
     exprt tmpval = expr_initializer_rec(vector_type.subtype(), source_location);
 
-    mp_integer vector_size;
+    auto vector_size = numeric_cast<mp_integer>(vector_type.size());
 
-    if(to_integer(vector_type.size(), vector_size))
+    if(!vector_size.has_value())
     {
       if(nondet)
       {
@@ -207,10 +208,10 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
     }
 
     DATA_INVARIANT(
-      vector_size >= 0, "vector should not have negative size");
+      *vector_size >= 0, "vector should not have negative size");
 
     vector_exprt value(vector_type);
-    value.operands().resize(integer2size_t(vector_size), tmpval);
+    value.operands().resize(numeric_cast_v<std::size_t>(*vector_size), tmpval);
     value.add_source_location()=source_location;
 
     return value;

src/util/pointer_offset_size.cpp

@@ -122,15 +122,13 @@ mp_integer pointer_offset_bits(
       return -1;
 
     // get size
-    const exprt &size=to_array_type(type).size();
+    const auto size = numeric_cast<mp_integer>(to_array_type(type).size());
 
     // constant?
-    mp_integer i;
-
-    if(to_integer(size, i))
+    if(!size.has_value())
       return -1; // we cannot distinguish the elements
 
-    return sub*i;
+    return sub * *size;
   }
   else if(type.id()==ID_vector)
   {
@@ -139,15 +137,13 @@ mp_integer pointer_offset_bits(
       return -1;
 
     // get size
-    const exprt &size=to_vector_type(type).size();
+    const auto size = numeric_cast<mp_integer>(to_vector_type(type).size());
 
     // constant?
-    mp_integer i;
-
-    if(to_integer(size, i))
+    if(!size.has_value())
       return -1; // we cannot distinguish the elements
 
-    return sub*i;
+    return sub * *size;
   }
   else if(type.id()==ID_complex)
   {