diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index d233a47f710..c0e38960235 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -720,61 +721,59 @@ void janalyzer_parse_optionst::help() std::cout << '\n' << banner_string("JANALYZER", CBMC_VERSION) << '\n' << align_center_with_border("Copyright (C) 2016-2018") << '\n' << align_center_with_border("Daniel Kroening, Diffblue") << '\n' - << align_center_with_border("kroening@kroening.com") << '\n' - << + << align_center_with_border("kroening@kroening.com") << '\n'; + + std::cout << help_formatter( "\n" - "Usage: Purpose:\n" + "Usage: \tPurpose:\n" "\n" - " janalyzer [-?] [-h] [--help] show help\n" - " janalyzer\n" + " {bjanalyzer} [{y-?}] [{y-h}] [{y--help}] \t show this help\n" + " {bjanalyzer}\n" HELP_JAVA_METHOD_NAME - " janalyzer\n" + " {bjanalyzer}\n" HELP_JAVA_CLASS_NAME - " janalyzer\n" + " {bjanalyzer}\n" HELP_JAVA_JAR - " janalyzer\n" + " {bjanalyzer}\n" HELP_JAVA_GOTO_BINARY "\n" HELP_JAVA_CLASSPATH HELP_FUNCTIONS "\n" "Task options:\n" - " --show display the abstract domains\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --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" - // NOLINTNEXTLINE(whitespace/line_length) - " --reachable-functions list functions reachable from the entry point\n" + " {y--show} \t display the abstract domains\n" + " {y--verify} \t use the abstract domains to check assertions\n" + " {y--simplify} {ufile_name} \t use the abstract domains to simplify the" + " program\n" + " {y--no-simplify-slicing} \t do not remove instructions from which no" + " property can be reached (use with {y--simplify})\n" + " {y--unreachable-instructions} \t list dead code\n" + " {y--unreachable-functions} \t list functions unreachable from the entry" + " point" + " {y--reachable-functions} \t list functions reachable from the entry point" "\n" "Abstract interpreter options:\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --location-sensitive use location-sensitive abstract interpreter\n" - " --concurrent use concurrency-aware abstract interpreter\n" + " {y--location-sensitive} \t use location-sensitive abstract interpreter" + " {y--concurrent} \t use concurrency-aware abstract interpreter\n" "\n" "Domain options:\n" - " --constants constant domain\n" - " --intervals interval domain\n" - " --non-null non-null domain\n" - " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*) + " {y--constants} \t constant domain\n" + " {y--intervals} \t interval domain\n" + " {y--non-null} \t non-null domain\n" + " {y--dependence-graph} \t data and control dependencies between" + " instructions" "\n" "Output options:\n" - " --text file_name output results in plain text to given file\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --json file_name output results in JSON format to given file\n" - " --xml file_name output results in XML format to given file\n" - " --dot file_name output results in DOT format to given file\n" + " {y--text} {ufile_name} \t output results in plain text to given file\n" + " {y--json} {ufile_name} \t output results in JSON format to given file\n" + " {y--xml} {ufile_name} \t output results in XML format to given file\n" + " {y--dot} {ufile_name} \t output results in DOT format to given file\n" "\n" "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" + " {y--taint} {ufile_name} \t perform taint analysis using rules in given" + " file\n" + " {y--show-taint} \t print taint analysis results on stdout\n" + " {y--show-local-may-alias} \t perform procedure-local may alias analysis\n" "\n" "Java Bytecode frontend options:\n" JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP @@ -783,20 +782,20 @@ void janalyzer_parse_optionst::help() HELP_CONFIG_PLATFORM "\n" "Program representations:\n" - " --show-parse-tree show parse tree\n" - " --show-symbol-table show loaded symbol table\n" + " {y--show-parse-tree} \t show parse tree\n" + " {y--show-symbol-table} \t show loaded symbol table\n" HELP_SHOW_GOTO_FUNCTIONS HELP_SHOW_PROPERTIES "\n" "Program instrumentation options:\n" - " --no-assertions ignore user assertions\n" - " --no-assumptions ignore user assumptions\n" - " --property id enable selected properties only\n" + " {y--no-assertions} \t ignore user assertions\n" + " {y--no-assumptions} \t ignore user assumptions\n" + " {y--property} {uid} \t enable selected properties only\n" "\n" "Other options:\n" - " --version show version and exit\n" - " --verbosity # verbosity level\n" + " {y--version} \t show version and exit\n" + " {y--verbosity {u#} \t verbosity level\n" HELP_TIMESTAMP - "\n"; + "\n"); // clang-format on } diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 486a3447c88..22189337dc1 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -52,82 +52,75 @@ Author: Daniel Kroening, kroening@kroening.com "(static-values):" \ "(java-lift-clinit-calls)" -#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \ - " --disable-uncaught-exception-check\n" \ - " ignore uncaught exceptions and errors\n" \ - " --throw-assertion-error throw java.lang.AssertionError on violated\n" \ - " assert statements instead of failing\n" \ - " at the location of the assert statement\n" \ - " --throw-runtime-exceptions make implicit runtime exceptions explicit\n" \ - " --assert-no-exceptions-thrown\n"\ - " transform `throw` instructions into `assert FALSE`\n"/* NOLINT(*) */ \ - " followed by `assume FALSE`.\n" \ - " --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \ - " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \ - " at level N references are set to null\n" /* NOLINT(*) */ \ - " --java-assume-inputs-non-null\n" \ - " never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \ - " entry point with null\n" /* NOLINT(*) */ \ - " --java-assume-inputs-interval [L:U] or [L:] or [:U]\n" \ - " force numerical primitive-typed inputs\n" /* NOLINT(*) */ \ - " (byte, short, int, long, float, double) to be\n" /* NOLINT(*) */ \ - " initialized within the given range; lower bound\n" /* NOLINT(*) */ \ - " L and upper bound U must be integers;\n" /* NOLINT(*) */ \ - " does not work for arrays;\n" /* NOLINT(*) */ \ - " --java-assume-inputs-integral\n" \ - " force float and double inputs to have integer values;\n" /* NOLINT(*) */ \ - " does not work for arrays;\n" /* NOLINT(*) */ \ - " --java-max-vla-length N limit the length of user-code-created arrays\n" /* NOLINT(*) */ \ - " --java-cp-include-files r regexp or JSON list of files to load\n" \ - " (with '@' prefix)\n" \ - " --java-load-class CLASS also load code from class CLASS\n" \ - " --java-no-load-class CLASS never load code from class CLASS\n" \ - " --ignore-manifest-main-class ignore Main-Class entries in JAR manifest files.\n" /* NOLINT(*) */ \ - " If this option is specified and the options\n" /* NOLINT(*) */ \ - " --function and --main-class are not, we can be\n" /* NOLINT(*) */ \ - " certain that all classes in the JAR file are\n" /* NOLINT(*) */ \ - " loaded.\n" \ - " --context-include i only analyze code matching specification i that\n" /* NOLINT(*) */ \ - " --context-exclude e does not match specification e.\n" \ - " All other methods are excluded, i.e. we load their\n" /* NOLINT(*) */ \ - " signatures and meta-information, but not their\n" /* NOLINT(*) */ \ - " bodies.\n" \ - " A specification is any prefix of a package, class\n" /* NOLINT(*) */ \ - " or method name, e.g. \"org.cprover.\" or\n" /* NOLINT(*) */ \ - " \"org.cprover.MyClass.\" or\n" \ - " \"org.cprover.MyClass.methodToStub:(I)Z\".\n" \ - " These options can be given multiple times.\n" \ - " The default for context-include is 'all\n" \ - " included'; default for context-exclude is\n" \ - " 'nothing excluded'.\n" \ - " --no-lazy-methods load and translate all methods given on\n" \ - " the command line and in --classpath\n" \ - " Default is to load methods that appear to be\n" /* NOLINT(*) */ \ - " reachable from the --function entry point\n" \ - " or main class\n" \ - " Note that --show-symbol-table, --show-goto-functions\n" /* NOLINT(*) */ \ - " and --show-properties output are restricted to\n" /* NOLINT(*) */ \ - " loaded methods by default.\n" \ - " --lazy-methods-extra-entry-point METHODNAME\n" \ - " treat METHODNAME as a possible program entry\n" /* NOLINT(*) */ \ - " point for the purpose of lazy method loading\n" /* NOLINT(*) */ \ - " METHODNAME can be a regex that will be matched\n" /* NOLINT(*) */ \ - " against all symbols. If missing a java:: prefix\n" /* NOLINT(*) */ \ - " will be added. If no descriptor is found, all\n"/* NOLINT(*) */ \ - " overloads of a method will also be added.\n" \ - " --static-values f Load initial values of static fields from the given\n"/* NOLINT(*) */ \ - " JSON file. We assign static fields to these values\n"/* NOLINT(*) */ \ - " instead of calling the normal static initializer\n"/* NOLINT(*) */ \ - " (clinit) method.\n" \ - " The argument can be a relative or absolute path to\n"/* NOLINT(*) */ \ - " the file.\n" \ - " --java-lift-clinit-calls Lifts clinit calls in function bodies to the top of the\n" /* NOLINT(*) */ \ - " function. This may reduce the overall cost of static\n" /* NOLINT(*) */ \ - " initialisation, but may be unsound if there are\n" /* NOLINT(*) */ \ - " cyclic dependencies between static initializers due\n" /* NOLINT(*) */ \ - " to potentially changing their order of execution,\n" /* NOLINT(*) */ \ - " or if static initializers have side-effects such as\n" /* NOLINT(*) */ \ - " updating another class' static field.\n" /* NOLINT(*) */ +#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP \ + " {y--disable-uncaught-exception-check} \t " \ + "ignore uncaught exceptions and errors\n" \ + " {y--throw-assertion-error} \t " \ + "throw java.lang.AssertionError on violated assert statements instead of " \ + "failing at the location of the assert statement\n" \ + " {y--throw-runtime-exceptions} \t " \ + "make implicit runtime exceptions explicit\n" \ + " {y--assert-no-exceptions-thrown} \t " \ + "transform `throw` instructions into `assert FALSE` followed by " \ + "`assume FALSE`.\n" \ + " {y--max-nondet-array-length} {uN} \t " \ + "limit nondet (e.g. input) array size to <= {uN}\n" \ + " {y--max-nondet-tree-depth} {uN} \t " \ + "limit size of nondet (e.g. input) object tree; at level {uN} references " \ + "are set to null\n" \ + " {y--java-assume-inputs-non-null} \t " \ + "never initialize reference-typed parameter to the entry point with null\n" \ + " {y--java-assume-inputs-interval} {y[}{uL}{y:}{uU}|{uL}{y:}|{y:}{uU}{y]} " \ + "\t " \ + "force numerical primitive-typed inputs (byte, short, int, long, float, " \ + "double) to be initialized within the given range; lower bound {uL} and " \ + "upper bound {uU} must be integers; does not work for arrays\n" \ + " {y--java-assume-inputs-integral} \t " \ + "force float and double inputs to have integer values; does not work for " \ + "arrays\n" \ + " {y--java-max-vla-length} {uN} \t " \ + "limit the length of user-code-created arrays\n" \ + " {y--java-cp-include-files} {ur} \t " \ + "regexp or JSON list of files to load (with '@' prefix)\n" \ + " {y--java-load-class} {uCLASS} \t also load code from class {uCLASS}\n" \ + " {y--java-no-load-class} {uCLASS} \t never load code from class " \ + "{uCLASS}\n" \ + " {y--ignore-manifest-main-class} \t " \ + "ignore Main-Class entries in JAR manifest files. If this option is " \ + "specified and the options {y--function} and {y--main-class} are not, we " \ + "can be certain that all classes in the JAR file are loaded.\n" \ + " {y--context-include} {ui} \t " \ + "only analyze code matching specification {ui}\n" \ + " {y--context-exclude} {ue} \t " \ + "only analyze code does not match specification {ue}. All other methods " \ + "are excluded, i.e. we load their signatures and meta-information, but not " \ + "their bodies. A specification is any prefix of a package, class or method " \ + "name, e.g. \"org.cprover.\" or \"org.cprover.MyClass.\" or " \ + "\"org.cprover.MyClass.methodToStub:(I)Z\". These options can be given " \ + "multiple times. The default for context-include is 'all included'; " \ + "default for context-exclude is 'nothing excluded'.\n" \ + " {y--no-lazy-methods} \t " \ + "load and translate all methods given on the command line and in " \ + "{y--classpath}. Default is to load methods that appear to be reachable " \ + "from the {y--function} entry point or main class Note that " \ + "{y--show-symbol-table}, {y--show-goto-functions} and " \ + "{y--show-properties} output are restricted to loaded methods by default.\n" \ + " {y--lazy-methods-extra-entry-point} {uMETHODNAME} \t " \ + "treat {uMETHODNAME} as a possible program entry point for the purpose of " \ + "lazy method loading {uMETHODNAME} can be a regex that will be matched " \ + "against all symbols. If missing a java:: prefix will be added. If no " \ + "descriptor is found, all overloads of a method will also be added.\n" \ + " {y--static-values} {uf} \t " \ + "Load initial values of static fields from the given JSON file {uf}. We " \ + "assign static fields to these values instead of calling the normal " \ + "static initializer (clinit) method. The argument can be a relative or " \ + "absolute path to the file.\n" \ + " {y--java-lift-clinit-calls} \t " \ + "Lifts clinit calls in function bodies to the top of the function. This " \ + "may reduce the overall cost of static initialisation, but may be unsound " \ + "if there are cyclic dependencies between static initializers due to " \ + "potentially changing their order of execution, or if static initializers " \ + "have side-effects such as updating another class' static field.\n" \ #ifdef _WIN32 #define JAVA_CLASSPATH_SEPARATOR ";" @@ -135,50 +128,43 @@ Author: Daniel Kroening, kroening@kroening.com #define JAVA_CLASSPATH_SEPARATOR ":" #endif -#define HELP_JAVA_CLASSPATH /* NOLINT(*) */ \ - " -classpath dirs/jars\n" \ - " -cp dirs/jars\n" \ - " --classpath dirs/jars set class search path of directories and\n" \ - " jar files\n" \ - " A " JAVA_CLASSPATH_SEPARATOR \ - " separated list of directories and JAR\n" \ - " archives to search for class files.\n" \ - " --main-class class-name set the name of the main class\n" - -#define HELP_JAVA_METHOD_NAME /* NOLINT(*) */ \ - " method-name fully qualified name of method\n" \ - " used as entry point, e.g.\n" \ - " mypackage.Myclass.foo:(I)Z\n" - -#define HELP_JAVA_CLASS_NAME /* NOLINT(*) */ \ - " class-name name of class\n" \ - " The entry point is the method specified by\n" \ - " --function, or otherwise, the\n" \ - " public static void main(String[])\n" \ - " method of the given class.\n" - -#define OPT_JAVA_JAR /* NOLINT(*) */ \ +#define HELP_JAVA_CLASSPATH \ + " {y-classpath} {udirs/jars}, {y-cp} {udirs/jars}, " \ + "{y--classpath} {udirs/jars} \t " \ + "set class search path of directories and jar files to a " \ + JAVA_CLASSPATH_SEPARATOR "-separated list of directories and JAR " \ + "archives to search for class files\n" \ + " {y--main-class} {uclass-name} \t set the name of the main class\n" + +#define HELP_JAVA_METHOD_NAME \ + " {umethod-name} \t " \ + "fully qualified name of method used as entry point, e.g. " \ + "mypackage.Myclass.foo:(I)Z\n" + +#define HELP_JAVA_CLASS_NAME \ + " {uclass-name} \t " \ + "name of class. The entry point is the method specified by --function, " \ + "or otherwise, the public static void main(String[]) method of the given " \ + "class.\n" + +#define OPT_JAVA_JAR \ "(jar):" -#define HELP_JAVA_JAR /* NOLINT(*) */ \ - " -jar jarfile JAR file to be checked\n" \ - " The entry point is the method specified by\n" \ - " --function or otherwise, the\n" \ - " public static void main(String[]) method\n" \ - " of the class specified by --main-class or the main\n" /* NOLINT(*) */ \ - " class specified in the JAR manifest\n" \ - " (checked in this order).\n" +#define HELP_JAVA_JAR \ + " {y-jar} {ujarfile} \t " \ + "JAR file to be checked. The entry point is the method specified by " \ + "{y--function} or otherwise, the public static void main(String[]) method " \ + "of the class specified by {y--main-class} or the main class specified in " \ + "the JAR manifest (checked in this order).\n" -#define OPT_JAVA_GOTO_BINARY /* NOLINT(*) */ \ +#define OPT_JAVA_GOTO_BINARY \ "(gb):" -#define HELP_JAVA_GOTO_BINARY /* NOLINT(*) */ \ - " --gb goto-binary goto-binary file to be checked\n" \ - " The entry point is the method specified by\n" \ - " --function, or otherwise, the\n" \ - " public static void main(String[])\n" \ - " of the class specified by --main-class\n" \ - " (checked in this order).\n" +#define HELP_JAVA_GOTO_BINARY \ + " {y--gb} {ugoto-binary} \t " \ + "goto-binary file to be checked. The entry point is the method specified " \ + "by {y--function}, or otherwise, the public static void main(String[]) of " \ + "the class specified by {y--main-class} (checked in this order).\n" // clang-format on enum lazy_methods_modet diff --git a/jbmc/src/java_bytecode/java_trace_validation.h b/jbmc/src/java_bytecode/java_trace_validation.h index f9c4f253008..7b0b5b8935b 100644 --- a/jbmc/src/java_bytecode/java_trace_validation.h +++ b/jbmc/src/java_bytecode/java_trace_validation.h @@ -27,9 +27,9 @@ class messaget; "(validate-trace)" \ #define HELP_JAVA_TRACE_VALIDATION /*NOLINT*/ \ - " --validate-trace throw an error if the structure of the counterexample\n" /*NOLINT*/ \ - " trace does not match certain assumptions\n" /*NOLINT*/ \ - " (experimental, currently java only)\n" /*NOLINT*/ \ + " {y--validate-trace} \t throw an error if the structure of the" \ + " counterexample trace does not match certain assumptions (experimental," \ + " currently java only)\n" // clang-format on /// Checks that the structure of each step of the trace matches certain diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 324a0868fe3..ef776c63f3c 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -960,18 +961,20 @@ void jbmc_parse_optionst::help() << align_center_with_border("Copyright (C) 2001-2018") << '\n' << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*) << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*) - << align_center_with_border("kroening@kroening.com") << '\n' - << "\n" - "Usage: Purpose:\n" + << align_center_with_border("kroening@kroening.com") << '\n'; + + std::cout << help_formatter( + "\n" + "Usage: \tPurpose:\n" "\n" - " jbmc [-?] [-h] [--help] show help\n" - " jbmc\n" + " {bjbmc} [{y-?}] [{y-h}] [{y--help}] \t show this help\n" + " {bjbmc}\n" HELP_JAVA_METHOD_NAME - " jbmc\n" + " {bjbmc}\n" HELP_JAVA_CLASS_NAME - " jbmc\n" + " {bjbmc}\n" HELP_JAVA_JAR - " jbmc\n" + " {bjbmc}\n" HELP_JAVA_GOTO_BINARY "\n" HELP_JAVA_CLASSPATH @@ -979,49 +982,50 @@ void jbmc_parse_optionst::help() "\n" "Analysis options:\n" HELP_SHOW_PROPERTIES - " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*) - " --property id only check one specific property\n" - " --trace give a counterexample trace for failed properties\n" //NOLINT(*) - " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) - " (implies --trace)\n" - " --localize-faults localize faults (experimental)\n" + " {y--symex-coverage-report} {uf} \t generate a Cobertura XML coverage" + " report in {uf}\n" + " {y--property} {uid} \t only check one specific property\n" + " {y--trace} \t give a counterexample trace for failed properties\n" + " {y--stop-on-fail} \t stop analysis once a failed property is detected" + " (implies {y--trace})\n" + " {y--localize-faults} \t localize faults (experimental)\n" HELP_JAVA_TRACE_VALIDATION "\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" - " --list-symbols list symbols with type information\n" + " {y--show-parse-tree} \t show parse tree\n" + " {y--show-symbol-table} \t show loaded symbol table\n" + " {y--list-symbols} \t list symbols with type information\n" HELP_SHOW_GOTO_FUNCTIONS - " --drop-unused-functions drop functions trivially unreachable\n" - " from main function\n" + " {y--drop-unused-functions} \t drop functions trivially unreachable" + " from main function\n" HELP_SHOW_CLASS_HIERARCHY "\n" "Program instrumentation options:\n" - " --no-assertions ignore user assertions\n" - " --no-assumptions ignore user assumptions\n" - " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) + " {y--no-assertions} \t ignore user assertions\n" + " {y--no-assumptions} \t ignore user assumptions\n" + " {y--mm} {uMM} \t memory consistency model for concurrent programs\n" HELP_REACHABILITY_SLICER - " --full-slice run full slicer (experimental)\n" // NOLINT(*) + " {y--full-slice} \t run full slicer (experimental)\n" "\n" "Java Bytecode frontend options:\n" JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP // This one is handled by jbmc_parse_options not by the Java frontend, // hence its presence here: - " --java-threading enable java multi-threading support (experimental)\n" // NOLINT(*) - " --java-unwind-enum-static unwind loops in static initialization of enums\n" // NOLINT(*) - // Currently only supported in the JBMC frontend: - " --symex-driven-lazy-loading only load functions when first entered by symbolic\n" // NOLINT(*) - " execution. Note that --show-symbol-table,\n" - " --show-goto-functions/properties output\n" - " will be restricted to loaded methods in this case,\n" // NOLINT(*) - " and only output after the symex phase.\n" + " {y--java-threading} \t enable java multi-threading support" + " (experimental)\n" + " {y--java-unwind-enum-static} \t unwind loops in static initialization of" + " enums\n" + " {y--symex-driven-lazy-loading} \t only load functions when first entered" + " by symbolic execution. Note that {y--show-symbol-table}," + " {y--show-goto-functions}, {y--show-properties} output will be restricted" + " to loaded methods in this case, and only output after the symex phase.\n" "\n" "Semantic transformations:\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --nondet-static add nondeterministic initialization of variables with static lifetime\n" + " {y--nondet-static} \t add nondeterministic initialization of variables" + " with static lifetime\n" "\n" "BMC options:\n" HELP_BMC @@ -1030,18 +1034,19 @@ void jbmc_parse_optionst::help() HELP_CONFIG_BACKEND HELP_SOLVER HELP_STRING_REFINEMENT - " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) - " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*) + " {y--arrays-uf-never} \t never turn arrays into uninterpreted functions\n" + " {y--arrays-uf-always} \t always turn arrays into uninterpreted" + " functions\n" "\n" "Other options:\n" - " --version show version and exit\n" + " {y--version} \t show version and exit\n" HELP_XML_INTERFACE HELP_JSON_INTERFACE HELP_VALIDATE HELP_GOTO_TRACE HELP_FLUSH - " --verbosity # verbosity level\n" + " {y--verbosity} {u#} \t verbosity level\n" HELP_TIMESTAMP - "\n"; + "\n"); // clang-format on } diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index ea2c124f93c..512e7320f12 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -13,6 +13,7 @@ Author: Peter Schrammel #include #include +#include #include #include @@ -234,34 +235,34 @@ void jdiff_parse_optionst::help() std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n' << align_center_with_border("Copyright (C) 2016-2018") << '\n' << align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT(*) - << align_center_with_border("kroening@kroening.com") << '\n' - << + << align_center_with_border("kroening@kroening.com") << '\n'; + + std::cout << help_formatter( "\n" - "Usage: Purpose:\n" + "Usage: \tPurpose:\n" "\n" - " jdiff [-?] [-h] [--help] show help\n" - " jdiff old new jars to be compared\n" + " {bjdiff} [{y-?}] [{y-h}] [{y--help}] \t show this help\n" + " {bjdiff} {uold} {unew} \t jars to be compared\n" "\n" "Diff options:\n" HELP_SHOW_GOTO_FUNCTIONS HELP_SHOW_PROPERTIES - " --show-loops show the loops in the programs\n" - " -u | --unified output unified diff\n" - " --change-impact | \n" - " --forward-impact |\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n" - " --compact-output output dependencies in compact mode\n" + " {y--show-loops} \t show the loops in the programs\n" + " {y-u}, {y--unified} \t output unified diff\n" + " {y--change-impact}, {y--forward-impact}, {y--backward-impact} \t output" + " unified diff with forward&backward/forward/backward dependencies\n" + " {y--compact-output} \t output dependencies in compact mode\n" "\n" "Program instrumentation options:\n" - " --no-assertions ignore user assertions\n" - " --no-assumptions ignore user assumptions\n" + " {y--no-assertions} \t ignore user assertions\n" + " {y--no-assumptions} \t ignore user assumptions\n" HELP_COVER + "\n" "Other options:\n" - " --version show version and exit\n" - " --json-ui use JSON-formatted output\n" - " --verbosity # verbosity level\n" + " {y--version} \t show version and exit\n" + " {y--json-ui} \t use JSON-formatted output\n" + " {y--verbosity} {u#} \t verbosity level\n" HELP_TIMESTAMP - "\n"; + "\n"); // clang-format on } diff --git a/regression/goto-bmc/arguments/help.desc b/regression/goto-bmc/arguments/help.desc index e2da04f860e..9e406abd9e9 100644 --- a/regression/goto-bmc/arguments/help.desc +++ b/regression/goto-bmc/arguments/help.desc @@ -6,7 +6,7 @@ CORE goto-bmc \d\.\d+\.\d+ Usage\: Purpose\: -show help +show this help show version and exit -- -- diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h index 8904cbba97d..98eb8e6c79a 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h @@ -80,26 +80,25 @@ "(vsd-unions):" \ "(vsd-flow-insensitive)" \ "(vsd-data-dependencies)" \ - "(vsd-liveness)" \ - \ - // clang-format off + "(vsd-liveness)" + #define HELP_VSD \ - " --vsd-values value tracking - " \ - "constants|intervals|set-of-constants\n" /* NOLINT(whitespace/line_length) */\ - " --vsd-structs struct field sensitive analysis - " \ - "top-bottom|every-field\n" /* NOLINT(whitespace/line_length) */ \ - " --vsd-arrays array entry sensitive analysis - " \ - "top-bottom|smash|up-to-n-elements|every-element\n" /* NOLINT(whitespace/line_length) */ \ - " --vsd-array-max-elements the n in --vsd-arrays up-to-n-elements - " \ - "defaults to 10 if not given\n" /* NOLINT(whitespace/line_length) */ \ - " --vsd-pointers pointer sensitive analysis - " \ - "top-bottom|constants|value-set\n" /* NOLINT(whitespace/line_length) */ \ - " --vsd-unions union sensitive analysis - top-bottom\n" \ - " --vsd-data-dependencies track data dependencies\n" \ - " --vsd-liveness track variable liveness\n" \ - " --vsd-flow-insensitive disables flow sensitivity\n" \ - -// cland-format on + " {y--vsd-values} [{yconstants}|{yintervals}|{yset-of-constants}] \t " \ + "value tracking\n" \ + " {y--vsd-structs} [{ytop-bottom}|{yevery-field}] \t " \ + "struct field sensitive analysis\n" \ + " {y--vsd-arrays} [[ytop-bottom}|{ysmash}|{yup-to-n-elements}|" \ + "{yevery-element}] \t " \ + "array entry sensitive analysis\n" \ + " {y--vsd-array-max-elements} {uN} \t " \ + "set the {un} in {y--vsd-arrays} {yup-to-n-elements} (defaults to 10 if " \ + "not given)\n" \ + " {y--vsd-pointers} [{ytop-bottom}|{yconstants}|{yvalue-set}] \t " \ + "pointer sensitive analysis\n" \ + " {y--vsd-unions} [{ytop-bottom}] \t union sensitive analysis\n" \ + " {y--vsd-data-dependencies} \t track data dependencies\n" \ + " {y--vsd-liveness} \t track variable liveness\n" \ + " {y--vsd-flow-insensitive} \t disables flow sensitivity\n" #define PARSE_OPTIONS_VSD(cmdline, options) \ options.set_option("values", cmdline.get_value("vsd-values")); \ diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h index 0fd1ccefb8a..db80e687549 100644 --- a/src/ansi-c/ansi_c_language.h +++ b/src/ansi-c/ansi_c_language.h @@ -25,10 +25,12 @@ Author: Daniel Kroening, kroening@kroening.com "(min-null-tree-depth):" #define HELP_ANSI_C_LANGUAGE \ - " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */\ - " at level N pointers are set to null\n" \ - " --min-null-tree-depth N minimum level at which a pointer can first be\n" /* NOLINT(*) */\ - " NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */ + " {y--max-nondet-tree-depth} {uN} \t " \ + "limit size of nondet (e.g. input) object tree; at level {uN} pointers are " \ + "set to null\n" \ + " {y--min-null-tree-depth} {uN} \t " \ + "minimum level at which a pointer can first be NULL in a recursively " \ + "nondet initialized struct\n" \ // clang-format on class ansi_c_languaget:public languaget diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h index 7b144ad1123..a15c700df69 100644 --- a/src/ansi-c/goto_check_c.h +++ b/src/ansi-c/goto_check_c.h @@ -49,29 +49,35 @@ void goto_check_c( "(no-assertions)(no-assumptions)" \ "(assert-to-assume)" -// clang-format off -#define HELP_GOTO_CHECK \ - " --bounds-check enable array bounds checks\n" \ - " --pointer-check enable pointer checks\n" /* NOLINT(whitespace/line_length) */ \ - " --memory-leak-check enable memory leak checks\n" \ - " --memory-cleanup-check enable memory cleanup checks\n" \ - " --div-by-zero-check enable division by zero checks\n" \ - " --signed-overflow-check enable signed arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \ - " --unsigned-overflow-check enable arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \ - " --pointer-overflow-check enable pointer arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \ - " --conversion-check check whether values can be represented after type cast\n" /* NOLINT(whitespace/line_length) */ \ - " --undefined-shift-check check shift greater than bit-width\n" \ - " --float-overflow-check check floating-point for +/-Inf\n" \ - " --nan-check check floating-point for NaN\n" \ - " --enum-range-check checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \ - " --pointer-primitive-check checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */ \ - " --retain-trivial-checks include checks that are trivially true\n" \ - " --error-label label check that label is unreachable\n" \ - " --no-built-in-assertions ignore assertions in built-in library\n" \ - " --no-assertions ignore user assertions\n" \ - " --no-assumptions ignore user assumptions\n" \ - " --assert-to-assume convert user assertions to assumptions\n" \ +#define HELP_GOTO_CHECK \ + " {y--bounds-check} \t enable array bounds checks\n" \ + " {y--pointer-check} \t enable pointer checks\n" \ + " {y--memory-leak-check} \t enable memory leak checks\n" \ + " {y--memory-cleanup-check} \t enable memory cleanup checks\n" \ + " {y--div-by-zero-check} \t enable division by zero checks\n" \ + " {y--signed-overflow-check} \t " \ + "enable signed arithmetic over- and underflow checks\n" \ + " {y--unsigned-overflow-check} \t " \ + "enable arithmetic over- and underflow checks\n" \ + " {y--pointer-overflow-check} \t " \ + "enable pointer arithmetic over- and underflow checks\n" \ + " {y--conversion-check} \t " \ + "check whether values can be represented after type cast\n" \ + " {y--undefined-shift-check} \t check shift greater than bit-width" \ + " {y--float-overflow-check} \t check floating-point for +/-Inf\n" \ + " {y--nan-check} \t check floating-point for NaN\n" \ + " {y--enum-range-check} \t " \ + "checks that all enum type expressions have values in the enum range\n" \ + " {y--pointer-primitive-check} \t " \ + "checks that all pointers in pointer primitives are valid or null\n" \ + " {y--retain-trivial-checks} \t include checks that are trivially true\n" \ + " {y--error-label} {ulabel} \t check that label {ulabel} is unreachable\n" \ + " {y--no-built-in-assertions} \t ignore assertions in built-in library\n" \ + " {y--no-assertions} \t ignore user assertions\n" \ + " {y--no-assumptions} \t ignore user assumptions\n" \ + " {y--assert-to-assume} \t convert user assertions to assumptions\n" +// clang-format off #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \ options.set_option("bounds-check", cmdline.isset("bounds-check")); \ options.set_option("pointer-check", cmdline.isset("pointer-check")); \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 31cf9905f48..8867e612a83 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -935,27 +936,29 @@ void cbmc_parse_optionst::help() << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*) << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*) << align_center_with_border("kroening@kroening.com") << '\n' // NOLINT(*) - << align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n' // NOLINT(*) - << + << align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n'; // NOLINT(*) + + std::cout << help_formatter( "\n" - "Usage: Purpose:\n" + "Usage: \tPurpose:\n" "\n" - " cbmc [-?] [-h] [--help] show help\n" - " cbmc --version show version and exit\n" - " cbmc [options] file.c ... perform bounded model checking\n" + " {bcbmc} [{y-?}] [{y-h}] [{y--help}] \t show this help\n" + " {bcbmc} {y--version} \t show version and exit\n" + " {bcbmc} [options] {ufile.c} {u...} \t perform bounded model checking\n" "\n" "Analysis options:\n" HELP_SHOW_PROPERTIES - " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*) - " --property id only check one specific property\n" - " --trace give a counterexample trace for failed properties\n" //NOLINT(*) - " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) - " (implies --trace)\n" - " --localize-faults localize faults (experimental)\n" + " {y--symex-coverage-report} {uf} \t generate a Cobertura XML coverage" + " report in {uf}\n" + " {y--property} {uid} \t only check one specific property\n" + " {y--trace} \t give a counterexample trace for failed properties\n" + " {y--stop-on-fail} \t stop analysis once a failed property is detected" + " (implies {y--trace})\n" + " {y--localize-faults} \t localize faults (experimental)\n" "\n" "C/C++ frontend options:\n" - " --preprocess stop after preprocessing\n" - " --test-preprocessor stop after preprocessing, discard output\n" + " {y--preprocess} \t stop after preprocessing\n" + " {y--test-preprocessor} \t stop after preprocessing, discard output\n" HELP_CONFIG_C_CPP HELP_ANSI_C_LANGUAGE HELP_FUNCTIONS @@ -964,27 +967,30 @@ void cbmc_parse_optionst::help() HELP_CONFIG_PLATFORM "\n" "Program representations:\n" - " --show-parse-tree show parse tree\n" - " --show-symbol-table show loaded symbol table\n" + " {y--show-parse-tree} \t show parse tree\n" + " {y--show-symbol-table} \t show loaded symbol table\n" HELP_SHOW_GOTO_FUNCTIONS HELP_VALIDATE - " --export-symex-ready-goto f serialise goto-program in symex-ready-goto form in f\n" // NOLINT(*) + " {y--export-symex-ready-goto} {uf} \t " + "serialise goto-program in symex-ready-goto form in {uf}\n" "\n" "Program instrumentation options:\n" HELP_GOTO_CHECK HELP_COVER - " --mm MM memory consistency model for concurrent programs (default: sc)\n" // NOLINT(*) + " {y--mm} {uMM} \t memory consistency model for concurrent programs" + " (default: {ysc})\n" HELP_CONFIG_LIBRARY HELP_REACHABILITY_SLICER - " --full-slice run full slicer (experimental)\n" // NOLINT(*) - " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) - " --havoc-undefined-functions\n" - " for any function that has no body, assign non-deterministic values to\n" // NOLINT(*) - " any parameters passed as non-const pointers and the return value\n" // NOLINT(*) + " {y--full-slice} \t run full slicer (experimental)\n" + " {y--drop-unused-functions} \t drop functions trivially unreachable from" + " main function\n" + " {y--havoc-undefined-functions} \t for any function that has no body," + " assign non-deterministic values to any parameters passed as non-const" + " pointers and the return value\n" "\n" "Semantic transformations:\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --nondet-static add nondeterministic initialization of variables with static lifetime\n" + " {y--nondet-static} \t add nondeterministic initialization of variables" + " with static lifetime\n" "\n" "BMC options:\n" HELP_BMC @@ -993,19 +999,19 @@ void cbmc_parse_optionst::help() HELP_CONFIG_BACKEND HELP_SOLVER HELP_STRING_REFINEMENT_CBMC - " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) - " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*) - " --show-array-constraints show array theory constraints added\n" - " during post processing.\n" - " Requires --json-ui.\n" + " {y--arrays-uf-never} \t never turn arrays into uninterpreted functions\n" + " {y--arrays-uf-always} \t always turn arrays into uninterpreted" + " functions\n" + " {y--show-array-constraints} \t show array theory constraints added" + " during post processing. Requires {y--json-ui}.\n" "\n" "User-interface options:\n" HELP_XML_INTERFACE HELP_JSON_INTERFACE HELP_GOTO_TRACE HELP_FLUSH - " --verbosity # verbosity level\n" + " {y--verbosity} {u#} \t verbosity level\n" HELP_TIMESTAMP - "\n"; + "\n"); // clang-format on } diff --git a/src/cprover/cprover_parse_options.cpp b/src/cprover/cprover_parse_options.cpp index bd6ebc4d7c3..c55160d6bc6 100644 --- a/src/cprover/cprover_parse_options.cpp +++ b/src/cprover/cprover_parse_options.cpp @@ -313,7 +313,6 @@ void cprover_parse_optionst::help() << banner_string("CPROVER", CBMC_VERSION) << '\n' << align_center_with_border("Copyright 2022") << '\n'; - // clang-format off std::cout << help_formatter( "\n" "Usage: \tPurpose:\n" diff --git a/src/crangler/crangler_parse_options.cpp b/src/crangler/crangler_parse_options.cpp index 44ae4522a00..05db4227fb0 100644 --- a/src/crangler/crangler_parse_options.cpp +++ b/src/crangler/crangler_parse_options.cpp @@ -13,14 +13,15 @@ Author: Daniel Kroening, dkr@amazon.com #include #include +#include #include #include -#include - #include "c_wrangler.h" +#include + int crangler_parse_optionst::doit() { if(cmdline.args.empty()) @@ -49,12 +50,13 @@ void crangler_parse_optionst::process_crangler_json( void crangler_parse_optionst::help() { - std::cout << '\n' - << banner_string("CRANGLER", CBMC_VERSION) << '\n' - << "\n" - "Usage: Purpose:\n" - "\n" - " crangler [-?] [-h] [--help] show help\n" - " crangler file.json ... configuration file names\n" - "\n"; + std::cout << '\n' << banner_string("CRANGLER", CBMC_VERSION) << '\n'; + + std::cout << help_formatter( + "\n" + "Usage: \tPurpose:\n" + "\n" + " {bcrangler} [{y-?}] [{y-h}] [{y--help}] \t show this help\n" + " {bcrangler} {ufile.json} ... \t configuration file names\n" + "\n"); } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index b4535bc2366..840621d0baf 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -681,95 +682,85 @@ bool goto_analyzer_parse_optionst::process_goto_program( /// display command line help void goto_analyzer_parse_optionst::help() { - // clang-format off - std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n' + std::cout << '\n' + << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n' << align_center_with_border("Copyright (C) 2017-2018") << '\n' << align_center_with_border("Daniel Kroening, Diffblue") << '\n' - << align_center_with_border("kroening@kroening.com") << '\n' - << + << align_center_with_border("kroening@kroening.com") << '\n'; + + // clang-format off + std::cout << help_formatter( "\n" - "Usage: Purpose:\n" + "Usage: \tPurpose:\n" "\n" - " goto-analyzer [-?|-h|--help] show help\n" - " goto-analyzer file.c ... source file names\n" + " {bgoto-analyzer} [{y-?}|{y-h}|{y--help}] \t show this help\n" + " {bgoto-analyzer} {ufile.c...} \t source file names\n" "\n" "Task options:\n" - " --show display the abstract states on the goto program\n" // NOLINT(*) - " --show-on-source display the abstract states on the source\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --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" - // NOLINTNEXTLINE(whitespace/line_length) - " --reachable-functions list functions reachable from the entry point\n" + " {y--show} \t display the abstract states on the goto program\n" + " {y--show-on-source} \t display the abstract states on the source\n" + " {y--verify} \t use the abstract domains to check assertions\n" + " {y--simplify} {ufile_name} \t use the abstract domains to simplify the" + " program\n" + " {y--no-simplify-slicing} \t do not remove instructions from which no" + " property can be reached (use with {y--simplify})\n" + " {y--unreachable-instructions} \t list dead code\n" + " {y--unreachable-functions} \t list functions unreachable from the entry" + " point\n" + " {y--reachable-functions} \t list functions reachable from the entry" + " point\n" "\n" "Abstract interpreter options:\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --legacy-ait recursion for function and one domain per location\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --recursive-interprocedural use recursion to handle interprocedural reasoning\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --three-way-merge use VSD's three-way merge on return from function call\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" + " {y--legacy-ait} \t recursion for function and one domain per location\n" + " {y--recursive-interprocedural} \t use recursion to handle interprocedural" + " reasoning\n" + " {y--three-way-merge} \t use VSD's three-way merge on return from function" + " call\n" + " {y--legacy-concurrent} \t legacy-ait with an extended fixed-point for" + " concurrency\n" + " {y--location-sensitive} \t use location-sensitive abstract interpreter\n" "\n" "History options:\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --ahistorical the most basic history, tracks locations only\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --call-stack n track the calling location stack for each function\n" - // NOLINTNEXTLINE(whitespace/line_length) - " limiting to at most n recursive loops, 0 to disable\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --loop-unwind n track the number of loop iterations within a function\n" - // NOLINTNEXTLINE(whitespace/line_length) - " limited to n histories per location, 0 is unlimited\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --branching n track the forwards jumps (if, switch, etc.) within a function\n" - // NOLINTNEXTLINE(whitespace/line_length) - " limited to n histories per location, 0 is unlimited\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --loop-unwind-and-branching n track all local control flow\n" - // NOLINTNEXTLINE(whitespace/line_length) - " limited to n histories per location, 0 is unlimited\n" + " {y--ahistorical} \t the most basic history, tracks locations only\n" + " {y--call-stack} {un} \t track the calling location stack for each" + " function limiting to at most {un} recursive loops, 0 to disable\n" + " {y--loop-unwind} {un} \t track the number of loop iterations within a" + " function limited to {un} histories per location, 0 is unlimited\n" + " {y--branching} {un} \t track the forwards jumps (if, switch, etc.) within" + " a function limited to {un} histories per location, 0 is unlimited\n" + " {y--loop-unwind-and-branching} {un} \t track all local control flow" + " limited to {un} histories per location, 0 is unlimited\n" "\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" - " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*) - " --vsd, --variable-sensitivity\n" - " a configurable non-relational domain\n" - " --dependence-graph-vs dependencies between instructions using VSD\n" // NOLINT(*) + " {y--constants} \t a constant for each variable if possible\n" + " {y--intervals} \t an interval for each variable\n" + " {y--non-null} \t tracks which pointers are non-null\n" + " {y--dependence-graph} \t data and control dependencies between" + " instructions\n" + " {y--vsd}, {y--variable-sensitivity} \t a configurable non-relational" + " domain\n" + " {y--dependence-graph-vs} \t dependencies between instructions using VSD\n" "\n" "Variable sensitivity domain (VSD) options:\n" HELP_VSD "\n" "Storage options:\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --one-domain-per-location stores a domain for each location reached (default)\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --one-domain-per-history stores a domain for each history object created\n" + " {y--one-domain-per-location} \t stores a domain for each location" + " reached\n" + " {y--one-domain-per-history} \t stores a domain for each history object" + " created\n" "\n" "Output options:\n" - " --text file_name output results in plain text to given file\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --json file_name output results in JSON format to given file\n" - " --xml file_name output results in XML format to given file\n" - " --dot file_name output results in DOT format to given file\n" + " {y--text} {ufile_name} \t output results in plain text to given file\n" + " {y--json} {ufile_name} \t output results in JSON format to given file\n" + " {y--xml} {ufile_name} \t output results in XML format to given file\n" + " {y--dot} {ufile_name} \t output results in DOT format to given file\n" "\n" "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" + " {y--taint} {ufile_name} \t perform taint analysis using rules in given" + " file\n" + " {y--show-taint} \t print taint analysis results on stdout\n" + " {y--show-local-may-alias} \t perform procedure-local may alias analysis\n" "\n" "C/C++ frontend options:\n" HELP_CONFIG_C_CPP @@ -779,22 +770,22 @@ void goto_analyzer_parse_optionst::help() HELP_CONFIG_PLATFORM "\n" "Program representations:\n" - " --show-parse-tree show parse tree\n" - " --show-symbol-table show loaded symbol table\n" + " {y--show-parse-tree} \t show parse tree\n" + " {y--show-symbol-table} \t show loaded symbol table\n" HELP_SHOW_GOTO_FUNCTIONS HELP_SHOW_PROPERTIES "\n" "Program instrumentation options:\n" - " --property id enable selected properties only\n" + " {y--property} {uid} \t enable selected properties only\n" HELP_GOTO_CHECK HELP_CONFIG_LIBRARY "\n" "Other options:\n" HELP_VALIDATE - " --version show version and exit\n" + " {y--version} \t show version and exit\n" HELP_FLUSH - " --verbosity # verbosity level\n" + " {y--verbosity} {u#} \t verbosity level\n" HELP_TIMESTAMP - "\n"; + "\n"); // clang-format on } diff --git a/src/goto-bmc/goto_bmc_parse_options.cpp b/src/goto-bmc/goto_bmc_parse_options.cpp index df1dadc712a..cf9a6836aed 100644 --- a/src/goto-bmc/goto_bmc_parse_options.cpp +++ b/src/goto-bmc/goto_bmc_parse_options.cpp @@ -3,6 +3,7 @@ #include "goto_bmc_parse_options.h" #include +#include #include #include @@ -81,18 +82,18 @@ int goto_bmc_parse_optionst::doit() void goto_bmc_parse_optionst::help() { - // clang-format off - log.status() << '\n' << banner_string("goto-bmc", CBMC_VERSION) << '\n' + log.status() << '\n' + << banner_string("goto-bmc", CBMC_VERSION) << '\n' << align_center_with_border("Copyright (C) 2023") << '\n' - << align_center_with_border("Diffblue Ltd.") << '\n' // NOLINT(*) - << + << align_center_with_border("Diffblue Ltd.") << '\n'; + + log.status() << help_formatter( "\n" - "Usage: Purpose:\n" + "Usage: \tPurpose:\n" "\n" - "goto-bmc [-?] [-h] [--help] show help\n" - "goto-bmc --version show version and exit\n" - // NOLINTNEXTLINE(*) - "goto-bmc [options] file.c ... perform bounded model checking on symex-ready goto-binary\n"; - // clang-format on + " {bgoto-bmc} [{y-?}] [{y-h}] [{y--help}] \t show this help\n" + " {bgoto-bmc} {y--version} \t show version and exit\n" + " {bgoto-bmc} [options] {ufile_name} \t perform bounded model checking on" + " symex-ready goto-binary {ufile_name}\n"); log.status() << messaget::eom; } diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index ab4ae30a3c6..cb8e1b0b53e 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -169,83 +169,75 @@ void run_property_decider( std::chrono::duration solver_runtime, bool set_pass = true); -// clang-format off -#define OPT_BMC \ - "(program-only)" \ - "(show-byte-ops)" \ - "(show-vcc)" \ - "(show-goto-symex-steps)" \ - "(show-points-to-sets)" \ - "(slice-formula)" \ - "(unwinding-assertions)" \ - "(no-unwinding-assertions)" \ - "(no-self-loops-to-assumptions)" \ - "(partial-loops)" \ - "(paths):" \ - "(show-symex-strategies)" \ - "(depth):" \ - "(max-field-sensitivity-array-size):" \ - "(no-array-field-sensitivity)" \ - "(graphml-witness):" \ - "(symex-complexity-limit):" \ - "(symex-complexity-failed-child-loops-limit):" \ - "(incremental-loop):" \ - "(unwind-min):" \ - "(unwind-max):" \ - "(ignore-properties-before-unwind-min)" \ - "(symex-cache-dereferences)" \ - OPT_UNWINDSET \ - -#define HELP_BMC \ - " --paths [strategy] explore paths one at a time\n" \ - " --show-symex-strategies list strategies for use with --paths\n" \ - " --show-goto-symex-steps show which steps symex travels, includes\n" \ - " diagnostic information\n" \ - " --show-points-to-sets show points-to sets for\n" \ - " pointer dereference. Requires --json-ui.\n" \ - " --program-only only show program expression\n" \ - " --show-byte-ops show all byte extracts and updates\n" \ - " --depth nr limit search depth\n" \ - " --max-field-sensitivity-array-size M\n" \ - " maximum size M of arrays for which field\n" \ - " sensitivity will be applied to array,\n" \ - " the default is 64\n" \ - " --no-array-field-sensitivity\n" \ - " deactivate field sensitivity for arrays, " \ - "this is\n" \ - " equivalent to setting the maximum field \n" \ - " sensitivity size for arrays to 0\n" \ - HELP_UNWINDSET \ - " --incremental-loop L check properties after each unwinding\n" \ - " of loop L\n" \ - " (use --show-loops to get the loop IDs)\n" \ - " --unwind-min nr start incremental-loop after nr unwindings\n" \ - " but before solving that iteration. If for\n" \ - " example it is 1, then the loop will be\n" \ - " unwound once, and immediately checked.\n" \ - " Note: this means for min-unwind 1 or\n"\ - " 0 all properties are checked.\n" \ - " --unwind-max nr stop incremental-loop after nr unwindings\n" \ - " --ignore-properties-before-unwind-min\n" \ - " do not check properties before unwind-min\n" \ - " when using incremental-loop\n" \ - " --show-vcc show the verification conditions\n" \ - " --slice-formula remove assignments unrelated to property\n" \ - " --unwinding-assertions generate unwinding assertions (cannot be\n" \ - " used with --cover)\n" \ - " --partial-loops permit paths with partial loops\n" \ - " --no-self-loops-to-assumptions\n" \ - " do not simplify while(1){} to assume(0)\n" \ - " --symex-complexity-limit N how complex (N) a path can become before\n" \ - " symex abandons it. Currently uses guard\n" \ - " size to calculate complexity. \n" \ - " --symex-complexity-failed-child-loops-limit N\n" \ - " how many child branches (N) in an\n" \ - " iteration are allowed to fail due to\n" \ - " complexity violations before the loop\n" \ - " gets blacklisted\n" \ - " --graphml-witness filename write the witness in GraphML format to filename\n" /* NOLINT(*) */ \ - " --symex-cache-dereferences enable caching of repeated dereferences\n" \ -// clang-format on +#define OPT_BMC \ + "(program-only)" \ + "(show-byte-ops)" \ + "(show-vcc)" \ + "(show-goto-symex-steps)" \ + "(show-points-to-sets)" \ + "(slice-formula)" \ + "(unwinding-assertions)" \ + "(no-unwinding-assertions)" \ + "(no-self-loops-to-assumptions)" \ + "(partial-loops)" \ + "(paths):" \ + "(show-symex-strategies)" \ + "(depth):" \ + "(max-field-sensitivity-array-size):" \ + "(no-array-field-sensitivity)" \ + "(graphml-witness):" \ + "(symex-complexity-limit):" \ + "(symex-complexity-failed-child-loops-limit):" \ + "(incremental-loop):" \ + "(unwind-min):" \ + "(unwind-max):" \ + "(ignore-properties-before-unwind-min)" \ + "(symex-cache-dereferences)" OPT_UNWINDSET + +#define HELP_BMC \ + " {y--paths} [strategy] \t explore paths one at a time\n" \ + " {y--show-symex-strategies} \t list strategies for use with {y--paths}\n" \ + " {y--show-goto-symex-steps} \t show which steps symex travels, includes " \ + "diagnostic information\n" \ + " {y--show-points-to-sets} \t show points-to sets for pointer dereference. " \ + "Requires {y--json-ui}.\n" \ + " {y--program-only} \t only show program expression\n" \ + " {y--show-byte-ops} \t show all byte extracts and updates\n" \ + " {y--depth} {unr} \t limit search depth\n" \ + " {y--max-field-sensitivity-array-size} {uM} \t " \ + "maximum size {uM} of arrays for which field sensitivity will be " \ + "applied to array, the default is 64\n" \ + " {y--no-array-field-sensitivity} \t " \ + "deactivate field sensitivity for arrays, this is equivalent to setting " \ + "the maximum field sensitivity size for arrays to 0\n" HELP_UNWINDSET \ + " {y--incremental-loop} {uL} \t " \ + "check properties after each unwinding of loop {uL} (use {y--show-loops} " \ + "to get the loop IDs)\n" \ + " {y--unwind-min} {unr} \t " \ + "start incremental-loop after {unr} unwindings but before solving that " \ + "iteration. If for example it is 1, then the loop will be unwound once, " \ + "and immediately checked. Note: this means for {y--unwind-min} 1 or 0 all " \ + "properties are checked.\n" \ + " {--unwind-max} {unr} \t stop incremental-loop after {unr} unwindings\n" \ + " {y--ignore-properties-before-unwind-min} \t " \ + "do not check properties before unwind-min when using " \ + "{y--incremental-loop}\n" \ + " {y--show-vcc} \t show the verification conditions\n" \ + " {y--slice-formula} \t remove assignments unrelated to property\n" \ + " {y--unwinding-assertions} \t generate unwinding assertions (cannot be " \ + "used with {y--cover})\n" \ + " {y--partial-loops} \t permit paths with partial loops\n" \ + " {y--no-self-loops-to-assumptions} \t do not simplify while(1){} to " \ + "assume(0)\n" \ + " {y--symex-complexity-limit} {uN} \t " \ + "how complex ({uN}) a path can become before symex abandons it. Currently " \ + "uses guard size to calculate complexity.\n" \ + " {y--symex-complexity-failed-child-loops-limit} {uN} \t " \ + "how many child branches ({uN}) in an iteration are allowed to fail due to " \ + "complexity violations before the loop gets blacklisted\n" \ + " {y--graphml-witness} {ufilename} \t write the witness in GraphML format " \ + "to {ufilename}\n" \ + " {y--symex-cache-dereferences} \t enable caching of repeated " \ + "dereferences\n" #endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h index 40f46ce7f60..c172e9bd2ec 100644 --- a/src/goto-checker/solver_factory.h +++ b/src/goto-checker/solver_factory.h @@ -116,36 +116,35 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options); "(write-solver-stats-to):" #define HELP_SOLVER \ - " --external-sat-solver cmd command to invoke SAT solver process\n" \ - " --no-sat-preprocessor disable the SAT solver's simplifier\n" \ - " --dimacs generate CNF in DIMACS format\n" \ - " --beautify beautify the counterexample\n" \ - " (greedy heuristic)\n" \ - " --smt1 use default SMT1 solver (obsolete)\n" \ - " --smt2 use default SMT2 solver (Z3)\n" \ - " --bitwuzla use Bitwuzla\n" \ - " --boolector use Boolector\n" \ - " --sat-solver solver use specified SAT solver\n" \ - " --cprover-smt2 use CPROVER SMT2 solver\n" \ - " --cvc3 use CVC3\n" \ - " --cvc4 use CVC4\n" \ - " --cvc5 use CVC5\n" \ - " --mathsat use MathSAT\n" \ - " --yices use Yices\n" \ - " --z3 use Z3\n" \ - " --fpa use theory of floating-point arithmetic\n" \ - " --refine use refinement procedure (experimental)\n" \ - " --refine-arrays use refinement for arrays only\n" \ - " --refine-arithmetic refinement of arithmetic expressions only\n" \ - " --max-node-refinement maximum refinement iterations for\n" \ - " arithmetic expressions\n" \ - " --incremental-smt2-solver cmd\n" \ - " command to invoke external SMT solver for\n" \ - " incremental solving (experimental)\n" \ - " --outfile filename output formula to given file\n" \ - " --dump-smt-formula filename output smt incremental formula to the\n" \ - " given file\n" \ - " --write-solver-stats-to json-file\n" \ - " collect the solver query complexity\n" + " {y--sat-solver} {usolver} \t use specified SAT solver\n" \ + " {y--external-sat-solver} {ucmd} \t command to invoke SAT solver process\n" \ + " {y--no-sat-preprocessor} \t disable the SAT solver's simplifier\n" \ + " {y--dimacs} \t generate CNF in DIMACS format\n" \ + " {y--beautify} \t beautify the counterexample (greedy heuristic)\n" \ + " {y--smt1} \t use default SMT1 solver (obsolete)\n" \ + " {y--smt2} \t use default SMT2 solver (Z3)\n" \ + " {y--bitwuzla} \t use Bitwuzla\n" \ + " {y--boolector} \t use Boolector\n" \ + " {y--cprover-smt2} \t use CPROVER SMT2 solver\n" \ + " {y--cvc3} \t use CVC3\n" \ + " {y--cvc4} \t use CVC4\n" \ + " {y--cvc5} \t use CVC5\n" \ + " {y--mathsat} \t use MathSAT\n" \ + " {y--yices} \t use Yices\n" \ + " {y--z3} \t use Z3\n" \ + " {y--fpa} \t use theory of floating-point arithmetic\n" \ + " {y--refine} \t use refinement procedure (experimental)\n" \ + " {y--refine-arrays} \t use refinement for arrays only\n" \ + " {y--refine-arithmetic} \t refinement of arithmetic expressions only\n" \ + " {y--max-node-refinement} \t " \ + "maximum refinement iterations for arithmetic expressions\n" \ + " {y--incremental-smt2-solver} {ucmd} \t " \ + "command to invoke external SMT solver for incremental solving " \ + "(experimental)\n" \ + " {y--outfile} {ufilename} \t output formula to given file\n" \ + " {y--dump-smt-formula} {ufilename} \t " \ + "output smt incremental formula to the given file\n" \ + " {y--write-solver-stats-to} {ujson-file} \t " \ + "collect the solver query complexity\n" #endif // CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 52c3f984f2f..55a129324b9 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -13,6 +13,7 @@ Author: Peter Schrammel #include #include +#include #include #include @@ -220,35 +221,34 @@ void goto_diff_parse_optionst::help() std::cout << '\n' << banner_string("GOTO_DIFF", CBMC_VERSION) << '\n' << align_center_with_border("Copyright (C) 2016") << '\n' << align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT (*) - << align_center_with_border("kroening@kroening.com") << '\n' - << + << align_center_with_border("kroening@kroening.com") << '\n'; + + std::cout << help_formatter( "\n" - "Usage: Purpose:\n" + "Usage: \tPurpose:\n" "\n" - " goto_diff [-?] [-h] [--help] show help\n" - " goto_diff old new goto binaries to be compared\n" + " {bgoto-diff} [{y-?}] [{y-h}] [{y--help}] \t show this help\n" + " {bgoto-diff} {uold} {unew} \t compare two goto binaries\n" "\n" "Diff options:\n" HELP_SHOW_GOTO_FUNCTIONS HELP_SHOW_PROPERTIES - " --show-loops show the loops in the programs\n" - " -u | --unified output unified diff\n" - " --change-impact | \n" - " --forward-impact |\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n" - " --compact-output output dependencies in compact mode\n" + " {y--show-loops} \t show the loops in the programs\n" + " {y-u}, {y--unified} \t output unified diff\n" + " {y--change-impact}, {y--forward-impact}, {y--backward-impact} \t output" + " unified diff with forward&backward/forward/backward dependencies\n" + " {y--compact-output} \t output dependencies in compact mode\n" "\n" "Program instrumentation options:\n" HELP_GOTO_CHECK HELP_COVER "\n" "Other options:\n" - " --version show version and exit\n" - " --json-ui use JSON-formatted output\n" + " {y--version} \t show version and exit\n" + " {y--json-ui} \t use JSON-formatted output\n" HELP_FLUSH - " --verbosity # verbosity level\n" + " {y--verbosity} {u#} \t verbosity level\n" HELP_TIMESTAMP - "\n"; + "\n"); // clang-format on } diff --git a/src/goto-harness/common_harness_generator_options.h b/src/goto-harness/common_harness_generator_options.h index 5d39f44d8a6..5dc0d28cc1e 100644 --- a/src/goto-harness/common_harness_generator_options.h +++ b/src/goto-harness/common_harness_generator_options.h @@ -18,39 +18,41 @@ Author: Diffblue Ltd. "function-pointer-can-be-null" #define COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT "havoc-member" -// clang-format off #define COMMON_HARNESS_GENERATOR_OPTIONS \ - "(" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "):" \ - "(" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):" \ - "(" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "):" \ - "(" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):" \ - "(" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT "):" \ - "(" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT "):" \ -// COMMON_HARNESS_GENERATOR_OPTIONS + "(" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT \ + "):" \ + "(" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \ + "):" \ + "(" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT \ + "):" \ + "(" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT \ + "):" \ + "(" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \ + "):" \ + "(" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT "):" -// clang-format on - -// clang-format off #define COMMON_HARNESS_GENERATOR_HELP \ - "--" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT \ - " N minimum level at which a pointer can first be NULL\n" \ - " in a recursively nondet initialized struct\n" \ - "--" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \ - " N limit size of nondet (e.g. input) object tree;\n" \ - " at level N pointers are set to null\n" \ - "--" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT \ - " N minimum size of dynamically created arrays\n" \ - " (default: 1)\n" \ - "--" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT \ - " N maximum size of dynamically created arrays\n" \ - " (default: 2)\n" \ - "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \ - " , name of the function(s) pointer parameters\n" \ - " that can be NULL pointing.\n" \ - "--" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT \ - " path to the member to be havoced\n" \ - // COMMON_HARNESS_GENERATOR_HELP - -// clang-format on + " {y--" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT \ + "} {uN} \t " \ + "minimum level at which a pointer can first be NULL in a recursively " \ + "nondet initialized struct\n" \ + " {y--" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \ + "} {uN} \t " \ + "limit size of nondet (e.g. input) object tree; at level {uN} pointers " \ + "are set to null\n" \ + " {y--" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT \ + "} {uN} \t " \ + "minimum size of dynamically created arrays (default: 1)\n" \ + " {y--" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT \ + "} {uN} \t " \ + "maximum size of dynamically created arrays (default: 2)\n" \ + " {y--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \ + "} " \ + "{ufunction_name} \t " \ + "name of the function(s) pointer parameters that can be NULL " \ + "pointing\n" \ + " {y--" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT \ + "} {umember_expr} \t " \ + "path to the member to be havocked\n" #endif // CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H diff --git a/src/goto-harness/function_harness_generator_options.h b/src/goto-harness/function_harness_generator_options.h index 477b53a8aff..c8b7d48c9d1 100644 --- a/src/goto-harness/function_harness_generator_options.h +++ b/src/goto-harness/function_harness_generator_options.h @@ -24,48 +24,52 @@ Author: Diffblue Ltd. #define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT \ "treat-pointers-equal-maybe" -// clang-format off #define FUNCTION_HARNESS_GENERATOR_OPTIONS \ - "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):" \ - "(" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT ")" \ - "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT "):" \ - "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT "):" \ - "(" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT "):" \ - "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING "):" \ - "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT ")" \ -// FUNCTION_HARNESS_GENERATOR_OPTIONS + "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT \ + "):" \ + "(" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT \ + ")" \ + "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \ + "):" \ + "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT \ + "):" \ + "(" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \ + "):" \ + "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING \ + "):" \ + "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT ")" -// clang-format on - -// clang-format off #define FUNCTION_HARNESS_GENERATOR_HELP \ - "function harness generator (--harness-type call-function)\n\n" \ - "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT \ - " the function the harness should call\n" \ - "--" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT \ - " set global variables to non-deterministic values\n" \ - " in harness\n" \ - COMMON_HARNESS_GENERATOR_HELP \ - "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \ - " p treat the function parameter with the name `p' as\n" \ - " an array\n" \ - "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT \ - " p,q,r[;s,t] treat the function parameters `q,r' equal\n" \ - " to parameter `p'; `s` to `t` and so on\n" \ - "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT \ - " function parameters equality is non-deterministic\n" \ - "--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \ - " array_name:size_name\n" \ - " set the parameter to the size" \ - " of\n the array \n" \ - " (implies " \ - "-- " FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \ - " )\n" \ - "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING \ - " p treat the function parameter with the name `p' as\n" \ - " a string of characters\n" \ - // FUNCTION_HARNESS_GENERATOR_HELP - -// clang-format on + "function harness generator ({y--harness-type} {ycall-function}):\n" \ + " {y--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT \ + "} {ufunction_name} \t " \ + "the function the harness should call\n" \ + " {y--" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT \ + "} \t " \ + "set global variables to non-deterministic values in " \ + "harness\n" COMMON_HARNESS_GENERATOR_HELP \ + " {y--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \ + "} {up} \t " \ + "treat the function parameter with the name {up} as an array\n" \ + " {y--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT \ + "} " \ + "{up}{y,}{uq}{y,}{ur}[{y;}{us}{y,}{ut}] \t " \ + "treat the function parameters {uq}{y,}{ur} equal to parameter {up}; " \ + "{us} to {ut} and so on\n" \ + " {y--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT \ + "} \t " \ + "function parameters equality is non-deterministic\n" \ + " {y--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \ + "} " \ + "{uarray_name}{y:}{usize_name} \t " \ + "set the parameter {usize_name} to the size of the array {uarray_name} " \ + "(implies " \ + "{y-- " FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \ + "} " \ + "{uarray_name})\n" \ + " {y--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING \ + "} {up} \t " \ + "treat the function parameter with the name {up} as a string of " \ + "characters\n" #endif // CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp index 427283eaa2b..56741e3e1d6 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -11,6 +11,7 @@ Author: Diffblue Ltd. #include #include #include +#include #include #include #include @@ -172,32 +173,35 @@ int goto_harness_parse_optionst::doit() void goto_harness_parse_optionst::help() { - std::cout - << '\n' - << banner_string("Goto-Harness", CBMC_VERSION) << '\n' - << align_center_with_border("Copyright (C) 2019") << '\n' - << align_center_with_border("Diffblue Ltd.") << '\n' - << align_center_with_border("info@diffblue.com") << '\n' - << '\n' - << "Usage: Purpose:\n" - << '\n' - << " goto-harness [-?] [-h] [--help] show help\n" - << " goto-harness --version show version\n" - << " goto-harness --harness-function-name --harness-type " - " [harness options]\n" - << "\n" - << " goto binary to read from\n" - << " file to write the harness to\n" - << " the harness is printed as C code, if " - "has a .c suffix,\n" - " else a goto binary including the harness is " - "generated\n" - << "--harness-function-name the name of the harness function to " - "generate\n" - << "--harness-type one of the harness types listed below\n" - << "\n\n" - << FUNCTION_HARNESS_GENERATOR_HELP << "\n\n" - << MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP << '\n'; + std::cout << '\n' + << banner_string("Goto-Harness", CBMC_VERSION) << '\n' + << align_center_with_border("Copyright (C) 2019") << '\n' + << align_center_with_border("Diffblue Ltd.") << '\n' + << align_center_with_border("info@diffblue.com") << '\n'; + + // clang-format off + std::cout << help_formatter( + "\n" + "Usage: \tPurpose:\n" + "\n" + " {bgoto-harness} [{y-?}] [{y-h}] [{y--help}] \t show this help\n" + " {bgoto-harness} {y--version} \t show version and exit\n" + " {bgoto-harness} {uin} {uout} {y--harness-function-name} {uname}" + " {y--harness-type} {uharness-type} [harness options]\n" + "\n" + " {uin} \t goto binary to read from\n" + " {uout} \t file to write the harness to; the harness is printed as C" + " code, if {uout} has a .c suffix, else a goto binary including the harness" + " is generated\n" + " {y--harness-function-name} {uname} \t the name of the harness function to" + " generate\n" + " {y--harness-type} {utype} \t one of the harness types listed below\n" + "\n" + FUNCTION_HARNESS_GENERATOR_HELP + "\n" + MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP + "\n"); + // clang-format on } goto_harness_parse_optionst::goto_harness_parse_optionst( diff --git a/src/goto-harness/memory_snapshot_harness_generator_options.h b/src/goto-harness/memory_snapshot_harness_generator_options.h index 8f95bcdb7c7..b9044591e49 100644 --- a/src/goto-harness/memory_snapshot_harness_generator_options.h +++ b/src/goto-harness/memory_snapshot_harness_generator_options.h @@ -18,46 +18,47 @@ Author: Diffblue Ltd. #define MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT "pointer-as-array" #define MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT "size-of-array" -// clang-format off #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS \ - "(" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT "):" \ - "(" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT "):" \ - "(" MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT "):" \ - "(" MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT "):" \ - "(" MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT "):" \ - "(" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT "):" \ -// MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS + "(" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT \ + "):" \ + "(" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT \ + "):" \ + "(" MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT \ + "):" \ + "(" MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT \ + "):" \ + "(" MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT \ + "):" \ + "(" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT "):" -// clang-format on - -// clang-format off #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP \ - "memory snapshot harness generator (--harness-type\n" \ - " initialize-with-memory-snapshot)\n\n" \ - "--" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT " initialise memory " \ - "from JSON memory snapshot\n" \ - "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT " ]>\n" \ - " use given function and location number as " \ - "entry\n point\n" \ - "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT " >\n" \ - " use given file name and line number as " \ - "entry\n point\n" \ - "--" MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT " vars initialise" \ - " variables from `vars' to\n" \ - " non-deterministic values\n" \ - COMMON_HARNESS_GENERATOR_HELP \ - "--" MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT \ - " p treat the global pointer with the name `p' as\n" \ - " an array\n" \ - "--" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT \ - " array_name:size_name\n" \ - " set the parameter to the size" \ - " of\n the array \n" \ - " (implies " \ - "-- " MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT \ - " )\n" \ -// MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP - -// clang-format on + "memory snapshot harness generator ({y--harness-type}\n" \ + " {yinitialize-with-memory-snapshot}):\n" \ + " {y--" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT \ + "} {ufile} \t " \ + "initialize memory from JSON memory snapshot\n" \ + " {y--" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT \ + "} {ufunc}[{y:}{un}] " \ + "\t " \ + "use given function and location number as entry point\n" \ + " {y--" MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT \ + "} {ufile}{y:}{un} " \ + "\t " \ + "use given file name and line number as entry point\n" \ + " {y--" MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT \ + "} {uvars} \t " \ + "initialize variables from {uvars} to non-deterministic " \ + "values\n" COMMON_HARNESS_GENERATOR_HELP \ + " {y--" MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT \ + "} {up} \t " \ + "treat the global pointer with the name {up} as an array\n" \ + " {y--" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT \ + "} " \ + "{uarray_name}{y:}{usize_name} \t " \ + "set the parameter {usize_name} to the size of the array {uarray_name} " \ + "(implies " \ + "{y-- " MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT \ + "} " \ + "{uarray_name})\n" #endif // CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS_H diff --git a/src/goto-inspect/goto_inspect_parse_options.cpp b/src/goto-inspect/goto_inspect_parse_options.cpp index 441fcc268cc..d9e4bc02417 100644 --- a/src/goto-inspect/goto_inspect_parse_options.cpp +++ b/src/goto-inspect/goto_inspect_parse_options.cpp @@ -5,6 +5,7 @@ #include #include #include +#include #include #include @@ -76,16 +77,17 @@ void goto_inspect_parse_optionst::help() << banner_string("Goto-Inspect", CBMC_VERSION) << '\n' << align_center_with_border("Copyright (C) 2023") << '\n' << align_center_with_border("Diffblue Ltd.") << '\n' - << align_center_with_border("info@diffblue.com") << '\n' - << '\n' - << "Usage: Purpose:\n" - << '\n' - << " goto-inspect [-?] [-h] [--help] show help\n" - << " goto-inspect --version show version\n" - << " goto-inspect --show-goto-functions show code for " - "goto-functions present in goto-binary\n" - << "\n" - << " goto binary to read from\n"; + << align_center_with_border("info@diffblue.com") << '\n'; + + std::cout << help_formatter( + "\n" + "Usage: \tPurpose:\n" + "\n" + " {bgoto-inspect} [{y-?}] [{y-h}] [{y--help}] \t show this help\n" + " {bgoto-inspect} {y--version} \t show version and exit\n" + " {bgoto-inspect} {y--show-goto-functions} {ufile_name} \t show code for" + " goto-functions present in goto-binary {ufile_name}\n" + "\n"); } goto_inspect_parse_optionst::goto_inspect_parse_optionst( diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index ce0c061c6f5..ddf4358bc57 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -29,32 +29,28 @@ Date: February 2016 #include #include -// clang-format off #define FLAG_LOOP_CONTRACTS "apply-loop-contracts" #define HELP_LOOP_CONTRACTS \ - " --apply-loop-contracts\n" \ - " check and use loop contracts when provided\n" + " {y--apply-loop-contracts} \t check and use loop contracts when provided\n" #define FLAG_LOOP_CONTRACTS_NO_UNWIND "loop-contracts-no-unwind" #define HELP_LOOP_CONTRACTS_NO_UNWIND \ - " --loop-contracts-no-unwind\n" \ - " do not unwind transformed loops\n" + " {y--loop-contracts-no-unwind} \t do not unwind transformed loops\n" #define FLAG_LOOP_CONTRACTS_FILE "loop-contracts-file" #define HELP_LOOP_CONTRACTS_FILE \ - " --loop-contracts-file \n" \ - " parse and annotate loop contracts from files\n" + " {y--loop-contracts-file} {ufile} \t " \ + "parse and annotate loop contracts from files\n" #define FLAG_REPLACE_CALL "replace-call-with-contract" #define HELP_REPLACE_CALL \ - " --replace-call-with-contract [/contract]\n" \ - " replace calls to function with contract\n" + " {y--replace-call-with-contract} {ufunction}[/{ucontract}] \t " \ + "replace calls to {ufunction} with {ucontract}\n" #define FLAG_ENFORCE_CONTRACT "enforce-contract" #define HELP_ENFORCE_CONTRACT \ - " --enforce-contract [/contract]" \ - " wrap function with an assertion of contract\n" -// clang-format on + " {y--enforce-contract} {ufunction}[/{ucontract}] \t " \ + "wrap function with an assertion of contract\n" class local_may_aliast; diff --git a/src/goto-instrument/count_eloc.h b/src/goto-instrument/count_eloc.h index eb719d08a55..9062b3a207a 100644 --- a/src/goto-instrument/count_eloc.h +++ b/src/goto-instrument/count_eloc.h @@ -28,12 +28,11 @@ void print_global_state_size(const goto_modelt &); "(print-path-lengths)" #define HELP_GOTO_PROGRAM_STATS \ - " --count-eloc count effective lines of code\n" \ - " --list-eloc list full path names of lines " \ - "containing code\n" \ - " --print-global-state-size count the total number of bits of global " \ - "objects\n" \ - " --print-path-lengths print statistics about control-flow graph " \ - "paths\n" + " {y--count-eloc} \t count effective lines of code\n" \ + " {y--list-eloc} \t list full path names of lines containing code\n" \ + " {y--print-global-state-size} \t " \ + "count the total number of bits of global objects\n" \ + " {y--print-path-lengths} \t " \ + "print statistics about control-flow graph paths\n" #endif // CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 84ec1873095..4d5026d3a9a 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -31,19 +31,16 @@ class symbol_tablet; "(show-test-suite)" #define HELP_COVER \ - " --cover CC create test-suite with coverage criterion " \ - "CC,\n" \ - " where CC is one of assertion[s], " \ - "assume[s],\n" \ - " branch[es], condition[s], cover, " \ - "decision[s],\n" \ - " location[s], or mcdc\n" \ - " --cover-failed-assertions do not stop coverage checking at failed " \ - "assertions\n" \ - " (this is the default for --cover " \ - "assertions)\n" \ - " --show-test-suite print test suite for coverage criterion " \ - "(requires --cover)\n" + " {y--cover} {uCC} \t " \ + "create test-suite with coverage criterion {uCC}, where {uCC} is one of " \ + "{yassertion}[{ys}], {yassume}[{ys}], {ybranch}[{yes}], " \ + "{ycondition}[{ys}], {ycover}, {decision}[{ys}], {ylocation}[{ys}], " \ + "or {ymcdc}\n" \ + " {y--cover-failed-assertions} \t " \ + "do not stop coverage checking at failed assertions (this is the default " \ + "for {y--cover} {yassertions})\n" \ + " {y--show-test-suite} \t " \ + "print test suite for coverage criterion (requires {y--cover})\n" enum class coverage_criteriont { diff --git a/src/goto-instrument/document_properties.h b/src/goto-instrument/document_properties.h index f48f9440f00..01c21528f2a 100644 --- a/src/goto-instrument/document_properties.h +++ b/src/goto-instrument/document_properties.h @@ -28,11 +28,8 @@ void document_properties_html( "(document-claims-latex)(document-claims-html)" \ "(document-properties-latex)(document-properties-html)" -// clang-format off #define HELP_DOCUMENT_PROPERTIES \ - " --document-properties-html generate HTML property documentation\n" \ - " --document-properties-latex generate Latex property documentation\n" - -// clang-format on + " {y--document-properties-html} \t generate HTML property documentation\n" \ + " {y--document-properties-latex} \t generate LaTeX property documentation\n" #endif // CPROVER_GOTO_INSTRUMENT_DOCUMENT_PROPERTIES_H diff --git a/src/goto-instrument/dump_c.h b/src/goto-instrument/dump_c.h index 69820a33d3f..b36925d2549 100644 --- a/src/goto-instrument/dump_c.h +++ b/src/goto-instrument/dump_c.h @@ -48,15 +48,13 @@ void dump_cpp( "(dump-c-type-header):" \ "(no-system-headers)(use-all-headers)(harness)" -// clang-format off #define HELP_DUMP_C \ - " --dump-c generate C source\n" \ - " --dump-c-type-header m generate a C header for types local in m\n" \ - " --dump-cpp generate C++ source\n" \ - " --no-system-headers generate C source expanding libc includes\n"\ - " --use-all-headers generate C source with all includes\n" \ - " --harness include input generator in output\n" - -// clang-format on + " {y--dump-c} \t generate C source\n" \ + " {y--dump-c-type-header} {um} \t " \ + "generate a C header for types local in {um}\n" \ + " {y--dump-cpp} \t generate C++ source\n" \ + " {y--no-system-headers} \t generate C source expanding libc includes\n" \ + " {y--use-all-headers} \t generate C source with all includes\n" \ + " {y--harness} \t include input generator in output\n" #endif // CPROVER_GOTO_INSTRUMENT_DUMP_C_H diff --git a/src/goto-instrument/generate_function_bodies.h b/src/goto-instrument/generate_function_bodies.h index aa4d6dc6fc7..2f4cb2380c5 100644 --- a/src/goto-instrument/generate_function_bodies.h +++ b/src/goto-instrument/generate_function_bodies.h @@ -84,29 +84,24 @@ void generate_function_bodies( goto_modelt &model, message_handlert &message_handler); -// clang-format off #define OPT_REPLACE_FUNCTION_BODY \ "(generate-function-body):" \ "(generate-havocing-body):" \ "(generate-function-body-options):" -#define HELP_REPLACE_FUNCTION_BODY \ - " --generate-function-body \n" \ - /* NOLINTNEXTLINE(whitespace/line_length) */ \ - " Generate bodies for functions matching regex\n" \ - " --generate-havocing-body