C++ front-end: fix global constructor and member initialization

regression/cbmc-cpp/gh-issue-537/main.cpp

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+class C
+{
+public:
+  int x;
+
+  C() : x(7)
+  {
+  }
+};
+
+C c1;
+
+class D
+{
+public:
+  int x = 7;
+};
+
+int main()
+{
+  assert(c1.x == 7); // Fails
+
+  C c2;
+  assert(c2.x == 7); // Succeeds
+
+  D d;
+  assert(d.x == 7); // C++11 Class Member Initialization Fails
+
+  return 0;
+}

regression/cbmc-cpp/gh-issue-537/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.cpp
+--cpp11
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/cpp/cpp_typecheck_compound_type.cpp

@@ -754,6 +754,13 @@ void cpp_typecheckt::typecheck_compound_declarator(
     }
   }
 
+  // Handle C++11 default member initializers for non-static members
+  if(!is_static && !is_method && value.is_not_nil())
+  {
+    // Store the default initializer value in the component
+    component.add(ID_C_default_value) = value;
+  }
+
   // array members must have fixed size
   check_fixed_size_array(component.type());
 
@@ -1097,7 +1104,25 @@ void cpp_typecheckt::typecheck_compound_body(symbolt &symbol)
   if(symbol.type.id()==ID_struct)
     do_virtual_table(symbol);
 
-  if(!found_ctor && !cpp_is_pod(symbol.type))
+  // Check if any component has a C++11 default member initializer
+  bool has_default_member_initializer = false;
+  for(const auto &component : type.components())
+  {
+    if(
+      !component.get_bool(ID_from_base) && component.type().id() != ID_code &&
+      !component.get_bool(ID_is_type) && !component.get_bool(ID_is_static) &&
+      component.find(ID_C_default_value).is_not_nil())
+    {
+      has_default_member_initializer = true;
+      break;
+    }
+  }
+
+  // Generate a default constructor if:
+  // - No constructor was found, AND
+  // - Either the type is not POD OR it has C++11 default member initializers
+  if(
+    !found_ctor && (!cpp_is_pod(symbol.type) || has_default_member_initializer))
   {
     // it's public!
     exprt cpp_public("cpp-public");

src/cpp/cpp_typecheck_constructor.cpp

@@ -752,6 +752,18 @@ void cpp_typecheckt::full_member_initialization(
       mem_init.set(ID_member, cppname);
       final_initializers.move_to_sub(mem_init);
     }
+    // Handle C++11 default member initializers for POD types
+    else if(
+      !found && cpp_is_pod(c.type()) && c.find(ID_C_default_value).is_not_nil())
+    {
+      cpp_namet cppname(mem_name);
+
+      codet mem_init(ID_member_initializer);
+      mem_init.set(ID_member, cppname);
+      mem_init.copy_to_operands(
+        static_cast<const exprt &>(c.find(ID_C_default_value)));
+      final_initializers.move_to_sub(mem_init);
+    }
   }
 
   initializers.swap(final_initializers);