Merge pull request #2342 from tautschnig/constructor

Only parameter-free constructors can be static initializer functions

Author: kroening

regression/systemc/Constructor1/main.cpp

@@ -0,0 +1,13 @@
+struct S
+{
+  S(int _x) : x(_x) {}
+  int x;
+};
+
+S s(42);
+
+int main()
+{
+  __CPROVER_assert(s.x == 42, "");
+  return 0;
+}

regression/systemc/Constructor1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+no body for function

src/linking/static_lifetime_init.cpp

@@ -143,8 +143,13 @@ bool static_lifetime_init(
   {
     const symbolt &symbol=ns.lookup(id);
 
-    if(symbol.type.id()==ID_code &&
-       to_code_type(symbol.type).return_type().id()==ID_constructor)
+    if(symbol.type.id() != ID_code)
+      continue;
+
+    const code_typet &code_type = to_code_type(symbol.type);
+    if(
+      code_type.return_type().id() == ID_constructor &&
+      code_type.parameters().empty())
     {
       code_function_callt function_call;
       function_call.function()=symbol.symbol_expr();