File tree 3 files changed +29
-2
lines changed
regression/systemc/Constructor1
3 files changed +29
-2
lines changed Original file line number Diff line number Diff line change
1
+ struct S
2
+ {
3
+ S (int _x) : x(_x) {}
4
+ int x;
5
+ };
6
+
7
+ S s (42 );
8
+
9
+ int main ()
10
+ {
11
+ __CPROVER_assert (s.x == 42 , " " );
12
+ return 0 ;
13
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ main.cpp
3
+
4
+ ^EXIT=0$
5
+ ^SIGNAL=0$
6
+ ^VERIFICATION SUCCESSFUL$
7
+ --
8
+ ^warning: ignoring
9
+ no body for function
Original file line number Diff line number Diff line change @@ -143,8 +143,13 @@ bool static_lifetime_init(
143
143
{
144
144
const symbolt &symbol=ns.lookup (id);
145
145
146
- if (symbol.type .id ()==ID_code &&
147
- to_code_type (symbol.type ).return_type ().id ()==ID_constructor)
146
+ if (symbol.type .id () != ID_code)
147
+ continue ;
148
+
149
+ const code_typet &code_type = to_code_type (symbol.type );
150
+ if (
151
+ code_type.return_type ().id () == ID_constructor &&
152
+ code_type.parameters ().empty ())
148
153
{
149
154
code_function_callt function_call;
150
155
function_call.function ()=symbol.symbol_expr ();
You can’t perform that action at this time.
0 commit comments