cpp_typecheckt::cpp_destructor now returns optionalt<codet> instead of an expression

Author: kroening

src/cpp/cpp_destructor.cpp

@@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/c_types.h>
 
 /// \return typechecked code
-codet cpp_typecheckt::cpp_destructor(
+optionalt<codet> cpp_typecheckt::cpp_destructor(
   const source_locationt &source_location,
   const exprt &object)
 {
@@ -31,22 +31,15 @@ codet cpp_typecheckt::cpp_destructor(
 
   // PODs don't need a destructor
   if(cpp_is_pod(tmp_type))
-  {
-    new_code.make_nil();
-    return new_code;
-  }
+    return {};
 
   if(tmp_type.id()==ID_array)
   {
     const exprt &size_expr=
       to_array_type(tmp_type).size();
 
     if(size_expr.id()=="infinity")
-    {
-      // don't initialize
-      new_code.make_nil();
-      return new_code;
-    }
+      return {}; // don't initialize
 
     exprt tmp_size=size_expr;
     make_constant_index(tmp_size);
@@ -73,9 +66,9 @@ codet cpp_typecheckt::cpp_destructor(
       index_exprt index(object, constant);
       index.add_source_location()=source_location;
 
-      exprt i_code = cpp_destructor(source_location, index);
-
-      new_code.move_to_operands(i_code);
+      auto i_code = cpp_destructor(source_location, index);
+      if(i_code.has_value())
+        new_code.move_to_operands(i_code.value());
     }
   }
   else

src/cpp/cpp_typecheck.h

@@ -427,9 +427,8 @@ class cpp_typecheckt:public c_typecheck_baset
 
   const struct_typet &this_struct_type();
 
-  codet cpp_destructor(
-      const source_locationt &source_location,
-      const exprt &object);
+  optionalt<codet>
+  cpp_destructor(const source_locationt &source_location, const exprt &object);
 
   // expressions
   void explicit_typecast_ambiguity(exprt &expr);

src/cpp/cpp_typecheck_destructor.cpp

@@ -144,11 +144,11 @@ codet cpp_typecheckt::dtor(const symbolt &symbol)
 
     const bool disabled_access_control = disable_access_control;
     disable_access_control = true;
-    codet dtor_code = cpp_destructor(source_location, member);
+    auto dtor_code = cpp_destructor(source_location, member);
     disable_access_control = disabled_access_control;
 
-    if(dtor_code.is_not_nil())
-      block.move_to_operands(dtor_code);
+    if(dtor_code.has_value())
+      block.move_to_operands(dtor_code.value());
   }
 
   const irept::subt &bases=symbol.type.find(ID_bases).get_sub();
@@ -169,11 +169,11 @@ codet cpp_typecheckt::dtor(const symbolt &symbol)
 
     const bool disabled_access_control = disable_access_control;
     disable_access_control = true;
-    exprt dtor_code = cpp_destructor(source_location, object);
+    auto dtor_code = cpp_destructor(source_location, object);
     disable_access_control = disabled_access_control;
 
-    if(dtor_code.is_not_nil())
-      block.move_to_operands(dtor_code);
+    if(dtor_code.has_value())
+      block.move_to_operands(dtor_code.value());
   }
 
   return block;

src/cpp/cpp_typecheck_expr.cpp

@@ -1074,15 +1074,16 @@ void cpp_typecheckt::typecheck_expr_delete(exprt &expr)
 
   already_typechecked(new_object);
 
-  codet destructor_code=cpp_destructor(
-    expr.source_location(),
-    new_object);
+  auto destructor_code = cpp_destructor(expr.source_location(), new_object);
 
-  // this isn't typechecked yet
-  if(destructor_code.is_not_nil())
-    typecheck_code(destructor_code);
-
-  expr.set(ID_destructor, destructor_code);
+  if(destructor_code.has_value())
+  {
+    // this isn't typechecked yet
+    typecheck_code(destructor_code.value());
+    expr.set(ID_destructor, destructor_code.value());
+  }
+  else
+    expr.set(ID_destructor, nil_exprt());
 }
 
 void cpp_typecheckt::typecheck_expr_typecast(exprt &)