diff --git a/regression/systemc/Constructor1/main.cpp b/regression/systemc/Constructor1/main.cpp new file mode 100644 index 00000000000..a7eed75df7b --- /dev/null +++ b/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; +} diff --git a/regression/systemc/Constructor1/test.desc b/regression/systemc/Constructor1/test.desc new file mode 100644 index 00000000000..b2309a9fc34 --- /dev/null +++ b/regression/systemc/Constructor1/test.desc @@ -0,0 +1,9 @@ +CORE +main.cpp + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +no body for function diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 3da62aec260..f27374eba53 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/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();