Skip to content

Commit

Permalink
Full slicing always requires consistent location numbers
Browse files Browse the repository at this point in the history
We need to ensure consistency both with single properties as well as
when slicing for all properties.
  • Loading branch information
tautschnig committed Feb 2, 2024
1 parent 5d85d38 commit 709ff79
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/goto-instrument/goto_instrument_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1764,6 +1764,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
do_indirect_call_and_rtti_removal();
do_remove_returns();
rewrite_rw_ok(goto_model);
// full_slicer requires that the model has unique location numbers:
goto_model.goto_functions.update();

log.warning() << "**** WARNING: Experimental option --full-slice, "
<< "analysis results may be unsound. See "
Expand All @@ -1775,8 +1777,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
goto_model, cmdline.get_values("property"), ui_message_handler);
else
{
// full_slicer requires that the model has unique location numbers:
goto_model.goto_functions.update();
full_slicer(goto_model, ui_message_handler);
}
}
Expand Down

0 comments on commit 709ff79

Please sign in to comment.