Skip to content

Switch CPAchecker to "--long-form" command-line arguments

Philipp Wendler requested to merge 1218-new-command-line-arguments into trunk

The previous "-argument" style is not as common as "--argument". This MR implements #1218 (closed).

Most command-line arguments keep their name and just gain a dash, some arguments are renamed, and some do not get a new form at all because we consider them unimportant. A table with a mapping from old to new is at #1218 (comment 1950486702).

All old arguments continue to be supported for now (but will become undocumented and produce a warning). A mixture of old and new arguments is also (mostly) not allowed, as discussed in #1218 (comment 1952602398). The concrete rules of what is allowed and not is as follows:

  • Mixture of "-old" and "--new" arguments is forbidden in general except where described below.
  • The arguments -heap, -stack, -debug, -disable-java-assertions and their -- equivalents are always allowed, no matter what style the other arguments have. (Otherwise we would have to implement full argument parsing in shell, which does not seem worth the effort.)
  • Short-form arguments (like -h) are always allowed.
  • Those arguments that do not have a new form (-cbmc, -clang, -cmc, -logfile, -nolog) are always allowed, no matter what style the other arguments have. But we print a warning telling the user that they are deprecated and what they would need to do to replace them (setting some options).
  • -X* is always allowed.
  • If a forbidden mixture is detected, an error message is printed with a map of replacements that the user should perform on their command line.
  • For every occurrence of -heap, -stack, -debug, or -disable-java-assertions a message is printed at the very top of CPAchecker's output telling the user about the replacement.
  • If a command line with "-old" arguments is used, a warning is printed with the map of recommended replacements (except for those arguments covered by other warnings, i.e., from the previous item and those arguments that do not have a direct replacement).

Todos:

  • Implement the desired short forms like -c.
  • Updating documentation, test sets, etc.
  • Updating any scripts that need it besides bin/cpachecker*.
Edited by Philipp Wendler

Merge request reports