replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Trim JBMC help text width to 80 chars

This commit is contained in:
Peter Schrammel 2018-07-15 22:33:34 +01:00
parent 080fc91b0e
commit 38fe61e02e
2 changed files with 43 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

62
jbmc/src/java_bytecode/java_bytecode_language.h
View File

@ -35,43 +35,47 @@ Author: Daniel Kroening, kroening@kroening.com
"(throw-runtime-exceptions)" \
"(java-max-input-array-length):" /* will go away */ \
"(max-nondet-array-length):" \
"(java-max-input-tree-depth):" /* will go away */ \
"(java-max-input-tree-depth):" /* will go away */ \
"(max-nondet-tree-depth):" \
"(java-max-vla-length):" \
"(java-cp-include-files):" \
"(lazy-methods)" /* will go away */ \
"(lazy-methods)" /* will go away */ \
"(no-lazy-methods)" \
"(lazy-methods-extra-entry-point):" \
"(java-load-class):" \
"(java-no-load-class):"
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \
" --disable-uncaught-exception-check" \
" ignore uncaught exceptions and errors\n" \
" --throw-assertion-error throw java.lang.AssertionError on violated\n" /* NOLINT(*) */ \
" assert statements instead of failing\n" \
" at the location of the assert statement\n" /* NOLINT(*) */ \
" --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \
" entry point with null\n" /* NOLINT(*) */ \
" --throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \
" --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \
" --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
" at level N references are set to null\n" /* NOLINT(*) */ \
" --java-max-vla-length limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
" --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n" /* NOLINT(*) */ \
" --no-lazy-methods load and translate all methods given on the command line\n" /* NOLINT(*) */ \
" and in --classpath\n" /* NOLINT(*) */ \
" Default is to load methods that appear to be\n" /* NOLINT(*) */ \
" reachable from the --function entry point or main class\n" /* NOLINT(*) */ \
" Note --show-symbol-table/goto-functions/properties output\n"/* NOLINT(*) */ \
" are restricted to loaded methods by default\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(*) */ \
" METHODNAME can be a regex that will be matched against\n" /* NOLINT(*) */ \
" all symbols. If missing a java:: prefix will be added\n" /* NOLINT(*) */ \
" If no descriptor is found, all overloads of a method will\n"/* NOLINT(*) */ \
" also be added." /* NOLINT(*) */
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \
" --disable-uncaught-exception-check\n" \
" ignore uncaught exceptions and errors\n" \
" --throw-assertion-error throw java.lang.AssertionError on violated\n" \
" assert statements instead of failing\n" \
" at the location of the assert statement\n" \
" --throw-runtime-exceptions make implicit runtime exceptions explicit\n" \
" --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \
" --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
" at level N references are set to null\n" /* NOLINT(*) */ \
" --java-assume-inputs-non-null\n" \
" never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \
" entry point with null\n" /* NOLINT(*) */ \
" --java-max-vla-length N limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
" --java-cp-include-files r regexp or JSON list of files to load\n" \
" (with '@' prefix)\n" \
" --no-lazy-methods load and translate all methods given on\n" \
" the command line and in --classpath\n" \
" Default is to load methods that appear to be\n" /* NOLINT(*) */ \
" reachable from the --function entry point\n" \
" or main class\n" \
" Note that --show-symbol-table, --show-goto-functions\n" /* NOLINT(*) */ \
" and --show-properties output are restricted to\n" /* NOLINT(*) */ \
" loaded methods by default.\n" \
" --lazy-methods-extra-entry-point METHODNAME\n" \
" treat METHODNAME as a possible program entry\n" /* NOLINT(*) */ \
" point for the purpose of lazy method loading\n" /* NOLINT(*) */ \
" METHODNAME can be a regex that will be matched\n" /* NOLINT(*) */ \
" against all symbols. If missing a java:: prefix\n" /* NOLINT(*) */ \
" will be added. If no descriptor is found, all\n"/* NOLINT(*) */ \
" overloads of a method will also be added.\n"
// clang-format on
class symbolt;

18
jbmc/src/jbmc/jbmc_parse_options.cpp
View File

@ -1070,7 +1070,8 @@ void jbmc_parse_optionst::help()
" --show-parse-tree show parse tree\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(*)
" --drop-unused-functions drop functions trivially unreachable\n"
" from main function\n"
HELP_SHOW_CLASS_HIERARCHY
"\n"
"Program instrumentation options:\n"
@ -1088,13 +1089,14 @@ void jbmc_parse_optionst::help()
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
// This one is handled by jbmc_parse_options not by the Java frontend,
// hence its presence here:
" --java-threading enable experimental support for java multi-threading\n"// NOLINT(*)
" --java-unwind-enum-static try to unwind loops in static initialization of enums\n" // NOLINT(*)
" --java-threading enable java multi-threading support (experimental)\n" // NOLINT(*)
" --java-unwind-enum-static 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"
" --symex-driven-lazy-loading only load functions when first entered by symbolic\n" // NOLINT(*)
" execution. Note that --show-symbol-table,\n"
" --show-goto-functions/properties output\n"
" will be restricted to loaded methods in this case,\n" // NOLINT(*)
" and only output after the symex phase.\n"
"\n"
"BMC options:\n"
HELP_BMC
@ -1113,7 +1115,7 @@ void jbmc_parse_optionst::help()
" --z3 use Z3\n"
" --refine use refinement procedure (experimental)\n"
" --no-refine-strings turn off string refinement\n"
" --string-printable add constraint that strings are printable (experimental)\n" // NOLINT(*)
" --string-printable restrict to printable strings (experimental)\n" // NOLINT(*)
" --max-nondet-string-length bound the length of nondet (e.g. input) strings\n" // NOLINT(*)
" --outfile filename output formula to given file\n"
" --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)