Skip to content

Commit a19dd36

Browse files
fixup! Make mode an argument of goto-convert functions
1 parent 0251c7e commit a19dd36

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed

src/goto-programs/goto_convert.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ Function: goto_convertt::finish_gotos
103103
104104
\*******************************************************************/
105105

106-
void goto_convertt::finish_gotos(goto_programt &dest)
106+
void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
107107
{
108108
for(const auto &g_it : targets.gotos)
109109
{
@@ -200,7 +200,7 @@ void goto_convertt::finish_gotos(goto_programt &dest)
200200
unwind_to_size,
201201
destructor_code,
202202
goto_stack,
203-
symbol_table.lookup(i.function)->mode);
203+
mode);
204204
dest.destructive_insert(g_it.first, destructor_code);
205205
// This should leave iterators intact, as long as
206206
// goto_programt::instructionst is std::list.
@@ -313,7 +313,7 @@ void goto_convertt::goto_convert_rec(
313313
PRECONDITION(guarded_gotos.empty());
314314
convert(code, dest, mode);
315315

316-
finish_gotos(dest);
316+
finish_gotos(dest, mode);
317317
finish_computed_gotos(dest);
318318
finish_guarded_gotos(dest);
319319
finish_catch_push_targets(dest);

src/goto-programs/goto_convert_class.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -361,7 +361,7 @@ class goto_convertt:public messaget
361361
// gotos
362362
//
363363

364-
void finish_gotos(goto_programt &dest);
364+
void finish_gotos(goto_programt &dest, const irep_idt &mode);
365365
void finish_computed_gotos(goto_programt &dest);
366366
void finish_guarded_gotos(goto_programt &dest);
367367

0 commit comments

Comments
 (0)