diff --git a/regression/cbmc-cpp/gh-issue-537/main.cpp b/regression/cbmc-cpp/gh-issue-537/main.cpp new file mode 100644 index 00000000000..f10ed6f1dbe --- /dev/null +++ b/regression/cbmc-cpp/gh-issue-537/main.cpp @@ -0,0 +1,32 @@ +#include + +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; +} \ No newline at end of file diff --git a/regression/cbmc-cpp/gh-issue-537/test.desc b/regression/cbmc-cpp/gh-issue-537/test.desc new file mode 100644 index 00000000000..e1e98c82c25 --- /dev/null +++ b/regression/cbmc-cpp/gh-issue-537/test.desc @@ -0,0 +1,8 @@ +CORE +main.cpp +--cpp11 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index d358bf61680..3117cb90ace 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/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"); diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index 79709e447a2..6ad5247e115 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/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(c.find(ID_C_default_value))); + final_initializers.move_to_sub(mem_init); + } } initializers.swap(final_initializers);