From 9ef7cc3520344901a704bda018cd1783ebc18d06 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 14 Dec 2021 13:14:48 -0800 Subject: [PATCH] Make some undocumented options regular/expert (#7805) We have some options that are currently "undocumented" for no good reason. This PR makes them regular or expert options. --- src/options/README.md | 12 +++++++++++- src/options/base_options.toml | 9 ++++++--- src/options/parser_options.toml | 3 ++- src/options/smt_options.toml | 14 +++++++------- 4 files changed, 26 insertions(+), 12 deletions(-) diff --git a/src/options/README.md b/src/options/README.md index c3e018215..2f89f04ee 100644 --- a/src/options/README.md +++ b/src/options/README.md @@ -26,7 +26,7 @@ Specifying Options Options can be defined within a module file with the `[[option]]` tag, the required attributes for an option are: -* `category` (string): one of `common`, `expert`, `regular`, or `undocumented` +* `category` (string): one of `common`, `regular`, `expert`, or `undocumented` * `type` (string): the C++ type of the option value, see below for more details. Optional attributes are: @@ -59,6 +59,16 @@ Optional attributes are: given) +Option categories +----------------- + +Every option has one of the following categories that influences where and how an option is visible: + +* `common`: Used for the most common options. All `common` options are shown at the very top in both the online documentation and the output of `--help` on the command line. +* `regular`: This should be used for most options. +* `expert`: This is for options that should be used with care only. A warning is shown in both the online documentation and the command line help. +* `undocumented`: Such an option is skipped entirely in both the online documentation and the command line help. This should only be used when users don't have a (reasonable) use case for this option (e.g., because it stores data that is added via another option like for `output` and `outputTagHolder`). + Option types ------------ diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 042fd6b8a..415dbf9f3 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -3,27 +3,30 @@ name = "Base" [[option]] name = "err" - category = "undocumented" + category = "regular" long = "err=erroutput" type = "ManagedErr" alias = ["diagnostic-output-channel"] predicates = ["setErrStream"] includes = ["", "options/managed_streams.h"] + help = "Set the error (or diagnostic) output channel. Writes to stderr for \"stderr\" or \"--\", stdout for \"stdout\" or the given filename otherwise." [[option]] name = "in" - category = "undocumented" + category = "regular" long = "in=input" type = "ManagedIn" includes = ["", "options/managed_streams.h"] + help = "Set the error (or diagnostic) output channel. Reads from stdin for \"stdin\" or \"--\" and the given filename otherwise." [[option]] name = "out" - category = "undocumented" + category = "regular" long = "out=output" type = "ManagedOut" alias = ["regular-output-channel"] includes = ["", "options/managed_streams.h"] + help = "Set the error (or diagnostic) output channel. Writes to stdout for \"stdout\" or \"--\", stderr for \"stderr\" or the given filename otherwise." [[option]] name = "inputLanguage" diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml index 6fc683368..5552a677d 100644 --- a/src/options/parser_options.toml +++ b/src/options/parser_options.toml @@ -45,10 +45,11 @@ name = "Parser" # overwrite an existing file with malicious content. [[option]] name = "filesystemAccess" - category = "undocumented" + category = "expert" long = "filesystem-access" type = "bool" default = "true" + help = "limits the file system access if set to false" [[option]] name = "forceLogicString" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 026c8f494..1e55f63d0 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -377,7 +377,7 @@ name = "SMT Layer" [[option]] name = "solveBVAsInt" - category = "undocumented" + category = "expert" long = "solve-bv-as-int=MODE" type = "SolveBVAsIntMode" default = "OFF" @@ -401,7 +401,7 @@ name = "SMT Layer" [[option]] name = "BVAndIntegerGranularity" - category = "undocumented" + category = "expert" long = "bvand-integer-granularity=N" type = "uint64_t" default = "1" @@ -409,7 +409,7 @@ name = "SMT Layer" [[option]] name = "iandMode" - category = "undocumented" + category = "expert" long = "iand-mode=mode" type = "IandMode" default = "VALUE" @@ -427,7 +427,7 @@ name = "SMT Layer" [[option]] name = "solveIntAsBV" - category = "undocumented" + category = "expert" long = "solve-int-as-bv=N" type = "uint64_t" default = "0" @@ -435,7 +435,7 @@ name = "SMT Layer" [[option]] name = "solveRealAsInt" - category = "undocumented" + category = "expert" long = "solve-real-as-int" type = "bool" default = "false" @@ -443,7 +443,7 @@ name = "SMT Layer" [[option]] name = "produceInterpols" - category = "undocumented" + category = "regular" long = "produce-interpols=MODE" type = "ProduceInterpols" default = "NONE" @@ -470,7 +470,7 @@ name = "SMT Layer" [[option]] name = "produceAbducts" - category = "undocumented" + category = "regular" long = "produce-abducts" type = "bool" default = "false" -- 2.30.2