Skip to content

Commit e59511c

Browse files
Factorize setting config from symbol table when reading goto binaries
1 parent 2456011 commit e59511c

7 files changed

+4
-12
lines changed

src/cbmc/cbmc_parse_options.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -677,9 +677,6 @@ int cbmc_parse_optionst::get_goto_program(
677677
}
678678
}
679679

680-
if(!binaries.empty())
681-
config.set_from_symbol_table(symbol_table);
682-
683680
if(cmdline.isset("show-symbol-table"))
684681
{
685682
show_symbol_table();

src/clobber/clobber_parse_options.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -208,8 +208,6 @@ bool clobber_parse_optionst::get_goto_program(
208208
symbol_table, goto_functions, get_message_handler()))
209209
return true;
210210

211-
config.set_from_symbol_table(symbol_table);
212-
213211
if(cmdline.isset("show-symbol-table"))
214212
{
215213
show_symbol_table();

src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -346,7 +346,6 @@ int goto_diff_parse_optionst::get_goto_program(
346346
return 6;
347347

348348
config.set(cmdline);
349-
config.set_from_symbol_table(goto_model.symbol_table);
350349

351350
// This one is done.
352351
cmdline.args.erase(cmdline.args.begin());

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -866,7 +866,6 @@ void goto_instrument_parse_optionst::get_goto_program()
866866
throw 0;
867867

868868
config.set(cmdline);
869-
config.set_from_symbol_table(symbol_table);
870869
}
871870

872871
void goto_instrument_parse_optionst::instrument_goto_program()

src/goto-programs/initialize_goto_model.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -130,9 +130,6 @@ bool initialize_goto_model(
130130
return true;
131131
}
132132

133-
if(!binaries.empty())
134-
config.set_from_symbol_table(goto_model.symbol_table);
135-
136133
msg.status() << "Generating GOTO Program" << messaget::eom;
137134

138135
goto_convert(

src/goto-programs/read_goto_binary.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ Module: Read Goto Programs
2626
#include <util/tempfile.h>
2727
#include <util/rename_symbol.h>
2828
#include <util/base_type.h>
29+
#include <util/config.h>
2930

3031
#include <langapi/language_ui.h>
3132

@@ -382,6 +383,9 @@ bool read_object_and_link(
382383
linking.object_type_updates))
383384
return true;
384385

386+
// reading successful, let's update config
387+
config.set_from_symbol_table(symbol_table);
388+
385389
return false;
386390
}
387391

src/musketeer/musketeer_parse_options.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -138,8 +138,6 @@ void goto_fence_inserter_parse_optionst::get_goto_program(
138138
if(read_goto_binary(cmdline.args[0],
139139
symbol_table, goto_functions, get_message_handler()))
140140
throw 0;
141-
142-
config.set_from_symbol_table(symbol_table);
143141
}
144142

145143
void goto_fence_inserter_parse_optionst::instrument_goto_program(

0 commit comments

Comments
 (0)