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

Author: kroening

src/cpp/cpp_constructor.cpp

@@ -22,7 +22,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 /// \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,21 @@ codet cpp_typecheckt::cpp_constructor(
           tmp_operands.push_back(operand);
         }
 
-        exprt i_code =
-          cpp_constructor(source_location, index, tmp_operands);
+        auto i_code = cpp_constructor(source_location, index, tmp_operands);
 
-        if(i_code.is_nil())
+        if(!i_code.has_value())
         {
           new_code.is_nil();
           break;
         }
 
-        new_code.move_to_operands(i_code);
+        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 +142,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 +152,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 +163,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 +282,7 @@ codet cpp_typecheckt::cpp_constructor(
   else
     UNREACHABLE;
 
-  codet nil;
-  nil.make_nil();
-  return nil;
+  return {};
 }
 
 void cpp_typecheckt::new_temporary(
@@ -316,15 +303,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_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);

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_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

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();
   }
 }