Skip to content

Commit 2283046

Browse files
author
martin
committed
Move the update functions earlier so that they are common between tools
remove_skip and various other passes compute the updates so moving this should not effect the behaviour of the program.
1 parent 6678956 commit 2283046

File tree

1 file changed

+6
-6
lines changed

1 file changed

+6
-6
lines changed

src/cbmc/cbmc_parse_options.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -963,6 +963,12 @@ bool cbmc_parse_optionst::process_goto_program(
963963
string_abstraction(goto_model, log.get_message_handler());
964964
}
965965

966+
// recalculate numbers, etc.
967+
goto_model.goto_functions.update();
968+
969+
// add loop ids
970+
goto_model.goto_functions.compute_loop_numbers();
971+
966972
// ignore default/user-specified initialization
967973
// of variables with static lifetime
968974
if(options.get_bool_option("nondet-static"))
@@ -977,12 +983,6 @@ bool cbmc_parse_optionst::process_goto_program(
977983
// needs to be done before pointer analysis
978984
add_failed_symbols(goto_model.symbol_table);
979985

980-
// recalculate numbers, etc.
981-
goto_model.goto_functions.update();
982-
983-
// add loop ids
984-
goto_model.goto_functions.compute_loop_numbers();
985-
986986
if(options.get_bool_option("drop-unused-functions"))
987987
{
988988
// Entry point will have been set before and function pointers removed

0 commit comments

Comments
 (0)