From 709ff796cb933c2c898590dc7bc2da7dfaca5564 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Feb 2024 13:39:03 +0000 Subject: [PATCH] Full slicing always requires consistent location numbers We need to ensure consistency both with single properties as well as when slicing for all properties. --- src/goto-instrument/goto_instrument_parse_options.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index db030ac89b5..e13dc0bc1db 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -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 " @@ -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); } }