read_goto_binary does not set the config

Daniel Kroening · Daniel Kroening · commit a816370278bf · 2018-09-18T18:07:04.000+01:00
Fixes #2949
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -898,14 +898,16 @@ void goto_instrument_parse_optionst::get_goto_program()
 {
   status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;
 
+  config.set(cmdline);
+
   auto result = read_goto_binary(cmdline.args[0], get_message_handler());
 
   if(!result.has_value())
     throw 0;
 
   goto_model = std::move(result.value());
 
-  config.set(cmdline);
+  config.set_from_symbol_table(goto_model.symbol_table);
 }
 
 void goto_instrument_parse_optionst::instrument_goto_program()

Original file line number	Diff line number	Diff line change
`@@ -898,14 +898,16 @@ void goto_instrument_parse_optionst::get_goto_program()`
`898`	`898`	`{`
`899`	`899`	status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;
`900`	`900`
	`901`	`+ config.set(cmdline);`
	`902`	`+`
`901`	`903`	`auto result = read_goto_binary(cmdline.args[0], get_message_handler());`
`902`	`904`
`903`	`905`	`if(!result.has_value())`
`904`	`906`	`throw 0;`
`905`	`907`
`906`	`908`	`goto_model = std::move(result.value());`
`907`	`909`
`908`		`- config.set(cmdline);`
	`910`	`+ config.set_from_symbol_table(goto_model.symbol_table);`
`909`	`911`	`}`
`910`	`912`
`911`	`913`	`void goto_instrument_parse_optionst::instrument_goto_program()`