Skip to content

Use goto_programt::make_X factories in remove_returns #4001

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Feb 11, 2019
Merged

Use goto_programt::make_X factories in remove_returns #4001

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3df3ef6
added variants of goto_programt::insert_before/after that take instru…
Jan 31, 2019
aa85fb2
use the new goto_programt::make_X factories in remove_returns
Jan 31, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions src/goto-programs/goto_program.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -573,6 +573,14 @@ class goto_programt
return instructions.insert(target, instructiont());
}

/// Insertion before the instruction pointed-to by the given instruction
/// iterator `target`.
/// \return newly inserted location
targett insert_before(const_targett target, const instructiont &i)
{
return instructions.insert(target, i);
}

/// Insertion after the instruction pointed-to by the given instruction
/// iterator `target`.
/// \return newly inserted location
Expand All @@ -581,6 +589,14 @@ class goto_programt
return instructions.insert(std::next(target), instructiont());
}

/// Insertion after the instruction pointed-to by the given instruction
/// iterator `target`.
/// \return newly inserted location
targett insert_after(const_targett target, const instructiont &i)
{
return instructions.insert(std::next(target), i);
}

/// Appends the given program `p` to `*this`. `p` is destroyed.
void destructive_append(goto_programt &p)
{
Expand Down
15 changes: 7 additions & 8 deletions src/goto-programs/remove_returns.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -206,20 +206,19 @@ void remove_returnst::do_function_calls(
rhs = side_effect_expr_nondett(
function_call.lhs().type(), i_it->source_location);

goto_programt::targett t_a=goto_program.insert_after(i_it);
t_a->make_assignment();
t_a->source_location=i_it->source_location;
t_a->code=code_assignt(function_call.lhs(), rhs);
goto_programt::targett t_a = goto_program.insert_after(
i_it,
goto_programt::make_assignment(
code_assignt(function_call.lhs(), rhs), i_it->source_location));

// fry the previous assignment
function_call.lhs().make_nil();

if(!is_stub)
{
goto_programt::targett t_d=goto_program.insert_after(t_a);
t_d->make_dead();
t_d->source_location=i_it->source_location;
t_d->code = code_deadt(*return_value);
goto_program.insert_after(
t_a,
goto_programt::make_dead(*return_value, i_it->source_location));
}
}
}
Expand Down