From 58fcebf5772671b50efe06327b72305d56a65cc7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 10 Aug 2023 11:35:56 +0000 Subject: [PATCH 1/4] Add unit test of help_formatter Modelled after help_entry's unit test. --- unit/Makefile | 1 + unit/util/help_formatter.cpp | 21 +++++++++++++++++++++ 2 files changed, 22 insertions(+) create mode 100644 unit/util/help_formatter.cpp diff --git a/unit/Makefile b/unit/Makefile index 59b3c5455eb..1653c2a3453 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -144,6 +144,7 @@ SRC += analyses/ai/ai.cpp \ util/format_number_range.cpp \ util/get_base_name.cpp \ util/graph.cpp \ + util/help_formatter.cpp \ util/interval/add.cpp \ util/interval/bitwise.cpp \ util/interval/comparisons.cpp \ diff --git a/unit/util/help_formatter.cpp b/unit/util/help_formatter.cpp new file mode 100644 index 00000000000..8e520eb2959 --- /dev/null +++ b/unit/util/help_formatter.cpp @@ -0,0 +1,21 @@ +/******************************************************************\ + +Module: help formatter unit tests + +Author: Michael Tautschnig + +\******************************************************************/ + +#include + +#include + +#include + +TEST_CASE("help_formatter", "[core][util]") +{ + std::ostringstream oss; + oss.clear(); + oss << help_formatter("--abc \t xyz\n"); + REQUIRE(oss.str() == "--abc xyz\n"); +} From 89b3740f5e392a7a027d7890e8e42162f5528239 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 14 Jun 2022 21:54:13 +0000 Subject: [PATCH 2/4] Use help_entry to consistently format help output We previously did manual line breaks that either suited the source code line length or approximated the output line width. help_entry, however, was specifically built to take care of this (and just wasn't widely used). We can then also happily have clang-format take care of source code formatting without impacting the resulting display. --- .../src/janalyzer/janalyzer_parse_options.cpp | 132 +++--- .../java_bytecode/java_bytecode_language.h | 219 +++++----- .../src/java_bytecode/java_trace_validation.h | 7 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 143 ++++--- jbmc/src/jdiff/jdiff_parse_options.cpp | 36 +- .../variable_sensitivity_domain.h | 40 +- src/ansi-c/ansi_c_language.h | 12 +- src/ansi-c/goto_check_c.h | 61 ++- src/cbmc/cbmc_parse_options.cpp | 122 +++--- .../goto_analyzer_parse_options.cpp | 194 ++++----- src/goto-checker/bmc_util.h | 165 ++++---- src/goto-checker/solver_factory.h | 66 +-- src/goto-diff/goto_diff_parse_options.cpp | 37 +- .../common_harness_generator_options.h | 64 +-- .../function_harness_generator_options.h | 83 ++-- .../goto_harness_parse_options.cpp | 13 +- ...emory_snapshot_harness_generator_options.h | 72 ++-- src/goto-instrument/contracts/contracts.h | 24 +- src/goto-instrument/count_eloc.h | 16 +- src/goto-instrument/cover.h | 25 +- src/goto-instrument/document_properties.h | 10 +- src/goto-instrument/dump_c.h | 17 +- .../generate_function_bodies.h | 36 +- .../goto_instrument_parse_options.cpp | 379 +++++++++++------- .../insert_final_assert_false.h | 10 +- src/goto-instrument/reachability_slicer.h | 28 +- src/goto-instrument/replace_calls.h | 2 +- src/goto-instrument/uninitialized.h | 5 +- src/goto-instrument/unwindset.h | 11 +- src/goto-instrument/wmm/weak_memory.h | 73 ++-- src/goto-programs/class_hierarchy.h | 6 +- src/goto-programs/goto_trace.h | 13 +- .../rebuild_goto_start_function.h | 6 - src/goto-programs/remove_calls_no_body.h | 3 +- .../remove_const_function_pointers.h | 6 +- .../restrict_function_pointers.h | 31 +- src/goto-programs/show_goto_functions.h | 8 +- src/goto-programs/show_properties.h | 6 +- .../goto_synthesizer_parse_options.cpp | 12 +- src/json/json_interface.h | 8 +- src/langapi/language.h | 3 +- .../memory_analyzer_parse_options.cpp | 13 +- .../goto_program_dereference.h | 7 +- src/solvers/strings/string_refinement.h | 36 +- src/symtab2gb/symtab2gb_parse_options.cpp | 9 +- src/util/config.h | 156 +++---- src/util/timestamper.h | 9 +- src/util/ui_message.h | 2 +- src/util/validation_interface.h | 12 +- src/xmllang/xml_interface.h | 4 +- 50 files changed, 1324 insertions(+), 1128 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index d233a47f710..58f66c433d1 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -727,76 +727,86 @@ void janalyzer_parse_optionst::help() "\n" " janalyzer [-?] [-h] [--help] show help\n" " janalyzer\n" - HELP_JAVA_METHOD_NAME - " janalyzer\n" - HELP_JAVA_CLASS_NAME - " janalyzer\n" - HELP_JAVA_JAR - " janalyzer\n" - HELP_JAVA_GOTO_BINARY - "\n" - HELP_JAVA_CLASSPATH - HELP_FUNCTIONS - "\n" + << HELP_JAVA_METHOD_NAME + << " janalyzer\n" + << HELP_JAVA_CLASS_NAME + << " janalyzer\n" + << HELP_JAVA_JAR + << " janalyzer\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" - "\n" + << help_entry("--show", "display the abstract domains") + << help_entry("--verify", "use the abstract domains to check assertions") + << help_entry( + "--simplify file_name", + "use the abstract domains to simplify the program") + << help_entry( + "--no-simplify-slicing", + "do not remove instructions from which no property can be reached (use " + "with --simplify)") + << help_entry("--unreachable-instructions", "list dead code") + << help_entry( + "--unreachable-functions", + "list functions unreachable from the entry point") + << help_entry( + "--reachable-functions", "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" - "\n" + << help_entry( + "--location-sensitive", "use location-sensitive abstract interpreter") + << help_entry("--concurrent", "use concurrency-aware abstract interpreter") + << "\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(*) - "\n" + << help_entry("--constants", "constant domain") + << help_entry("--intervals", "interval domain") + << help_entry("--non-null", "non-null domain") + << help_entry( + "--dependence-graph", + "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" - "\n" + << help_entry( + "--text file_name", "output results in plain text to given file") + << help_entry( + "--json file_name", "output results in JSON format to given file") + << help_entry( + "--xml file_name", "output results in XML format to given file") + << help_entry( + "--dot file_name", "output results in DOT format to given file") + << "\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" - "\n" + << help_entry( + "--taint file_name", "perform taint analysis using rules in given file") + << help_entry( + "--show-taint", "print taint analysis results on stdout") + << help_entry( + "--show-local-may-alias", "perform procedure-local may alias analysis") + << "\n" "Java Bytecode frontend options:\n" - JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP - "\n" + << JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP + << "\n" "Platform options:\n" - HELP_CONFIG_PLATFORM - "\n" + << HELP_CONFIG_PLATFORM + << "\n" "Program representations:\n" - " --show-parse-tree show parse tree\n" - " --show-symbol-table show loaded symbol table\n" - HELP_SHOW_GOTO_FUNCTIONS - HELP_SHOW_PROPERTIES - "\n" + << help_entry("--show-parse-tree", "show parse tree") + << help_entry("--show-symbol-table", "show loaded symbol table") + << 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" - "\n" + << help_entry("--no-assertions", "ignore user assertions") + << help_entry("--no-assumptions", "ignore user assumptions") + << help_entry("--property id", "enable selected properties only") + << "\n" "Other options:\n" - " --version show version and exit\n" - " --verbosity # verbosity level\n" - HELP_TIMESTAMP - "\n"; + << help_entry("--version", "show version and exit") + << help_entry("--verbosity #", "verbosity level") + << HELP_TIMESTAMP + << "\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..1c93b1fdb05 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -53,81 +53,95 @@ Author: Daniel Kroening, kroening@kroening.com "(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(*) */ + help_entry( \ + "--disable-uncaught-exception-check", \ + "ignore uncaught exceptions and errors") \ + << help_entry( \ + "--throw-assertion-error", \ + "throw java.lang.AssertionError on violated assert statements instead of " \ + "failing at the location of the assert statement") \ + << help_entry( \ + "--throw-runtime-exceptions", \ + "make implicit runtime exceptions explicit") \ + << help_entry( \ + "--assert-no-exceptions-thrown", \ + "transform `throw` instructions into `assert FALSE` followed by `assume " \ + "FALSE`.") \ + << help_entry( \ + "--max-nondet-array-length N", \ + "limit nondet (e.g. input) array size to <= N") \ + << help_entry( \ + "--max-nondet-tree-depth N", \ + "limit size of nondet (e.g. input) object tree; at level N references " \ + "are set to null") \ + << help_entry( \ + "--java-assume-inputs-non-null", \ + "never initialize reference-typed parameter to the entry point with null") \ + << help_entry( \ + "--java-assume-inputs-interval [L:U] or [L:] or [:U]", \ + "force numerical primitive-typed inputs (byte, short, int, long, float, " \ + "double) to be initialized within the given range; lower bound L and " \ + "upper bound U must be integers; does not work for arrays;") \ + << help_entry( \ + "--java-assume-inputs-integral", \ + "force float and double inputs to have integer values; does not work for " \ + "arrays;") \ + << help_entry( \ + "--java-max-vla-length N", \ + "limit the length of user-code-created arrays") \ + << help_entry( \ + "--java-cp-include-files r", \ + "regexp or JSON list of files to load (with '@' prefix)") \ + << help_entry( \ + "--java-load-class CLASS", \ + "also load code from class CLASS") \ + << help_entry( \ + "--java-no-load-class_CLASS", \ + "never load code from class CLASS") \ + << help_entry( \ + "--ignore-manifest-main-class", \ + "ignore Main-Class entries in JAR manifest files. If this option is " \ + "specified and the options --function and --main-class are not, we can " \ + "be certain that all classes in the JAR file are loaded.") \ + << help_entry( \ + "--context-include i", \ + "only analyze code matching specification i that") \ + << help_entry( \ + "--context-exclude e", \ + "does not match specification e. 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'.") \ + << help_entry( \ + "--no-lazy-methods", \ + "load and translate all methods given on the command line and in " \ + "--classpath. Default is to load methods that appear to be reachable " \ + "from the --function entry point or main class Note that " \ + "--show-symbol-table, --show-goto-functions and --show-properties output " \ + "are restricted to loaded methods by default.") \ + << help_entry( \ + "--lazy-methods-extra-entry-point METHODNAME", \ + "treat METHODNAME as a possible program entry point for the purpose of " \ + "lazy method loading METHODNAME 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.") \ + << help_entry( \ + "--static-values f", \ + "Load initial values of static fields from the given JSON file. 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.") \ + << help_entry( \ + "--java-lift-clinit-calls", \ + "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.") \ #ifdef _WIN32 #define JAVA_CLASSPATH_SEPARATOR ";" @@ -136,49 +150,46 @@ Author: Daniel Kroening, kroening@kroening.com #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" + help_entry( \ + "-classpath dirs/jars, -cp dirs/jars, --classpath dirs/jars", \ + "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") \ + << help_entry("--main-class class-name", "set the name of the main class") #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" + help_entry( \ + "method-name", \ + "fully qualified name of method used as entry point, e.g. " \ + "mypackage.Myclass.foo:(I)Z") #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" + help_entry( \ + "class-name", \ + "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.") #define OPT_JAVA_JAR /* NOLINT(*) */ \ "(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" + help_entry( \ + "-jar jarfile", \ + "JAR file to be checked. The entry point is the method specified by " \ + "--function or otherwise, the public static void main(String[]) method " \ + "of the class specified by --main-class or the main class specified in " \ + "the JAR manifes (checked in this order).") #define OPT_JAVA_GOTO_BINARY /* NOLINT(*) */ \ "(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" + help_entry( \ + "--gb goto-binary", \ + "goto-binary file to be checked. The entry point is the method specified " \ + "by --function, or otherwise, the public static void main(String[]) of " \ + "the class specified by --main-class (checked in this order).") // 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..9a02febfcc2 100644 --- a/jbmc/src/java_bytecode/java_trace_validation.h +++ b/jbmc/src/java_bytecode/java_trace_validation.h @@ -27,9 +27,10 @@ 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*/ \ + help_entry( \ + "--validate-trace", \ + "throw an error if the structure of the counterexample trace does not " \ + "match certain assumptions (experimental, currently java only)") // 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..454bc910cc5 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -966,82 +966,95 @@ void jbmc_parse_optionst::help() "\n" " jbmc [-?] [-h] [--help] show help\n" " jbmc\n" - HELP_JAVA_METHOD_NAME - " jbmc\n" - HELP_JAVA_CLASS_NAME - " jbmc\n" - HELP_JAVA_JAR - " jbmc\n" - HELP_JAVA_GOTO_BINARY - "\n" - HELP_JAVA_CLASSPATH - HELP_FUNCTIONS - "\n" + << HELP_JAVA_METHOD_NAME + << " jbmc\n" + << HELP_JAVA_CLASS_NAME + << " jbmc\n" + << HELP_JAVA_JAR + << " jbmc\n" + << HELP_JAVA_GOTO_BINARY + << "\n" + << HELP_JAVA_CLASSPATH + << HELP_FUNCTIONS + << "\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" - HELP_JAVA_TRACE_VALIDATION - "\n" + << HELP_SHOW_PROPERTIES + << help_entry( + "--symex-coverage-report f", + "generate a Cobertura XML coverage report in f") + << help_entry("--property id", "only check one specific property") + << help_entry( + "--trace", "give a counterexample trace for failed properties") + << help_entry( + "--stop-on-fail", + "stop analysis once a failed property is detected (implies --trace)") + << help_entry("--localize-faults", "localize faults (experimental)") + << HELP_JAVA_TRACE_VALIDATION + << "\n" "Platform options:\n" - HELP_CONFIG_PLATFORM - "\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" - HELP_SHOW_GOTO_FUNCTIONS - " --drop-unused-functions drop functions trivially unreachable\n" - " from main function\n" - HELP_SHOW_CLASS_HIERARCHY - "\n" + << help_entry("--show-parse-tree", "show parse tree") + << help_entry("--show-symbol-table", "show loaded symbol table") + << help_entry("--list-symbols", "list symbols with type information") + << HELP_SHOW_GOTO_FUNCTIONS + << help_entry( + "--drop-unused-functions", + "drop functions trivially unreachable from main function") + << 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(*) - HELP_REACHABILITY_SLICER - " --full-slice run full slicer (experimental)\n" // NOLINT(*) - "\n" + << help_entry("--no-assertions", "ignore user assertions") + << help_entry("--no-assumptions", "ignore user assumptions") + << help_entry("--mm MM", "memory consistency model for concurrent programs") + << HELP_REACHABILITY_SLICER + << help_entry("--full-slice", "run full slicer (experimental)") + << "\n" "Java Bytecode frontend options:\n" - JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP + << 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(*) + << help_entry( + "--java-threading", + "enable java multi-threading support (experimental)") + << help_entry( + "--java-unwind-enum-static", + "unwind loops in static initialization of enums") // 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" - "\n" + << help_entry( + "--symex-driven-lazy-loading", + "only load functions when first entered by symbolic execution. Note that " + "--show-symbol-table, --show-goto-functions/properties output will be " + "restricted to loaded methods in this case, and only output after the " + "symex phase.") + << "\n" "Semantic transformations:\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --nondet-static add nondeterministic initialization of variables with static lifetime\n" - "\n" + << help_entry( + "--nondet-static", + "add nondeterministic initialization of variables with static lifetime") + << "\n" "BMC options:\n" - HELP_BMC - "\n" + << HELP_BMC + << "\n" "Backend options:\n" - 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(*) - "\n" + << HELP_CONFIG_BACKEND + << HELP_SOLVER + << HELP_STRING_REFINEMENT + << help_entry( + "--arrays-uf-never", "never turn arrays into uninterpreted functions") + << help_entry( + "--arrays-uf-always", "always turn arrays into uninterpreted functions") + << "\n" "Other options:\n" - " --version show version and exit\n" - HELP_XML_INTERFACE - HELP_JSON_INTERFACE - HELP_VALIDATE - HELP_GOTO_TRACE - HELP_FLUSH - " --verbosity # verbosity level\n" - HELP_TIMESTAMP - "\n"; + << help_entry("--version", "show version and exit") + << HELP_XML_INTERFACE + << HELP_JSON_INTERFACE + << HELP_VALIDATE + << HELP_GOTO_TRACE + << HELP_FLUSH + << help_entry("--verbosity #", "verbosity level") + << HELP_TIMESTAMP + << "\n"; // clang-format on } diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index ea2c124f93c..8903dc68e5a 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -243,25 +243,25 @@ void jdiff_parse_optionst::help() " jdiff old new 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" - "\n" + << HELP_SHOW_GOTO_FUNCTIONS + << HELP_SHOW_PROPERTIES + << help_entry("--show-loops", "show the loops in the programs") + << help_entry("-u, --unified", "output unified diff") + << help_entry( + "--change-impact, --forward-impact, --backward-impact", + "output unified diff with forward&backward/forward/backward dependencies") + << help_entry("--compact-output", "output dependencies in compact mode") + << "\n" "Program instrumentation options:\n" - " --no-assertions ignore user assertions\n" - " --no-assumptions ignore user assumptions\n" - HELP_COVER + << help_entry("--no-assertions", "ignore user assertions") + << help_entry("--no-assumptions", "ignore user assumptions") + << HELP_COVER + << "\n" "Other options:\n" - " --version show version and exit\n" - " --json-ui use JSON-formatted output\n" - " --verbosity # verbosity level\n" - HELP_TIMESTAMP - "\n"; + << help_entry("--version", "show version and exit") + << help_entry("--json-ui", "use JSON-formatted output") + << help_entry("--verbosity #", "verbosity level") + << HELP_TIMESTAMP + << "\n"; // clang-format on } diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h index 8904cbba97d..d74e1c7b2de 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h @@ -80,26 +80,28 @@ "(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 + help_entry( \ + "--vsd-values [constants|intervals|set-of-constants]", "value tracking") \ + << help_entry( \ + "--vsd-structs [top-bottom|every-field]", \ + "struct field sensitive analysis") \ + << help_entry( \ + "--vsd-arrays [top-bottom|smash|up-to-n-elements|every-element]", \ + "array entry sensitive analysis") \ + << help_entry( \ + "--vsd-array-max-elements N", \ + "set the n in --vsd-arrays up-to-n-elements (defaults to 10 if not " \ + "given)") \ + << help_entry( \ + "--vsd-pointers [top-bottom|constants|value-set]", \ + "pointer sensitive analysis") \ + << help_entry("--vsd-unions [top-bottom]", "union sensitive analysis") \ + << help_entry("--vsd-data-dependencies", "track data dependencies") \ + << help_entry("--vsd-liveness", "track variable liveness") \ + << help_entry("--vsd-flow-insensitive", "disables flow sensitivity") #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..1f40207c92c 100644 --- a/src/ansi-c/ansi_c_language.h +++ b/src/ansi-c/ansi_c_language.h @@ -25,10 +25,14 @@ 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(*) */ + help_entry( \ + "--max-nondet-tree-depth N", \ + "limit size of nondet (e.g. input) object tree; at level N pointers are " \ + "set to null") \ + << help_entry( \ + "--min-null-tree-depth N", \ + "minimum level at which a pointer can first be NULL in a recursively " \ + "nondet initialized struct") \ // 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..38ad62e76e8 100644 --- a/src/ansi-c/goto_check_c.h +++ b/src/ansi-c/goto_check_c.h @@ -49,29 +49,46 @@ 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 \ + help_entry("--bounds-check", "enable array bounds checks") \ + << help_entry("--pointer-check", "enable pointer checks") \ + << help_entry("--memory-leak-check", "enable memory leak checks") \ + << help_entry("--memory-cleanup-check", "enable memory cleanup checks") \ + << help_entry("--div-by-zero-check", "enable division by zero checks") \ + << help_entry( \ + "--signed-overflow-check", \ + "enable signed arithmetic over- and underflow checks") \ + << help_entry( \ + "--unsigned-overflow-check", \ + "enable arithmetic over- and underflow checks") \ + << help_entry( \ + "--pointer-overflow-check", \ + "enable pointer arithmetic over- and underflow checks") \ + << help_entry( \ + "--conversion-check", \ + "check whether values can be represented after type cast") \ + << help_entry( \ + "--undefined-shift-check", "check shift greater than bit-width") \ + << help_entry("--float-overflow-check", "check floating-point for +/-Inf") \ + << help_entry("--nan-check", "check floating-point for NaN") \ + << help_entry( \ + "--enum-range-check", \ + "checks that all enum type expressions have values in the enum " \ + "range") \ + << help_entry( \ + "--pointer-primitive-check", \ + "checks that all pointers in pointer primitives are valid or null") \ + << help_entry( \ + "--retain-trivial-checks", "include checks that are trivially true") \ + << help_entry("--error-label label", "check that label is unreachable") \ + << help_entry( \ + "--no-built-in-assertions", "ignore assertions in built-in library") \ + << help_entry("--no-assertions", "ignore user assertions") \ + << help_entry("--no-assumptions", "ignore user assumptions") \ + << help_entry( \ + "--assert-to-assume", "convert user assertions to assumptions") +// 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..4fca13d4370 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -945,67 +945,81 @@ void cbmc_parse_optionst::help() " cbmc [options] file.c ... 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" - "\n" + << HELP_SHOW_PROPERTIES + << help_entry( + "--symex-coverage-report f", + "generate a Cobertura XML coverage report in f") + << help_entry("--property id", "only check one specific property") + << help_entry( + "--trace", + "give a counterexample trace for failed properties") + << help_entry( + "--stop-on-fail", + "stop analysis once a failed property is detected (implies --trace)") + << help_entry("--localize-faults", "localize faults (experimental)") + << "\n" "C/C++ frontend options:\n" - " --preprocess stop after preprocessing\n" - " --test-preprocessor stop after preprocessing, discard output\n" - HELP_CONFIG_C_CPP - HELP_ANSI_C_LANGUAGE - HELP_FUNCTIONS - "\n" + << help_entry("--preprocess", "stop after preprocessing") + << help_entry( + "--test-preprocessor", "stop after preprocessing, discard output") + << HELP_CONFIG_C_CPP + << HELP_ANSI_C_LANGUAGE + << HELP_FUNCTIONS + << "\n" "Platform options:\n" - HELP_CONFIG_PLATFORM - "\n" + << HELP_CONFIG_PLATFORM + << "\n" "Program representations:\n" - " --show-parse-tree show parse tree\n" - " --show-symbol-table 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(*) - "\n" + << help_entry("--show-parse-tree", "show parse tree") + << help_entry("--show-symbol-table", "show loaded symbol table") + << HELP_SHOW_GOTO_FUNCTIONS + << HELP_VALIDATE + << "\n" "Program instrumentation options:\n" - HELP_GOTO_CHECK - HELP_COVER - " --mm MM memory consistency model for concurrent programs (default: sc)\n" // NOLINT(*) - 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(*) - "\n" + << HELP_GOTO_CHECK + << HELP_COVER + << help_entry( + "--mm MM", + "memory consistency model for concurrent programs (default: sc)") + << HELP_CONFIG_LIBRARY + << HELP_REACHABILITY_SLICER + << help_entry("--full-slice", "run full slicer (experimental)") + << help_entry( + "--drop-unused-functions", + "drop functions trivially unreachable from main function") + << help_entry( + "--havoc-undefined-functions", + "for any function that has no body, assign non-deterministic values to " + "any parameters passed as non-const pointers and the return value") + << "\n" "Semantic transformations:\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --nondet-static add nondeterministic initialization of variables with static lifetime\n" - "\n" + << help_entry( + "--nondet-static", + "add nondeterministic initialization of variables with static lifetime") + << "\n" "BMC options:\n" - HELP_BMC - "\n" + << HELP_BMC + << "\n" "Backend options:\n" - 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" - "\n" + << HELP_CONFIG_BACKEND + << HELP_SOLVER + << HELP_STRING_REFINEMENT_CBMC + << help_entry( + "--arrays-uf-never", "never turn arrays into uninterpreted functions") + << help_entry( + "--arrays-uf-always", "always turn arrays into uninterpreted functions") + << help_entry( + "--show-array-constraints", + "show array theory constraints added during post processing. Requires " + "--json-ui.") + << "\n" "User-interface options:\n" - HELP_XML_INTERFACE - HELP_JSON_INTERFACE - HELP_GOTO_TRACE - HELP_FLUSH - " --verbosity # verbosity level\n" - HELP_TIMESTAMP - "\n"; + << HELP_XML_INTERFACE + << HELP_JSON_INTERFACE + << HELP_GOTO_TRACE + << HELP_FLUSH + << help_entry("--verbosity #", "verbosity level") + << HELP_TIMESTAMP + << "\n"; // clang-format on } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index b4535bc2366..459d85290b4 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -694,107 +694,121 @@ void goto_analyzer_parse_optionst::help() " goto-analyzer file.c ... 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" - "\n" + << help_entry("--show", "display the abstract states on the goto program") + << help_entry( + "--show-on-source", "display the abstract states on the source") + << help_entry("--verify", "use the abstract domains to check assertions") + << help_entry( + "--simplify file_name", + "use the abstract domains to simplify the program") + << help_entry( + "--no-simplify-slicing", + "do not remove instructions from which no property can be reached (use " + "with --simplify)") + << help_entry("--unreachable-instructions", "list dead code") + << help_entry( + "--unreachable-functions", + "list functions unreachable from the entry point") + << help_entry( + "--reachable-functions", "list functions reachable from the entry point") + << "\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" - "\n" + << help_entry( + "--legacy-ait", "recursion for function and one domain per location") + << help_entry( + "--recursive-interprocedural", + "use recursion to handle interprocedural reasoning") + << help_entry( + "--three-way-merge", + "use VSD's three-way merge on return from function call") + << help_entry( + "--legacy-concurrent", + "legacy-ait with an extended fixed-point for concurrency") + << help_entry( + "--location-sensitive", "use location-sensitive abstract interpreter") + << "\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" - "\n" + << help_entry( + "--ahistorical", "the most basic history, tracks locations only") + << help_entry( + "--call-stack n", + "track the calling location stack for each function limiting to at most " + "n recursive loops, 0 to disable") + << help_entry( + "--loop-unwind n", "track the number of loop iterations within a " + "function limited to n histories per location, 0 is unlimited") + << help_entry( + "--branching n", + "track the forwards jumps (if, switch, etc.) within a function limited " + "to n histories per location, 0 is unlimited") + << help_entry( + "--loop-unwind-and-branching n", + "track all local control flow limited to n histories per location, 0 is " + "unlimited") + << "\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(*) - "\n" + << help_entry("--constants", "a constant for each variable if possible") + << help_entry("--intervals", "an interval for each variable") + << help_entry("--non-null", "tracks which pointers are non-null") + << help_entry( + "--dependence-graph", + "data and control dependencies between instructions") + << help_entry( + "--vsd, --variable-sensitivity", "a configurable non-relational domain") + << help_entry( + "--dependence-graph-vs", "dependencies between instructions using VSD") + << "\n" "Variable sensitivity domain (VSD) options:\n" - HELP_VSD - "\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" - "\n" + << help_entry( + "--one-domain-per-location", "stores a domain for each location reached") + << help_entry( + "--one-domain-per-history", + "stores a domain for each history object created") + << "\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" - "\n" + << help_entry( + "--text file_name", "output results in plain text to given file") + << help_entry( + "--json file_name", "output results in JSON format to given file") + << help_entry( + "--xml file_name", "output results in XML format to given file") + << help_entry( + "--dot file_name", "output results in DOT format to given file") + << "\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" - "\n" + << help_entry( + "--taint file_name", "perform taint analysis using rules in given file") + << help_entry("--show-taint", "print taint analysis results on stdout") + << help_entry( + "--show-local-may-alias", "perform procedure-local may alias analysis") + << "\n" "C/C++ frontend options:\n" - HELP_CONFIG_C_CPP - HELP_FUNCTIONS - "\n" + << HELP_CONFIG_C_CPP + << HELP_FUNCTIONS + << "\n" "Platform options:\n" - HELP_CONFIG_PLATFORM - "\n" + << HELP_CONFIG_PLATFORM + << "\n" "Program representations:\n" - " --show-parse-tree show parse tree\n" - " --show-symbol-table show loaded symbol table\n" - HELP_SHOW_GOTO_FUNCTIONS - HELP_SHOW_PROPERTIES - "\n" + << help_entry("--show-parse-tree", "show parse tree") + << help_entry("--show-symbol-table", "show loaded symbol table") + << HELP_SHOW_GOTO_FUNCTIONS + << HELP_SHOW_PROPERTIES + << "\n" "Program instrumentation options:\n" - " --property id enable selected properties only\n" - HELP_GOTO_CHECK - HELP_CONFIG_LIBRARY - "\n" + << help_entry("--property id", "enable selected properties only") + << HELP_GOTO_CHECK + << HELP_CONFIG_LIBRARY + << "\n" "Other options:\n" - HELP_VALIDATE - " --version show version and exit\n" - HELP_FLUSH - " --verbosity # verbosity level\n" - HELP_TIMESTAMP - "\n"; + << HELP_VALIDATE + << help_entry("--version", "show version and exit") + << HELP_FLUSH + << help_entry("--verbosity #", "verbosity level") + << HELP_TIMESTAMP + << "\n"; // clang-format on } diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index ab4ae30a3c6..20c86903941 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -169,83 +169,92 @@ 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 \ + help_entry("--paths [strategy]", "explore paths one at a time") \ + << help_entry( \ + "--show-symex-strategies", "list strategies for use with --paths") \ + << help_entry( \ + "--show-goto-symex-steps", \ + "show which steps symex travels, includes diagnostic information") \ + << help_entry( \ + "--show-points-to-sets", \ + "show points-to sets for pointer dereference. Requires --json-ui.") \ + << help_entry("--program-only", "only show program expression") \ + << help_entry("--show-byte-ops", "show all byte extracts and updates") \ + << help_entry("--depth nr", "limit search depth") \ + << help_entry( \ + "--max-field-sensitivity-array-size M", \ + "maximum size M of arrays for which field sensitivity will be " \ + "applied to array, the default is 64") \ + << help_entry( \ + "--no-array-field-sensitivity", \ + "deactivate field sensitivity for arrays, this is equivalent to " \ + "setting the maximum field sensitivity size for arrays to 0") \ + << HELP_UNWINDSET \ + << help_entry( \ + "--incremental-loop L", \ + "check properties after each unwinding of loop L (use --show-loops " \ + "to get the loop IDs)") \ + << help_entry( \ + "--unwind-min nr", \ + "start incremental-loop after nr 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 min-unwind 1 " \ + "or 0 all properties are checked.") \ + << help_entry( \ + "--unwind-max nr", "stop incremental-loop after nr unwindings") \ + << help_entry( \ + "--ignore-properties-before-unwind-min", \ + "do not check properties before unwind-min when using " \ + "incremental-loop") \ + << help_entry("--show-vcc", "show the verification conditions") \ + << help_entry( \ + "--slice-formula", "remove assignments unrelated to property") \ + << help_entry( \ + "--unwinding-assertions", \ + "generate unwinding assertions (cannot be used with --cover)") \ + << help_entry("--partial-loops", "permit paths with partial loops") \ + << help_entry( \ + "--no-self-loops-to-assumptions", \ + "do not simplify while(1){} to assume(0)") \ + << help_entry( \ + "--symex-complexity-limit N", \ + "how complex (N) a path can become before symex abandons it. " \ + "Currently uses guard size to calculate complexity.") \ + << help_entry( \ + "--symex-complexity-failed-child-loops-limit N", \ + "how many child branches (N) in an iteration are allowed to fail " \ + "due to complexity violations before the loop gets blacklisted") \ + << help_entry( \ + "--graphml-witness_filename", \ + "write the witness in GraphML format to filename") \ + << help_entry( \ + "--symex-cache-dereferences", \ + "enable caching of repeated dereferences") #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..f35e28183fe 100644 --- a/src/goto-checker/solver_factory.h +++ b/src/goto-checker/solver_factory.h @@ -116,36 +116,40 @@ 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" + help_entry("--sat-solver solver", "use specified SAT solver") \ + << help_entry( \ + "--external-sat-solver cmd", "command to invoke SAT solver process") \ + << help_entry( \ + "--no-sat-preprocessor", "disable the SAT solver's simplifier") \ + << help_entry("--dimacs", "generate CNF in DIMACS format") \ + << help_entry( \ + "--beautify", "beautify the counterexample (greedy heuristic)") \ + << help_entry("--smt1", "use default SMT1 solver (obsolete)") \ + << help_entry("--smt2", "use default SMT2 solver (Z3)") \ + << help_entry("--bitwuzla", "use Bitwuzla") \ + << help_entry("--boolector", "use Boolector") \ + << help_entry("--cprover-smt2", "use CPROVER SMT2 solver") \ + << help_entry("--cvc3", "use CVC3") << help_entry("--cvc4", "use CVC4") \ + << help_entry("--mathsat", "use MathSAT") \ + << help_entry("--yices", "use Yices") << help_entry("--z3", "use Z3") \ + << help_entry("--fpa", "use theory of floating-point arithmetic") \ + << help_entry("--refine", "use refinement procedure (experimental)") \ + << help_entry("--refine-arrays", "use refinement for arrays only") \ + << help_entry( \ + "--refine-arithmetic", "refinement of arithmetic expressions only") \ + << help_entry( \ + "--max-node-refinement", \ + "maximum refinement iterations for arithmetic expressions") \ + << help_entry( \ + "--incremental-smt2-solver cmd", \ + "command to invoke external SMT solver for incremental solving " \ + "(experimental)") \ + << help_entry("--outfile filename", "output formula to given file") \ + << help_entry( \ + "--dump-smt-formula filename", \ + "output smt incremental formula to the given file") \ + << help_entry( \ + "--write-solver-stats-to json-file", \ + "collect the solver query complexity") #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..b2429019c16 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -229,26 +229,25 @@ void goto_diff_parse_optionst::help() " goto_diff old new goto binaries 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" - "\n" + << HELP_SHOW_GOTO_FUNCTIONS + << HELP_SHOW_PROPERTIES + << help_entry("--show-loops", "show the loops in the programs") + << help_entry("-u, --unified", "output unified diff") + << help_entry( + "--change-impact, --forward-impact, --backward-impact", + "output unified diff with forward&backward/forward/backward dependencies") + << help_entry("--compact-output", "output dependencies in compact mode") + << "\n" "Program instrumentation options:\n" - HELP_GOTO_CHECK - HELP_COVER - "\n" + << HELP_GOTO_CHECK + << HELP_COVER + << "\n" "Other options:\n" - " --version show version and exit\n" - " --json-ui use JSON-formatted output\n" - HELP_FLUSH - " --verbosity # verbosity level\n" - HELP_TIMESTAMP - "\n"; + << help_entry("--version", "show version and exit") + << help_entry("--json-ui", "use JSON-formatted output") + << HELP_FLUSH + << help_entry("--verbosity #", "verbosity level") + << HELP_TIMESTAMP + << "\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..97f32a97d74 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 + help_entry( \ + "--" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT " N", \ + "minimum level at which a pointer can first be NULL in a recursively " \ + "nondet initialized struct") \ + << help_entry( \ + "--" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT " N", \ + "limit size of nondet (e.g. input) object tree; at level N pointers " \ + "are set to null") \ + << help_entry( \ + "--" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT " N", \ + "minimum size of dynamically created arrays (default: 1)") \ + << help_entry( \ + "--" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT " N", \ + "maximum size of dynamically created arrays (default: 2)") \ + << help_entry( \ + "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \ + " ", \ + "name of the function(s) pointer parameters that can be NULL " \ + "pointing") \ + << help_entry( \ + "--" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT " ", \ + "path to the member to be havoced") #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..2c0ee4a1c6c 100644 --- a/src/goto-harness/function_harness_generator_options.h +++ b/src/goto-harness/function_harness_generator_options.h @@ -24,48 +24,51 @@ 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 (--harness-type call-function):\n" \ + << help_entry( \ + "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT " ", \ + "the function the harness should call") \ + << help_entry( \ + "--" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT, \ + "set global variables to non-deterministic values in harness") \ + << COMMON_HARNESS_GENERATOR_HELP \ + << help_entry( \ + "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT " p", \ + "treat the function parameter with the name `p' as an array") \ + << help_entry( \ + "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT \ + " p,q,r[;s,t]", \ + "treat the function parameters `q,r' equal to parameter `p'; `s` to " \ + "`t` and so on") \ + << help_entry( \ + "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT, \ + "function parameters equality is non-deterministic") \ + << help_entry( \ + "--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \ + " array_name:size_name", \ + "set the parameter to the size of the array " \ + " (implies " \ + "-- " FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \ + " )") \ + << help_entry( \ + "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING " p", \ + "treat the function parameter with the name `p' as a string of " \ + "characters") #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..21fe16265ee 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -192,11 +192,14 @@ void goto_harness_parse_optionst::help() "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" + << help_entry( + "--harness-function-name ", + "the name of the harness function to " + "generate") + << help_entry( + "--harness-type ", "one of the harness types listed below") + << '\n' + << FUNCTION_HARNESS_GENERATOR_HELP << '\n' << MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP << '\n'; } diff --git a/src/goto-harness/memory_snapshot_harness_generator_options.h b/src/goto-harness/memory_snapshot_harness_generator_options.h index 8f95bcdb7c7..409a609a108 100644 --- a/src/goto-harness/memory_snapshot_harness_generator_options.h +++ b/src/goto-harness/memory_snapshot_harness_generator_options.h @@ -18,46 +18,44 @@ 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 + " initialize-with-memory-snapshot):\n" \ + << help_entry( \ + "--" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT " ", \ + "initialize memory from JSON memory snapshot") \ + << help_entry( \ + "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT " ]>", \ + "use given function and location number as entry point") \ + << help_entry( \ + "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT " >", \ + "use given file name and line number as entry point") \ + << help_entry( \ + "--" MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT " vars", \ + "initialize variables from `vars' to non-deterministic values") \ + << COMMON_HARNESS_GENERATOR_HELP \ + << help_entry( \ + "--" MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT " p", \ + "treat the global pointer with the name `p' as an array") \ + << help_entry( \ + "--" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT \ + " array_name:size_name", \ + "set the parameter to the size of the array " \ + " (implies " \ + "-- " MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT \ + " )") #endif // CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS_H diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index ce0c061c6f5..3f1206f2c69 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -29,32 +29,32 @@ 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" + help_entry( \ + "--apply-loop-contracts", "check and use loop contracts when provided") #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" + help_entry("--loop-contracts-no-unwind", "do not unwind transformed loops") #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" + help_entry( \ + "loop-contracts-file ", \ + "parse and annotate loop contracts from files") #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" + help_entry( \ + "--replace-call-with-contract [/contract]", \ + "replace calls to function with contract") #define FLAG_ENFORCE_CONTRACT "enforce-contract" #define HELP_ENFORCE_CONTRACT \ - " --enforce-contract [/contract]" \ - " wrap function with an assertion of contract\n" -// clang-format on + help_entry( \ + "--enforce-contract [/contract]", \ + "wrap function with an assertion of contract") class local_may_aliast; diff --git a/src/goto-instrument/count_eloc.h b/src/goto-instrument/count_eloc.h index eb719d08a55..1edf8abe057 100644 --- a/src/goto-instrument/count_eloc.h +++ b/src/goto-instrument/count_eloc.h @@ -28,12 +28,14 @@ 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" + help_entry("--count-eloc", "count effective lines of code") \ + << help_entry( \ + "--list-eloc", "list full path names of lines containing code") \ + << help_entry( \ + "--print-global-state-size", \ + "count the total number of bits of global objects") \ + << help_entry( \ + "--print-path-lengths", \ + "print statistics about control-flow graph paths") #endif // CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 84ec1873095..f8d9c8c86fa 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -31,19 +31,18 @@ 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" + help_entry( \ + "--cover CC", \ + "create test-suite with coverage criterion CC, where CC is one of " \ + "assertion[s], assume[s], branch[es], condition[s], cover, decision[s], " \ + "location[s], or mcdc") \ + << help_entry( \ + "--cover-failed-assertions", \ + "do not stop coverage checking at failed assertions (this is the " \ + "default for --cover assertions)") \ + << help_entry( \ + "--show-test-suite", \ + "print test suite for coverage criterion (requires --cover)") enum class coverage_criteriont { diff --git a/src/goto-instrument/document_properties.h b/src/goto-instrument/document_properties.h index f48f9440f00..50154a3901d 100644 --- a/src/goto-instrument/document_properties.h +++ b/src/goto-instrument/document_properties.h @@ -28,11 +28,11 @@ 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 + help_entry( \ + "--document-properties-html", "generate HTML property documentation") \ + << help_entry( \ + "--document-properties-latex", \ + "generate Latex property documentation") #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..56343f4c48e 100644 --- a/src/goto-instrument/dump_c.h +++ b/src/goto-instrument/dump_c.h @@ -48,15 +48,14 @@ 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 + help_entry("--dump-c", "generate C source") \ + << help_entry( \ + "--dump-c-type-header m", "generate a C header for types local in m") \ + << help_entry("--dump-cpp", "generate C++ source") \ + << help_entry( \ + "--no-system-headers", "generate C source expanding libc includes") \ + << help_entry("--use-all-headers", "generate C source with all includes") \ + << help_entry("--harness", "include input generator in output") #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..485c50614ee 100644 --- a/src/goto-instrument/generate_function_bodies.h +++ b/src/goto-instrument/generate_function_bodies.h @@ -84,29 +84,27 @@ 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