Skip to content

Commit 9e1705f

Browse files
Enable list-goto-functions in CBMC
1 parent ebd8248 commit 9e1705f

File tree

2 files changed

+13
-3
lines changed

2 files changed

+13
-3
lines changed

src/cbmc/cbmc_parse_options.cpp

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -636,9 +636,14 @@ int cbmc_parse_optionst::get_goto_program(
636636
}
637637

638638
// show it?
639-
if(cmdline.isset("show-goto-functions"))
639+
if(
640+
cmdline.isset("show-goto-functions") ||
641+
cmdline.isset("list-goto-functions"))
640642
{
641-
show_goto_functions(goto_model, ui_message_handler.get_ui());
643+
show_goto_functions(
644+
goto_model,
645+
ui_message_handler.get_ui(),
646+
cmdline.isset("list-goto-functions"));
642647
return CPROVER_EXIT_SUCCESS;
643648
}
644649

@@ -897,6 +902,7 @@ int cbmc_parse_optionst::do_bmc(bmct &bmc)
897902
/// display command line help
898903
void cbmc_parse_optionst::help()
899904
{
905+
// clang-format off
900906
std::cout <<
901907
"\n"
902908
"* * CBMC " CBMC_VERSION " - Copyright (C) 2001-2017 ";
@@ -1025,4 +1031,5 @@ void cbmc_parse_optionst::help()
10251031
HELP_GOTO_TRACE
10261032
" --verbosity # verbosity level\n"
10271033
"\n";
1034+
// clang-format on
10281035
}

src/cbmc/cbmc_parse_options.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ class bmct;
2626
class goto_functionst;
2727
class optionst;
2828

29+
// clang-format off
2930
#define CBMC_OPTIONS \
3031
"(program-only)(preprocess)(slice-by-trace):" \
3132
OPT_FUNCTIONS \
@@ -50,7 +51,8 @@ class optionst;
5051
"(string-max-input-length):" \
5152
"(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
5253
"(little-endian)(big-endian)" \
53-
"(show-goto-functions)(show-loops)" \
54+
OPT_SHOW_GOTO_FUNCTIONS \
55+
"(show-loops)" \
5456
"(show-symbol-table)(show-parse-tree)(show-vcc)" \
5557
"(show-claims)(claim):(show-properties)" \
5658
"(drop-unused-functions)" \
@@ -69,6 +71,7 @@ class optionst;
6971
"(localize-faults)(localize-faults-method):" \
7072
OPT_GOTO_TRACE \
7173
"(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
74+
// clang-format on
7275

7376
class cbmc_parse_optionst:
7477
public parse_options_baset,

0 commit comments

Comments
 (0)