Skip to content

Commit a699a45

Browse files
committed
Clarify slightly that show-symbol-table et al are restricted to loaded symbols
Specifically they interact with --lazy-methods, --symex-driven-lazy-loading (where the driver program supports them) such that only loaded functions (and other symbols) are displayed.
1 parent f6219d4 commit a699a45

File tree

6 files changed

+7
-7
lines changed

6 files changed

+7
-7
lines changed

src/cbmc/cbmc_parse_options.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -915,7 +915,7 @@ void cbmc_parse_optionst::help()
915915
"\n"
916916
"Program representations:\n"
917917
" --show-parse-tree show parse tree\n"
918-
" --show-symbol-table show symbol table\n"
918+
" --show-symbol-table show loaded symbol table\n"
919919
HELP_SHOW_GOTO_FUNCTIONS
920920
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
921921
"\n"

src/clobber/clobber_parse_options.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -398,7 +398,7 @@ void clobber_parse_optionst::help()
398398
" --big-endian allow big-endian word-byte conversions\n"
399399
" --unsigned-char make \"char\" unsigned by default\n"
400400
" --show-parse-tree show parse tree\n"
401-
" --show-symbol-table show symbol table\n"
401+
" --show-symbol-table show loaded symbol table\n"
402402
HELP_SHOW_GOTO_FUNCTIONS
403403
" --ppc-macos set MACOS/PPC architecture\n"
404404
" --mm model set memory model (default: sc)\n"

src/goto-analyzer/goto_analyzer_parse_options.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -896,7 +896,7 @@ void goto_analyzer_parse_optionst::help()
896896
"\n"
897897
"Program representations:\n"
898898
" --show-parse-tree show parse tree\n"
899-
" --show-symbol-table show symbol table\n"
899+
" --show-symbol-table show loaded symbol table\n"
900900
HELP_SHOW_GOTO_FUNCTIONS
901901
HELP_SHOW_PROPERTIES
902902
"\n"

src/goto-instrument/goto_instrument_parse_options.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -1480,7 +1480,7 @@ void goto_instrument_parse_optionst::help()
14801480
"Diagnosis:\n"
14811481
" --show-loops show the loops in the program\n"
14821482
HELP_SHOW_PROPERTIES
1483-
" --show-symbol-table show symbol table\n"
1483+
" --show-symbol-table show loaded symbol table\n"
14841484
" --list-symbols list symbols with type information\n"
14851485
HELP_SHOW_GOTO_FUNCTIONS
14861486
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)

src/goto-programs/show_goto_functions.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,8 @@ class goto_functionst;
2424
"(list-goto-functions)"
2525

2626
#define HELP_SHOW_GOTO_FUNCTIONS \
27-
" --show-goto-functions show goto program\n" \
28-
" --list-goto-functions list goto functions\n"
27+
" --show-goto-functions show loaded goto program\n" \
28+
" --list-goto-functions list loaded goto functions\n"
2929
// clang-format on
3030

3131
void show_goto_functions(

src/jbmc/jbmc_parse_options.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -846,7 +846,7 @@ void jbmc_parse_optionst::help()
846846
"\n"
847847
"Program representations:\n"
848848
" --show-parse-tree show parse tree\n"
849-
" --show-symbol-table show symbol table\n"
849+
" --show-symbol-table show loaded symbol table\n"
850850
HELP_SHOW_GOTO_FUNCTIONS
851851
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
852852
"\n"

0 commit comments

Comments
 (0)