Merge pull request #1957 from smowton/smowton/cleanup/show-goto-functions-documentation

Clarify slightly that show-symbol-table et al are restricted to loaded symbols

Author: smowton

src/cbmc/cbmc_parse_options.cpp

@@ -942,7 +942,7 @@ void cbmc_parse_optionst::help()
     "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"
-    " --show-symbol-table          show symbol table\n"
+    " --show-symbol-table          show loaded symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"

src/clobber/clobber_parse_options.cpp

@@ -398,7 +398,7 @@ void clobber_parse_optionst::help()
     " --big-endian                 allow big-endian word-byte conversions\n"
     " --unsigned-char              make \"char\" unsigned by default\n"
     " --show-parse-tree            show parse tree\n"
-    " --show-symbol-table          show symbol table\n"
+    " --show-symbol-table          show loaded symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
     " --ppc-macos                  set MACOS/PPC architecture\n"
     " --mm model                   set memory model (default: sc)\n"

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -896,7 +896,7 @@ void goto_analyzer_parse_optionst::help()
     "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"
-    " --show-symbol-table          show symbol table\n"
+    " --show-symbol-table          show loaded symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
     HELP_SHOW_PROPERTIES
     "\n"

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1480,7 +1480,7 @@ void goto_instrument_parse_optionst::help()
     "Diagnosis:\n"
     " --show-loops                 show the loops in the program\n"
     HELP_SHOW_PROPERTIES
-    " --show-symbol-table          show symbol table\n"
+    " --show-symbol-table          show loaded symbol table\n"
     " --list-symbols               list symbols with type information\n"
     HELP_SHOW_GOTO_FUNCTIONS
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)

src/goto-programs/show_goto_functions.h

@@ -24,8 +24,8 @@ class goto_functionst;
   "(list-goto-functions)"
 
 #define HELP_SHOW_GOTO_FUNCTIONS \
-  " --show-goto-functions        show goto program\n" \
-  " --list-goto-functions        list goto functions\n"
+  " --show-goto-functions        show loaded goto program\n" \
+  " --list-goto-functions        list loaded goto functions\n"
 // clang-format on
 
 void show_goto_functions(

src/java_bytecode/java_bytecode_language.h

@@ -52,6 +52,8 @@ Author: Daniel Kroening, [email protected]
   " --java-cp-include-files          regexp or JSON list of files to load (with '@' prefix)\n"   /* NOLINT(*) */ \
   " --lazy-methods                   only translate methods that appear to be reachable from\n"  /* NOLINT(*) */ \
   "                                  the --function entry point or main class\n"                 /* NOLINT(*) */ \
+  "                                  Note --show-symbol-table/goto-functions/properties output\n"/* NOLINT(*) */ \
+  "                                  will be restricted to loaded methods in this case\n"        /* NOLINT(*) */ \
   " --lazy-methods-extra-entry-point METHODNAME\n"                                               /* NOLINT(*) */ \
   "                                  treat METHODNAME as a possible program entry point for\n"   /* NOLINT(*) */ \
   "                                  the purpose of lazy method loading\n"                       /* NOLINT(*) */ \

src/jbmc/jbmc_parse_options.cpp

@@ -1027,7 +1027,7 @@ void jbmc_parse_optionst::help()
     "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"
-    " --show-symbol-table          show symbol table\n"
+    " --show-symbol-table          show loaded symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"
@@ -1050,6 +1050,9 @@ void jbmc_parse_optionst::help()
     " --java-unwind-enum-static    try to unwind loops in static initialization of enums\n" // NOLINT(*)
     // Currently only supported in the JBMC frontend:
     " --symex-driven-lazy-loading  only load functions when first entered by symbolic execution\n" // NOLINT(*)
+    "                              Note --show-symbol-table/goto-functions/properties output\n" // NOLINT(*)
+    "                              will be restricted to loaded methods in this case, and only\n" // NOLINT(*)
+    "                              output after the symex phase\n"
     "\n"
     "BMC options:\n"
     HELP_BMC