Skip to content

Commit 52c6ad4

Browse files
committed
Use help_entry() for help of new --allocate-size-check option
Also adapt the help messages of all the tools to work with the macro HELP_GOTO_CHECK using help_entry()
1 parent c8b29ff commit 52c6ad4

File tree

5 files changed

+5
-5
lines changed

5 files changed

+5
-5
lines changed

src/analyses/goto_check.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ void goto_check(
5858
" --no-built-in-assertions ignore assertions in built-in library\n" \
5959
" --enum-range-check checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \
6060
" --pointer-primitive-check checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */ \
61-
" --allocate-size-check checks that not more memory is allocated than can be addressed by cbmc" /* NOLINT(whitespace/line_length) */
61+
<< help_entry("--allocate-size-check", "checks that not more memory is allocated than can be addressed by cbmc") /* NOLINT(whitespace/line_length) */
6262

6363
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
6464
options.set_option("bounds-check", cmdline.isset("bounds-check")); \

src/cbmc/cbmc_parse_options.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -1067,7 +1067,7 @@ void cbmc_parse_optionst::help()
10671067
HELP_SHOW_GOTO_FUNCTIONS
10681068
"\n"
10691069
"Program instrumentation options:\n"
1070-
HELP_GOTO_CHECK
1070+
<< HELP_GOTO_CHECK <<
10711071
" --no-assertions ignore user assertions\n"
10721072
" --no-assumptions ignore user assumptions\n"
10731073
" --error-label label check that label is unreachable\n"

src/goto-analyzer/goto_analyzer_parse_options.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -916,7 +916,7 @@ void goto_analyzer_parse_optionst::help()
916916
HELP_SHOW_PROPERTIES
917917
"\n"
918918
"Program instrumentation options:\n"
919-
HELP_GOTO_CHECK
919+
<< HELP_GOTO_CHECK <<
920920
"\n"
921921
"Other options:\n"
922922
HELP_VALIDATE

src/goto-diff/goto_diff_parse_options.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -407,7 +407,7 @@ void goto_diff_parse_optionst::help()
407407
" --compact-output output dependencies in compact mode\n"
408408
"\n"
409409
"Program instrumentation options:\n"
410-
HELP_GOTO_CHECK
410+
<< HELP_GOTO_CHECK <<
411411
" --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
412412
"Other options:\n"
413413
" --version show version and exit\n"

src/goto-instrument/goto_instrument_parse_options.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -1792,7 +1792,7 @@ void goto_instrument_parse_optionst::help()
17921792
"\n"
17931793
"Safety checks:\n"
17941794
" --no-assertions ignore user assertions\n"
1795-
HELP_GOTO_CHECK
1795+
<< HELP_GOTO_CHECK <<
17961796
" --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*)
17971797
" --error-label label check that label is unreachable\n"
17981798
" --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)

0 commit comments

Comments
 (0)