Replace use of deprecated nil_typet in c_bit_field_replacement_type

Use optionalt<typet> as recommended in the deprecation note.

Author: tautschnig

src/solvers/flattening/boolbv_typecast.cpp

@@ -38,20 +38,18 @@ bool boolbvt::type_conversion(
   bvtypet src_bvtype=get_bvtype(src_type);
 
   if(src_bvtype==bvtypet::IS_C_BIT_FIELD)
-    return
-      type_conversion(
-        c_bit_field_replacement_type(to_c_bit_field_type(src_type), ns),
-        src,
-        dest_type,
-        dest);
+    return type_conversion(
+      *c_bit_field_replacement_type(to_c_bit_field_type(src_type), ns),
+      src,
+      dest_type,
+      dest);
 
   if(dest_bvtype==bvtypet::IS_C_BIT_FIELD)
-    return
-      type_conversion(
-        src_type,
-        src,
-        c_bit_field_replacement_type(to_c_bit_field_type(dest_type), ns),
-        dest);
+    return type_conversion(
+      src_type,
+      src,
+      *c_bit_field_replacement_type(to_c_bit_field_type(dest_type), ns),
+      dest);
 
   std::size_t src_width=src.size();
   std::size_t dest_width=boolbv_width(dest_type);

src/solvers/flattening/c_bit_field_replacement_type.cpp

@@ -9,9 +9,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_bit_field_replacement_type.h"
 
-typet c_bit_field_replacement_type(
-  const c_bit_field_typet &src,
-  const namespacet &ns)
+#include <util/namespace.h>
+
+optionalt<typet>
+c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
 {
   const typet &subtype=src.subtype();
 
@@ -35,9 +36,7 @@ typet c_bit_field_replacement_type(
       result.set_width(src.get_width());
       return std::move(result);
     }
-    else
-      return nil_typet();
   }
-  else
-    return nil_typet();
+
+  return {};
 }

src/solvers/flattening/c_bit_field_replacement_type.h

@@ -10,11 +10,12 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_FLATTENING_C_BIT_FIELD_REPLACEMENT_TYPE_H
 #define CPROVER_SOLVERS_FLATTENING_C_BIT_FIELD_REPLACEMENT_TYPE_H
 
+#include <util/optional.h>
 #include <util/std_types.h>
-#include <util/namespace.h>
 
-typet c_bit_field_replacement_type(
-  const c_bit_field_typet &,
-  const namespacet &);
+class namespacet;
+
+optionalt<typet>
+c_bit_field_replacement_type(const c_bit_field_typet &, const namespacet &);
 
 #endif // CPROVER_SOLVERS_FLATTENING_C_BIT_FIELD_REPLACEMENT_TYPE_H

src/solvers/smt2/smt2_conv.cpp

@@ -2176,8 +2176,9 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
         convert_expr(src); // ignore
       else
       {
-        typet t=c_bit_field_replacement_type(to_c_bit_field_type(src_type), ns);
-        typecast_exprt tmp(typecast_exprt(src, t), dest_type);
+        const auto t =
+          c_bit_field_replacement_type(to_c_bit_field_type(src_type), ns);
+        typecast_exprt tmp(typecast_exprt(src, *t), dest_type);
         convert_typecast(tmp);
       }
     }
@@ -2416,8 +2417,9 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
       convert_expr(src); // ignore
     else
     {
-      typet t=c_bit_field_replacement_type(to_c_bit_field_type(dest_type), ns);
-      typecast_exprt tmp(typecast_exprt(src, t), dest_type);
+      const auto t =
+        c_bit_field_replacement_type(to_c_bit_field_type(dest_type), ns);
+      typecast_exprt tmp(typecast_exprt(src, *t), dest_type);
       convert_typecast(tmp);
     }
   }
@@ -4527,7 +4529,7 @@ void smt2_convt::convert_type(const typet &type)
   }
   else if(type.id()==ID_c_bit_field)
   {
-    convert_type(c_bit_field_replacement_type(to_c_bit_field_type(type), ns));
+    convert_type(*c_bit_field_replacement_type(to_c_bit_field_type(type), ns));
   }
   else
   {