Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Enable logging of default flags on tool invocation #8110

Closed
wants to merge 1 commit into from
Closed

Enable logging of default flags on tool invocation #8110

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 26 additions & 2 deletions src/cbmc/cbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,8 @@ void cbmc_parse_optionst::set_default_options(optionst &options)

void cbmc_parse_optionst::set_default_analysis_flags(
optionst &options,
const bool enabled)
const bool enabled,
const messaget &log)
{
// Checks enabled by default in v6.0+.
options.set_option("bounds-check", enabled);
Expand All @@ -121,6 +122,29 @@ void cbmc_parse_optionst::set_default_analysis_flags(
// Unwinding assertions required in certain cases for sound verification
// results. See https://github.com/diffblue/cbmc/issues/6561 for elaboration.
options.set_option("unwinding-assertions", enabled);

if(enabled)
{
log.status() << "Running with --standard-checks on: "
<< "bounds-check, pointer-check, pointer-primitive-check, "
"div-by-zero-check, "
<< "signed-overflow-check, undefined-shift-check and "
"unwinding-assertions are"
<< "**on** by default for this analysis run.\n"
<< messaget::eom;
;
}
else
{ // enabled == false
log.status() << "Running with --no-standard-checks on: "
<< "bounds-check, pointer-check, pointer-primitive-check, "
"div-by-zero-check, "
<< "signed-overflow-check, undefined-shift-check and "
"unwinding-assertions are "
<< "**off** by default for this analysis run.\n"
<< messaget::eom;
;
}
Comment on lines +125 to +147
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we perhaps do better in the sense that we log the checks that are actually on, rather than just listing the defaults. That is, IMHO --no-standard-checks --pointer-check should produce an output different from the above.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, the intention was to list the checks that are actually enabled.

}

void cbmc_parse_optionst::get_command_line_options(optionst &options)
Expand Down Expand Up @@ -335,7 +359,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
// Enable flags that in combination provide analysis with no surprises
// (expected checks and no unsoundness by missing checks).
cbmc_parse_optionst::set_default_analysis_flags(
options, !cmdline.isset("no-standard-checks"));
options, !cmdline.isset("no-standard-checks"), log);

// all (other) checks supported by goto_check
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
Expand Down
3 changes: 2 additions & 1 deletion src/cbmc/cbmc_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,8 @@ class cbmc_parse_optionst : public parse_options_baset
///
/// This function sets up the default analysis checks as discussed
/// in RFC https://github.com/diffblue/cbmc/issues/7975.
static void set_default_analysis_flags(optionst &, const bool enabled);
static void
set_default_analysis_flags(optionst &, const bool enabled, const messaget &);
static bool process_goto_program(goto_modelt &, const optionst &, messaget &);

static int get_goto_program(
Expand Down
28 changes: 26 additions & 2 deletions src/goto-analyzer/goto_analyzer_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,8 @@ goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(

void goto_analyzer_parse_optionst::set_default_analysis_flags(
optionst &options,
const bool enabled)
const bool enabled,
const messaget &log)
{
// Checks enabled by default in v6.0+.
options.set_option("bounds-check", enabled);
Expand All @@ -71,6 +72,29 @@ void goto_analyzer_parse_optionst::set_default_analysis_flags(
// This is in-line with the options we set for CBMC in cbmc_parse_optionst
// with the exception of unwinding-assertions, which don't make sense in
// the context of abstract interpretation.

if(enabled)
{
log.status()
<< "Running with --standard-checks on: "
<< "bounds-check, pointer-check, pointer-primitive-check, "
"div-by-zero-check, "
<< "signed-overflow-check and undefined-shift-check are **on** by "
<< "default for this analysis run.\n"
<< messaget::eom;
;
}
else
{ // enabled == false
log.status()
<< "Running with --no-standard-checks on: "
<< "bounds-check, pointer-check, pointer-primitive-check, "
"div-by-zero-check, "
<< "signed-overflow-check and undefined-shift-check are **off** by "
<< "default for this analysis run.\n"
<< messaget::eom;
;
}
}

void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
Expand All @@ -85,7 +109,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
options.set_option("function", cmdline.get_value("function"));

goto_analyzer_parse_optionst::set_default_analysis_flags(
options, !cmdline.isset("no-standard-checks"));
options, !cmdline.isset("no-standard-checks"), log);

// all (other) checks supported by goto_check
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
Expand Down
3 changes: 2 additions & 1 deletion src/goto-analyzer/goto_analyzer_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,8 @@ class goto_analyzer_parse_optionst: public parse_options_baset
virtual int perform_analysis(const optionst &options);

// TODO: Add documentation
static void set_default_analysis_flags(optionst &options, const bool enabled);
static void
set_default_analysis_flags(optionst &options, const bool enabled, const messaget &);
};

#endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H