Switch CPAchecker to "--long-form" command-line arguments
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