Merge pull request #4151 from tautschnig/update-after-remove-returns
Update after remove returns
This commit is contained in:
commit
ee11014382
|
@ -448,10 +448,6 @@ int goto_instrument_parse_optionst::doit()
|
||||||
if(cmdline.isset("check-call-sequence"))
|
if(cmdline.isset("check-call-sequence"))
|
||||||
{
|
{
|
||||||
do_remove_returns();
|
do_remove_returns();
|
||||||
|
|
||||||
// recalculate numbers, etc.
|
|
||||||
goto_model.goto_functions.update();
|
|
||||||
|
|
||||||
check_call_sequence(goto_model);
|
check_call_sequence(goto_model);
|
||||||
return CPROVER_EXIT_SUCCESS;
|
return CPROVER_EXIT_SUCCESS;
|
||||||
}
|
}
|
||||||
|
@ -1456,9 +1452,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
|
||||||
{
|
{
|
||||||
do_indirect_call_and_rtti_removal();
|
do_indirect_call_and_rtti_removal();
|
||||||
|
|
||||||
// recalculate numbers, etc.
|
|
||||||
goto_model.goto_functions.update();
|
|
||||||
|
|
||||||
status() << "Performing a reachability slice" << eom;
|
status() << "Performing a reachability slice" << eom;
|
||||||
if(cmdline.isset("property"))
|
if(cmdline.isset("property"))
|
||||||
reachability_slicer(goto_model, cmdline.get_values("property"));
|
reachability_slicer(goto_model, cmdline.get_values("property"));
|
||||||
|
@ -1470,9 +1463,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
|
||||||
{
|
{
|
||||||
do_indirect_call_and_rtti_removal();
|
do_indirect_call_and_rtti_removal();
|
||||||
|
|
||||||
// recalculate numbers, etc.
|
|
||||||
goto_model.goto_functions.update();
|
|
||||||
|
|
||||||
status() << "Performing a function pointer reachability slice" << eom;
|
status() << "Performing a function pointer reachability slice" << eom;
|
||||||
function_path_reachability_slicer(
|
function_path_reachability_slicer(
|
||||||
goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
|
goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
|
||||||
|
@ -1484,9 +1474,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
|
||||||
do_indirect_call_and_rtti_removal();
|
do_indirect_call_and_rtti_removal();
|
||||||
do_remove_returns();
|
do_remove_returns();
|
||||||
|
|
||||||
// recalculate numbers, etc.
|
|
||||||
goto_model.goto_functions.update();
|
|
||||||
|
|
||||||
status() << "Performing a full slice" << eom;
|
status() << "Performing a full slice" << eom;
|
||||||
if(cmdline.isset("property"))
|
if(cmdline.isset("property"))
|
||||||
property_slicer(goto_model, cmdline.get_values("property"));
|
property_slicer(goto_model, cmdline.get_values("property"));
|
||||||
|
|
|
@ -44,7 +44,7 @@ protected:
|
||||||
const irep_idt &function_id,
|
const irep_idt &function_id,
|
||||||
goto_functionst::goto_functiont &function);
|
goto_functionst::goto_functiont &function);
|
||||||
|
|
||||||
void do_function_calls(
|
bool do_function_calls(
|
||||||
function_is_stubt function_is_stub,
|
function_is_stubt function_is_stub,
|
||||||
goto_programt &goto_program);
|
goto_programt &goto_program);
|
||||||
|
|
||||||
|
@ -142,10 +142,14 @@ void remove_returnst::replace_returns(
|
||||||
/// \param function_is_stub: function (irep_idt -> bool) that determines whether
|
/// \param function_is_stub: function (irep_idt -> bool) that determines whether
|
||||||
/// a given function ID is a stub
|
/// a given function ID is a stub
|
||||||
/// \param goto_program: program to transform
|
/// \param goto_program: program to transform
|
||||||
void remove_returnst::do_function_calls(
|
/// \return True if, and only if, instructions have been inserted. In that case
|
||||||
|
/// the caller must invoke an appropriate method to update location numbers.
|
||||||
|
bool remove_returnst::do_function_calls(
|
||||||
function_is_stubt function_is_stub,
|
function_is_stubt function_is_stub,
|
||||||
goto_programt &goto_program)
|
goto_programt &goto_program)
|
||||||
{
|
{
|
||||||
|
bool requires_update = false;
|
||||||
|
|
||||||
Forall_goto_program_instructions(i_it, goto_program)
|
Forall_goto_program_instructions(i_it, goto_program)
|
||||||
{
|
{
|
||||||
if(i_it->is_function_call())
|
if(i_it->is_function_call())
|
||||||
|
@ -221,6 +225,8 @@ void remove_returnst::do_function_calls(
|
||||||
t_a,
|
t_a,
|
||||||
goto_programt::make_dead(*return_value, i_it->source_location));
|
goto_programt::make_dead(*return_value, i_it->source_location));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
requires_update = true;
|
||||||
}
|
}
|
||||||
|
|
||||||
// update the call
|
// update the call
|
||||||
|
@ -228,6 +234,8 @@ void remove_returnst::do_function_calls(
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
return requires_update;
|
||||||
}
|
}
|
||||||
|
|
||||||
void remove_returnst::operator()(goto_functionst &goto_functions)
|
void remove_returnst::operator()(goto_functionst &goto_functions)
|
||||||
|
@ -244,7 +252,8 @@ void remove_returnst::operator()(goto_functionst &goto_functions)
|
||||||
};
|
};
|
||||||
|
|
||||||
replace_returns(it->first, it->second);
|
replace_returns(it->first, it->second);
|
||||||
do_function_calls(function_is_stub, it->second.body);
|
if(do_function_calls(function_is_stub, it->second.body))
|
||||||
|
goto_functions.compute_location_numbers(it->second.body);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -261,7 +270,8 @@ void remove_returnst::operator()(
|
||||||
return;
|
return;
|
||||||
|
|
||||||
replace_returns(model_function.get_function_id(), goto_function);
|
replace_returns(model_function.get_function_id(), goto_function);
|
||||||
do_function_calls(function_is_stub, goto_function.body);
|
if(do_function_calls(function_is_stub, goto_function.body))
|
||||||
|
model_function.compute_location_numbers();
|
||||||
}
|
}
|
||||||
|
|
||||||
/// removes returns
|
/// removes returns
|
||||||
|
|
Loading…
Reference in New Issue