Skip to content

Document all {goto-,j}analyzer options #6929

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

Merged
merged 2 commits into from
Jun 14, 2022
Merged

Document all {goto-,j}analyzer options #6929

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fb9b749
Remove unsupported --show-reachable-properties
tautschnig Jun 14, 2022
06350a0
Document all {goto-,j}analyzer options
tautschnig Jun 14, 2022
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
14 changes: 12 additions & 2 deletions jbmc/src/janalyzer/janalyzer_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -744,6 +744,8 @@ void janalyzer_parse_optionst::help()
" --verify use the abstract domains to check assertions\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --simplify file_name use the abstract domains to simplify the program\n"
" --no-simplify-slicing do not remove instructions from which no\n"
" property can be reached (use with --simplify)\n" // NOLINT(*)
" --unreachable-instructions list dead code\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --unreachable-functions list functions unreachable from the entry point\n"
Expand All @@ -757,8 +759,9 @@ void janalyzer_parse_optionst::help()
"\n"
"Domain options:\n"
" --constants constant domain\n"
" --intervals interval domain\n"
" --non-null non-null domain\n"
" --intervals, --show-intervals\n"
Copy link
Member

Choose a reason for hiding this comment

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

💡 Looks as if there should be a common definition of these options somewhere. Non-blocking.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Ack, but actually there's quite a lot more that seems to be duplicated across goto-analyzer and janalyzer. A variant of goto-checker would be nice :-) So I'll leave this as-is for now, but will put it in my backlog.

Copy link
Collaborator

Choose a reason for hiding this comment

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

A. There is a lot that could be refactored between the two. I guess I hadn't because of concern about breaking out-of-tree janalyzer patches. But, yeah, could look at that post-marking.
B. The --show-* options are legacy. The goal is to "orthogonalize" the options so it is --show --intervals. I would rather these were removed (along with their complex option parsing) than documented.

" interval domain\n"
" --non-null, --show-non-null non-null domain\n"
" --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
"\n"
"Output options:\n"
Expand All @@ -771,10 +774,15 @@ void janalyzer_parse_optionst::help()
"Specific analyses:\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --taint file_name perform taint analysis using rules in given file\n"
" --show-taint print taint analysis results on stdout\n"
" --show-local-may-alias perform procedure-local may alias analysis\n"
"\n"
"Java Bytecode frontend options:\n"
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
"\n"
"Platform options:\n"
HELP_CONFIG_PLATFORM
"\n"
"Program representations:\n"
" --show-parse-tree show parse tree\n"
" --show-symbol-table show loaded symbol table\n"
Expand All @@ -784,9 +792,11 @@ void janalyzer_parse_optionst::help()
"Program instrumentation options:\n"
" --no-assertions ignore user assertions\n"
" --no-assumptions ignore user assumptions\n"
" --property id enable selected properties only\n"
"\n"
"Other options:\n"
" --version show version and exit\n"
" --verbosity # verbosity level\n"
HELP_TIMESTAMP
"\n";
// clang-format on
Expand Down
3 changes: 1 addition & 2 deletions jbmc/src/janalyzer/janalyzer_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,9 +128,8 @@ class optionst;
OPT_SHOW_GOTO_FUNCTIONS \
OPT_SHOW_PROPERTIES \
"(no-assertions)(no-assumptions)" \
"(show-loops)" \
"(show-symbol-table)(show-parse-tree)" \
"(show-reachable-properties)(property):" \
"(property):" \
"(verbosity):(version)" \
"(arch):" \
"(taint):(show-taint)" \
Expand Down
18 changes: 14 additions & 4 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 @@ -691,7 +691,7 @@ void goto_analyzer_parse_optionst::help()
"\n"
"Usage: Purpose:\n"
"\n"
" goto-analyzer [-h] [--help] show help\n"
" goto-analyzer [-?|-h|--help] show help\n"
" goto-analyzer file.c ... source file names\n"
"\n"
"Task options:\n"
Expand All @@ -701,6 +701,8 @@ void goto_analyzer_parse_optionst::help()
" --verify use the abstract domains to check assertions\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --simplify file_name use the abstract domains to simplify the program\n"
" --no-simplify-slicing do not remove instructions from which no\n"
" property can be reached (use with --simplify)\n" // NOLINT(*)
" --unreachable-instructions list dead code\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --unreachable-functions list functions unreachable from the entry point\n"
Expand All @@ -716,6 +718,8 @@ void goto_analyzer_parse_optionst::help()
" --legacy-ait recursion for function and one domain per location\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --legacy-concurrent legacy-ait with an extended fixed-point for concurrency\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --location-sensitive use location-sensitive abstract interpreter\n"
"\n"
"History options:\n"
// NOLINTNEXTLINE(whitespace/line_length)
Expand All @@ -739,10 +743,12 @@ void goto_analyzer_parse_optionst::help()
"\n"
"Domain options:\n"
" --constants a constant for each variable if possible\n"
" --intervals an interval for each variable\n"
" --non-null tracks which pointers are non-null\n"
" --intervals, --show-intervals\n"
" an interval for each variable\n"
" --non-null, --show-non-null tracks which pointers are non-null\n"
" --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
" --vsd a configurable non-relational domain\n" // NOLINT(*)
" --vsd, --variable-sensitivity\n"
" a configurable non-relational domain\n"
" --dependence-graph-vs dependencies between instructions using VSD\n" // NOLINT(*)
"\n"
"Variable sensitivity domain (VSD) options:\n"
Expand All @@ -763,6 +769,8 @@ void goto_analyzer_parse_optionst::help()
"Specific analyses:\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --taint file_name perform taint analysis using rules in given file\n"
" --show-taint print taint analysis results on stdout\n"
" --show-local-may-alias perform procedure-local may alias analysis\n"
"\n"
"C/C++ frontend options:\n"
HELP_CONFIG_C_CPP
Expand All @@ -778,13 +786,15 @@ void goto_analyzer_parse_optionst::help()
HELP_SHOW_PROPERTIES
"\n"
"Program instrumentation options:\n"
" --property id enable selected properties only\n"
HELP_GOTO_CHECK
HELP_CONFIG_LIBRARY
"\n"
"Other options:\n"
HELP_VALIDATE
" --version show version and exit\n"
HELP_FLUSH
" --verbosity # verbosity level\n"
HELP_TIMESTAMP
"\n";
// clang-format on
Expand Down
3 changes: 1 addition & 2 deletions 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 @@ -151,9 +151,8 @@ class optionst;
OPT_SHOW_GOTO_FUNCTIONS \
OPT_SHOW_PROPERTIES \
OPT_GOTO_CHECK \
"(show-loops)" \
"(show-symbol-table)(show-parse-tree)" \
"(show-reachable-properties)(property):" \
"(property):" \
"(verbosity):(version)" \
OPT_FLUSH \
OPT_TIMESTAMP \
Expand Down