cpp_typecheckt::cpp_constructor now returns optionalt<codet>

src/cpp/cpp_constructor.cpp

@@ -22,7 +22,7 @@ Author: Daniel Kroening, [email protected]
 /// \param object: non-typechecked object
 /// \param operands: non-typechecked operands
 /// \return typechecked code
-codet cpp_typecheckt::cpp_constructor(
+optionalt<codet> cpp_typecheckt::cpp_constructor(
   const source_locationt &source_location,
   const exprt &object,
   const exprt::operandst &operands)
@@ -56,22 +56,13 @@ codet cpp_typecheckt::cpp_constructor(
     assert(operands.empty() || operands.size()==1);
 
     if(operands.empty() && cpp_is_pod(tmp_type))
-    {
-      codet nil;
-      nil.make_nil();
-      return nil;
-    }
+      return {};
 
     const exprt &size_expr=
       to_array_type(tmp_type).size();
 
     if(size_expr.id() == ID_infinity)
-    {
-      // don't initialize
-      codet nil;
-      nil.make_nil();
-      return nil;
-    }
+      return {}; // don't initialize
 
     exprt tmp_size=size_expr;
     make_constant_index(tmp_size);
@@ -122,23 +113,16 @@ codet cpp_typecheckt::cpp_constructor(
           tmp_operands.push_back(operand);
         }
 
-        exprt i_code =
-          cpp_constructor(source_location, index, tmp_operands);
-
-        if(i_code.is_nil())
-        {
-          new_code.is_nil();
-          break;
-        }
+        auto i_code = cpp_constructor(source_location, index, tmp_operands);
 
-        new_code.move_to_operands(i_code);
+        if(i_code.has_value())
+          new_code.move(i_code.value());
       }
       return new_code;
     }
   }
   else if(cpp_is_pod(tmp_type))
   {
-    code_expressiont new_code;
     exprt::operandst operands_tc=operands;
 
     for(exprt::operandst::iterator
@@ -153,7 +137,7 @@ codet cpp_typecheckt::cpp_constructor(
     if(operands_tc.empty())
     {
       // a POD is NOT initialized
-      new_code.make_nil();
+      return {};
     }
     else if(operands_tc.size()==1)
     {
@@ -163,7 +147,9 @@ codet cpp_typecheckt::cpp_constructor(
       side_effect_exprt assign(ID_assign, typet(), source_location);
       assign.copy_to_operands(object_tc, operands_tc.front());
       typecheck_side_effect_assignment(assign);
+      code_expressiont new_code;
       new_code.expression()=assign;
+      return new_code;
     }
     else
     {
@@ -172,8 +158,6 @@ codet cpp_typecheckt::cpp_constructor(
                  "but got " << operands.size() << eom;
       throw 0;
     }
-
-    return new_code;
   }
   else if(tmp_type.id()==ID_union)
   {
@@ -293,9 +277,7 @@ codet cpp_typecheckt::cpp_constructor(
   else
     UNREACHABLE;
 
-  codet nil;
-  nil.make_nil();
-  return nil;
+  return {};
 }
 
 void cpp_typecheckt::new_temporary(
@@ -316,15 +298,14 @@ void cpp_typecheckt::new_temporary(
 
   already_typechecked(new_object);
 
-  codet new_code =
-    cpp_constructor(source_location, new_object, ops);
+  auto new_code = cpp_constructor(source_location, new_object, ops);
 
-  if(new_code.is_not_nil())
+  if(new_code.has_value())
   {
-    if(new_code.get(ID_statement)==ID_assign)
-      tmp_object_expr.move_to_operands(new_code.op1());
+    if(new_code->get_statement() == ID_assign)
+      tmp_object_expr.move_to_operands(new_code->op1());
     else
-      tmp_object_expr.add(ID_initializer)=new_code;
+      tmp_object_expr.add(ID_initializer) = *new_code;
   }
 
   temporary.swap(tmp_object_expr);

src/cpp/cpp_destructor.cpp

@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
 #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.cpp

@@ -188,11 +188,10 @@ void cpp_typecheckt::static_and_dynamic_initialization()
       // use default constructor
       exprt::operandst ops;
 
-      codet call=
-        cpp_constructor(symbol.location, symbol_expr, ops);
+      auto call = cpp_constructor(symbol.location, symbol_expr, ops);
 
-      if(call.is_not_nil())
-        init_block.move_to_operands(call);
+      if(call.has_value())
+        init_block.move(call.value());
     }
   }
 

src/cpp/cpp_typecheck.h

@@ -99,7 +99,7 @@ class cpp_typecheckt:public c_typecheck_baset
 
   bool cpp_is_pod(const typet &type) const;
 
-  codet cpp_constructor(
+  optionalt<codet> cpp_constructor(
     const source_locationt &source_location,
     const exprt &object,
     const exprt::operandst &operands);
@@ -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_code.cpp

@@ -327,16 +327,17 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
         // it's a data member
         already_typechecked(symbol_expr);
 
-        exprt call=
+        auto call =
           cpp_constructor(code.source_location(), symbol_expr, code.operands());
 
-        if(call.is_nil())
+        if(call.has_value())
+          code.swap(call.value());
+        else
         {
-          call=codet(ID_skip);
-          call.add_source_location()=code.source_location();
+          auto source_location = code.source_location();
+          code = codet(ID_skip);
+          code.add_source_location() = source_location;
         }
-
-        code.swap(call);
       }
     }
     else
@@ -434,14 +435,11 @@ void cpp_typecheckt::typecheck_decl(codet &code)
 
       already_typechecked(object_expr);
 
-      exprt constructor_call=
-        cpp_constructor(
-          symbol.location,
-          object_expr,
-          declarator.init_args().operands());
+      auto constructor_call = cpp_constructor(
+        symbol.location, object_expr, declarator.init_args().operands());
 
-      if(constructor_call.is_not_nil())
-        new_code.move_to_operands(constructor_call);
+      if(constructor_call.has_value())
+        new_code.move_to_operands(constructor_call.value());
     }
   }
 

src/cpp/cpp_typecheck_compound_type.cpp

@@ -740,10 +740,10 @@ void cpp_typecheckt::typecheck_compound_declarator(
 
         exprt::operandst ops;
         ops.push_back(value);
-        codet defcode =
-          cpp_constructor(source_locationt(), symexpr, ops);
+        auto defcode = cpp_constructor(source_locationt(), symexpr, ops);
+        CHECK_RETURN(defcode.has_value());
 
-        new_symbol->value.swap(defcode);
+        new_symbol->value.swap(defcode.value());
       }
     }
   }

src/cpp/cpp_typecheck_declaration.cpp

@@ -178,11 +178,15 @@ void cpp_typecheckt::convert_non_template_declaration(
     if(symbol.is_lvalue &&
        declarator.init_args().has_operands())
     {
-      symbol.value=
-        cpp_constructor(
-          symbol.location,
-          cpp_symbol_expr(symbol),
-          declarator.init_args().operands());
+      auto constructor = cpp_constructor(
+        symbol.location,
+        cpp_symbol_expr(symbol),
+        declarator.init_args().operands());
+
+      if(constructor.has_value())
+        symbol.value = constructor.value();
+      else
+        symbol.value = nil_exprt();
     }
   }
 }

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

@@ -852,13 +852,13 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr)
     throw 0;
   }
 
-  exprt code=
-    cpp_constructor(
-      expr.find_source_location(),
-      object_expr,
-      initializer.operands());
+  auto code = cpp_constructor(
+    expr.find_source_location(), object_expr, initializer.operands());
 
-  expr.add(ID_initializer).swap(code);
+  if(code.has_value())
+    expr.add(ID_initializer).swap(code.value());
+  else
+    expr.add(ID_initializer) = nil_exprt();
 
   // we add the size of the object for convenience of the
   // runtime library
@@ -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);
-
-  // this isn't typechecked yet
-  if(destructor_code.is_not_nil())
-    typecheck_code(destructor_code);
+  auto destructor_code = cpp_destructor(expr.source_location(), new_object);
 
-  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 &)

src/cpp/cpp_typecheck_initializer.cpp

@@ -180,10 +180,13 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol)
     exprt::operandst ops;
     ops.push_back(symbol.value);
 
-    symbol.value = cpp_constructor(
-      symbol.value.source_location(),
-      expr_symbol,
-      ops);
+    auto constructor =
+      cpp_constructor(symbol.value.source_location(), expr_symbol, ops);
+
+    if(constructor.has_value())
+      symbol.value = constructor.value();
+    else
+      symbol.value = nil_exprt();
   }
 }