Skip to content

Commit 6aa7d25

Browse files
author
Daniel Kroening
committed
read_goto_binary does not set the config
Fixes #2949 This enables auto-detecting the architecture of a goto-binary when performing transformations on it, e.g., with main.c: int main(){ char buffer[] = "a"; int x = strlen(buffer); return x; } the commands goto-cc -m32 -o main.gb main.c goto-instrument --add-library main.gb main2.gb now pass.
1 parent 5565441 commit 6aa7d25

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -898,14 +898,16 @@ void goto_instrument_parse_optionst::get_goto_program()
898898
{
899899
status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;
900900

901+
config.set(cmdline);
902+
901903
auto result = read_goto_binary(cmdline.args[0], get_message_handler());
902904

903905
if(!result.has_value())
904906
throw 0;
905907

906908
goto_model = std::move(result.value());
907909

908-
config.set(cmdline);
910+
config.set_from_symbol_table(goto_model.symbol_table);
909911
}
910912

911913
void goto_instrument_parse_optionst::instrument_goto_program()

0 commit comments

Comments
 (0)