From 0759129de3c490901d2ac461a6441235f6ecbd93 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 22 Mar 2018 11:09:26 +0000 Subject: [PATCH] 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. --- src/cbmc/cbmc_parse_options.cpp | 2 +- src/clobber/clobber_parse_options.cpp | 2 +- src/goto-analyzer/goto_analyzer_parse_options.cpp | 2 +- src/goto-instrument/goto_instrument_parse_options.cpp | 2 +- src/goto-programs/show_goto_functions.h | 4 ++-- src/java_bytecode/java_bytecode_language.h | 2 ++ src/jbmc/jbmc_parse_options.cpp | 5 ++++- 7 files changed, 12 insertions(+), 7 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 14a92fb6117..100c83c2abf 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/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" diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index fa04de3bed2..05d9c3f75f0 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/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" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 75dbc2617ae..2e7cddeb793 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/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" diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index a371065d8f6..d5224337440 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/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(*) diff --git a/src/goto-programs/show_goto_functions.h b/src/goto-programs/show_goto_functions.h index 9935f3f75d2..db1510db64b 100644 --- a/src/goto-programs/show_goto_functions.h +++ b/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( diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index 04a70935f37..61faeddaed3 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -52,6 +52,8 @@ Author: Daniel Kroening, kroening@kroening.com " --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(*) */ \ diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 0cd241a8cad..25cce4cacd1 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/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