Skip to content

Commit 1575958

Browse files
thomasspriggsNlightNFotis
authored andcommitted
Combine NEGATIVE and POSITIVE check macros
This allows for parsing the whole set of options regardless of whether the default is true or false. This then simplifies the usage of the macro as the separate option parsing no longer depends on if "no-standard-checks" is specified.
1 parent 9b52a38 commit 1575958

File tree

4 files changed

+13
-39
lines changed

4 files changed

+13
-39
lines changed

src/ansi-c/goto_check_c.h

Lines changed: 13 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -94,27 +94,12 @@ void goto_check_c(
9494
" {y--assert-to-assume} \t convert user assertions to assumptions\n"
9595
// clang-format on
9696

97-
// clang-format off
98-
#define PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options) \
99-
options.set_option("bounds-check", !cmdline.isset("no-bounds-check")); \
100-
options.set_option("pointer-check", !cmdline.isset("no-pointer-check")); \
101-
options.set_option("div-by-zero-check", !cmdline.isset("no-div-by-zero-check")); \
102-
options.set_option("signed-overflow-check", !cmdline.isset("no-signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \
103-
options.set_option("undefined-shift-check", !cmdline.isset("no-undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \
104-
options.set_option("pointer-primitive-check", !cmdline.isset("no-pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \
105-
(void) 0;
106-
// clang-format on
107-
108-
// clang-format off
109-
#define PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options) \
110-
options.set_option("bounds-check", cmdline.isset("bounds-check")); \
111-
options.set_option("pointer-check", cmdline.isset("pointer-check")); \
112-
options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
113-
options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \
114-
options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \
115-
options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \
116-
(void) 0;
117-
// clang-format on
97+
#define PARSE_OPTION_OVERRIDE(cmdline, options, option) \
98+
if(cmdline.isset(option)) \
99+
options.set_option(option, true); \
100+
if(cmdline.isset("no-" option)) \
101+
options.set_option(option, false); \
102+
(void)0
118103

119104
// clang-format off
120105
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
@@ -134,7 +119,13 @@ void goto_check_c(
134119
options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \
135120
options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \
136121
if(cmdline.isset("error-label")) \
137-
options.set_option("error-label", cmdline.get_values("error-label")); \
122+
options.set_option("error-label", cmdline.get_values("error-label")); \
123+
PARSE_OPTION_OVERRIDE(cmdline, options, "bounds-check"); \
124+
PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-check"); \
125+
PARSE_OPTION_OVERRIDE(cmdline, options, "div-by-zero-check"); \
126+
PARSE_OPTION_OVERRIDE(cmdline, options, "signed-overflow-check"); \
127+
PARSE_OPTION_OVERRIDE(cmdline, options, "undefined-shift-check"); \
128+
PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-primitive-check"); \
138129
(void)0
139130
// clang-format on
140131

src/cbmc/cbmc_parse_options.cpp

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -353,14 +353,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
353353
config.ansi_c.malloc_failure_mode =
354354
configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null;
355355
}
356-
PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options);
357-
}
358-
else if(cmdline.isset("no-standard-checks"))
359-
{
360-
PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options);
361-
// If the user opts for no standard checks, it's safe to assume he also
362-
// wants to control the malloc failure behaviour, in which case we can
363-
// also assume that it's going to be setup in the `config.set` call above.
364356
}
365357

366358
// all (other) checks supported by goto_check

src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -107,14 +107,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
107107
config.ansi_c.malloc_failure_mode =
108108
configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null;
109109
}
110-
PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options);
111-
}
112-
else if(cmdline.isset("no-standard-checks"))
113-
{
114-
PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options);
115-
// If the user opts for no standard checks, it's safe to assume he also
116-
// wants to control the malloc failure behaviour, in which case we can
117-
// also assume that it's going to be setup in the `config.set` call above.
118110
}
119111

120112
// all (other) checks supported by goto_check

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1026,7 +1026,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
10261026
options.set_option("simplify", true);
10271027

10281028
// all checks supported by goto_check
1029-
PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options);
10301029
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
10311030

10321031
// initialize argv with valid pointers

0 commit comments

Comments
 (0)