Skip to content

Commit 6b3e32d

Browse files
author
martin
committed
Replace the use of cmdline with options in goto-analyzer and goto-diff
This uncovered a bug in goto-analyzer where the options for goto-check are recognised but not actually parsed.
1 parent cf0554b commit 6b3e32d

File tree

2 files changed

+5
-2
lines changed

2 files changed

+5
-2
lines changed

src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -147,6 +147,9 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
147147
options.set_option("error-label", cmdline.get_values("error-label"));
148148
#endif
149149

150+
// all checks supported by goto_check
151+
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
152+
150153
// The user should either select:
151154
// 1. a specific analysis, or
152155
// 2. a tuple of task / analyser options / outputs
@@ -894,7 +897,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
894897
log.status() << "Removing function pointers and virtual functions"
895898
<< messaget::eom;
896899
remove_function_pointers(
897-
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
900+
ui_message_handler, goto_model, options.get_bool_option("pointer-check"));
898901

899902
// instrument library preconditions
900903
instrument_preconditions(goto_model);

src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -340,7 +340,7 @@ bool goto_diff_parse_optionst::process_goto_program(
340340
log.status() << "Removal of function pointers and virtual functions"
341341
<< messaget::eom;
342342
remove_function_pointers(
343-
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
343+
ui_message_handler, goto_model, options.get_bool_option("pointer-check"));
344344

345345
mm_io(goto_model);
346346

0 commit comments

Comments
 (0)