Skip to content

Commit 38fe61e

Browse files
peterschrammelpeterschrammel
committed
Trim JBMC help text width to 80 chars
1 parent 080fc91 commit 38fe61e

File tree

2 files changed

+43
-37
lines changed

2 files changed

+43
-37
lines changed

‎jbmc/src/java_bytecode/java_bytecode_language.h‎

Lines changed: 33 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -35,43 +35,47 @@ Author: Daniel Kroening, kroening@kroening.com
3535
"(throw-runtime-exceptions)" \
3636
"(java-max-input-array-length):" /* will go away */ \
3737
"(max-nondet-array-length):" \
38-
"(java-max-input-tree-depth):" /* will go away */ \
38+
"(java-max-input-tree-depth):" /* will go away */ \
3939
"(max-nondet-tree-depth):" \
4040
"(java-max-vla-length):" \
4141
"(java-cp-include-files):" \
42-
"(lazy-methods)" /* will go away */ \
42+
"(lazy-methods)" /* will go away */ \
4343
"(no-lazy-methods)" \
4444
"(lazy-methods-extra-entry-point):" \
4545
"(java-load-class):" \
4646
"(java-no-load-class):"
4747

48-
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \
49-
" --disable-uncaught-exception-check" \
50-
" ignore uncaught exceptions and errors\n" \
51-
" --throw-assertion-error throw java.lang.AssertionError on violated\n" /* NOLINT(*) */ \
52-
" assert statements instead of failing\n" \
53-
" at the location of the assert statement\n" /* NOLINT(*) */ \
54-
" --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \
55-
" entry point with null\n" /* NOLINT(*) */ \
56-
" --throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \
57-
" --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \
58-
" --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
59-
" at level N references are set to null\n" /* NOLINT(*) */ \
60-
" --java-max-vla-length limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
61-
" --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n" /* NOLINT(*) */ \
62-
" --no-lazy-methods load and translate all methods given on the command line\n" /* NOLINT(*) */ \
63-
" and in --classpath\n" /* NOLINT(*) */ \
64-
" Default is to load methods that appear to be\n" /* NOLINT(*) */ \
65-
" reachable from the --function entry point or main class\n" /* NOLINT(*) */ \
66-
" Note --show-symbol-table/goto-functions/properties output\n"/* NOLINT(*) */ \
67-
" are restricted to loaded methods by default\n" /* NOLINT(*) */ \
68-
" --lazy-methods-extra-entry-point METHODNAME\n" /* NOLINT(*) */ \
69-
" treat METHODNAME as a possible program entry point for\n" /* NOLINT(*) */ \
70-
" the purpose of lazy method loading\n" /* NOLINT(*) */ \
71-
" METHODNAME can be a regex that will be matched against\n" /* NOLINT(*) */ \
72-
" all symbols. If missing a java:: prefix will be added\n" /* NOLINT(*) */ \
73-
" If no descriptor is found, all overloads of a method will\n"/* NOLINT(*) */ \
74-
" also be added." /* NOLINT(*) */
48+
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \
49+
" --disable-uncaught-exception-check\n" \
50+
" ignore uncaught exceptions and errors\n" \
51+
" --throw-assertion-error throw java.lang.AssertionError on violated\n" \
52+
" assert statements instead of failing\n" \
53+
" at the location of the assert statement\n" \
54+
" --throw-runtime-exceptions make implicit runtime exceptions explicit\n" \
55+
" --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \
56+
" --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
57+
" at level N references are set to null\n" /* NOLINT(*) */ \
58+
" --java-assume-inputs-non-null\n" \
59+
" never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \
60+
" entry point with null\n" /* NOLINT(*) */ \
61+
" --java-max-vla-length N limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
62+
" --java-cp-include-files r regexp or JSON list of files to load\n" \
63+
" (with '@' prefix)\n" \
64+
" --no-lazy-methods load and translate all methods given on\n" \
65+
" the command line and in --classpath\n" \
66+
" Default is to load methods that appear to be\n" /* NOLINT(*) */ \
67+
" reachable from the --function entry point\n" \
68+
" or main class\n" \
69+
" Note that --show-symbol-table, --show-goto-functions\n" /* NOLINT(*) */ \
70+
" and --show-properties output are restricted to\n" /* NOLINT(*) */ \
71+
" loaded methods by default.\n" \
72+
" --lazy-methods-extra-entry-point METHODNAME\n" \
73+
" treat METHODNAME as a possible program entry\n" /* NOLINT(*) */ \
74+
" point for the purpose of lazy method loading\n" /* NOLINT(*) */ \
75+
" METHODNAME can be a regex that will be matched\n" /* NOLINT(*) */ \
76+
" against all symbols. If missing a java:: prefix\n" /* NOLINT(*) */ \
77+
" will be added. If no descriptor is found, all\n"/* NOLINT(*) */ \
78+
" overloads of a method will also be added.\n"
7579
// clang-format on
7680

7781
class symbolt;

‎jbmc/src/jbmc/jbmc_parse_options.cpp‎

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1070,7 +1070,8 @@ void jbmc_parse_optionst::help()
10701070
" --show-parse-tree show parse tree\n"
10711071
" --show-symbol-table show loaded symbol table\n"
10721072
HELP_SHOW_GOTO_FUNCTIONS
1073-
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1073+
" --drop-unused-functions drop functions trivially unreachable\n"
1074+
" from main function\n"
10741075
HELP_SHOW_CLASS_HIERARCHY
10751076
"\n"
10761077
"Program instrumentation options:\n"
@@ -1088,13 +1089,14 @@ void jbmc_parse_optionst::help()
10881089
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
10891090
// This one is handled by jbmc_parse_options not by the Java frontend,
10901091
// hence its presence here:
1091-
" --java-threading enable experimental support for java multi-threading\n"// NOLINT(*)
1092-
" --java-unwind-enum-static try to unwind loops in static initialization of enums\n" // NOLINT(*)
1092+
" --java-threading enable java multi-threading support (experimental)\n" // NOLINT(*)
1093+
" --java-unwind-enum-static unwind loops in static initialization of enums\n" // NOLINT(*)
10931094
// Currently only supported in the JBMC frontend:
1094-
" --symex-driven-lazy-loading only load functions when first entered by symbolic execution\n" // NOLINT(*)
1095-
" Note --show-symbol-table/goto-functions/properties output\n" // NOLINT(*)
1096-
" will be restricted to loaded methods in this case, and only\n" // NOLINT(*)
1097-
" output after the symex phase\n"
1095+
" --symex-driven-lazy-loading only load functions when first entered by symbolic\n" // NOLINT(*)
1096+
" execution. Note that --show-symbol-table,\n"
1097+
" --show-goto-functions/properties output\n"
1098+
" will be restricted to loaded methods in this case,\n" // NOLINT(*)
1099+
" and only output after the symex phase.\n"
10981100
"\n"
10991101
"BMC options:\n"
11001102
HELP_BMC
@@ -1113,7 +1115,7 @@ void jbmc_parse_optionst::help()
11131115
" --z3 use Z3\n"
11141116
" --refine use refinement procedure (experimental)\n"
11151117
" --no-refine-strings turn off string refinement\n"
1116-
" --string-printable add constraint that strings are printable (experimental)\n" // NOLINT(*)
1118+
" --string-printable restrict to printable strings (experimental)\n" // NOLINT(*)
11171119
" --max-nondet-string-length bound the length of nondet (e.g. input) strings\n" // NOLINT(*)
11181120
" --outfile filename output formula to given file\n"
11191121
" --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)

0 commit comments

Comments
 (0)