@@ -122,24 +122,7 @@ void goto_program2codet::scan_for_varargs()
122
122
}
123
123
124
124
if (!va_list_expr.empty ())
125
- {
126
125
system_headers.insert (" stdarg.h" );
127
-
128
- code_typet &code_type=
129
- to_code_type (symbol_table.get_writeable_ref (func_name).type );
130
- code_typet::parameterst ¶meters=code_type.parameters ();
131
-
132
- for (code_typet::parameterst::iterator
133
- it2=parameters.begin ();
134
- it2!=parameters.end ();
135
- ++it2)
136
- {
137
- const symbol_exprt arg=
138
- ns.lookup (it2->get_identifier ()).symbol_expr ();
139
- if (va_list_expr.find (arg)!=va_list_expr.end ())
140
- it2->type ().id (ID_gcc_builtin_va_list);
141
- }
142
- }
143
126
}
144
127
145
128
goto_programt::const_targett goto_program2codet::convert_instruction (
@@ -323,7 +306,6 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
323
306
code_function_callt f (
324
307
symbol_exprt (" va_end" , code_typet ({}, empty_typet ())),
325
308
{this_va_list_expr});
326
- f.arguments ().back ().type ().id (ID_gcc_builtin_va_list);
327
309
328
310
dest.add (std::move (f));
329
311
}
@@ -332,7 +314,6 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
332
314
code_function_callt f (
333
315
symbol_exprt (" va_start" , code_typet ({}, empty_typet ())),
334
316
{this_va_list_expr, to_address_of_expr (r).object ()});
335
- f.arguments ().front ().type ().id (ID_gcc_builtin_va_list);
336
317
337
318
dest.add (std::move (f));
338
319
}
@@ -342,7 +323,6 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
342
323
code_function_callt f (
343
324
symbol_exprt (" va_arg" , code_typet ({}, empty_typet ())),
344
325
{this_va_list_expr});
345
- f.arguments ().back ().type ().id (ID_gcc_builtin_va_list);
346
326
347
327
// we do not bother to set the correct types here, they are not relevant for
348
328
// generating the correct dumped output
@@ -395,7 +375,6 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
395
375
code_function_callt f (
396
376
symbol_exprt (" va_copy" , code_typet ({}, empty_typet ())),
397
377
{this_va_list_expr, r});
398
- f.arguments ().front ().type ().id (ID_gcc_builtin_va_list);
399
378
400
379
dest.add (std::move (f));
401
380
}
@@ -1461,9 +1440,6 @@ void goto_program2codet::cleanup_code(
1461
1440
{
1462
1441
if (code.get_statement ()==ID_decl)
1463
1442
{
1464
- if (va_list_expr.find (code.op0 ())!=va_list_expr.end ())
1465
- code.op0 ().type ().id (ID_gcc_builtin_va_list);
1466
-
1467
1443
if (code.operands ().size ()==2 &&
1468
1444
code.op1 ().id ()==ID_side_effect &&
1469
1445
to_side_effect_expr (code.op1 ()).get_statement ()==ID_function_call)
0 commit comments