diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index df91f7be78c..24dab815b90 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1748,43 +1748,62 @@ void goto_instrument_parse_optionst::help() "Usage: Purpose:\n" "\n" " goto-instrument [-?] [-h] [--help] show help\n" - " goto-instrument in out perform instrumentation\n" - "\n" - "Main options:\n" - HELP_DOCUMENT_PROPERTIES - " --dot generate CFG graph in DOT format\n" - " --interpreter do concrete execution\n" + " goto-instrument --version show version and exit\n" + " goto-instrument [options] in [out] perform analysis or instrumentation\n" "\n" "Dump Source:\n" HELP_DUMP_C + " --horn print program as constrained horn clauses\n" "\n" "Diagnosis:\n" HELP_SHOW_PROPERTIES + HELP_DOCUMENT_PROPERTIES " --show-symbol-table show loaded symbol table\n" " --list-symbols list symbols with type information\n" HELP_SHOW_GOTO_FUNCTIONS HELP_GOTO_PROGRAM_STATS - " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) + " --show-locations show all source locations\n" + " --dot generate CFG graph in DOT format\n" " --print-internal-representation\n" // NOLINTNEXTLINE(*) " show verbose internal representation of the program\n" " --list-undefined-functions list functions without body\n" - " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*) - " --show-natural-loops show natural loop heads\n" // NOLINTNEXTLINE(whitespace/line_length) " --list-calls-args list all function calls with their arguments\n" " --call-graph show graph of function calls\n" // NOLINTNEXTLINE(whitespace/line_length) " --reachable-call-graph show graph of function calls potentially reachable from main function\n" HELP_SHOW_CLASS_HIERARCHY + HELP_VALIDATE + // NOLINTNEXTLINE(whitespace/line_length) + " --validate-goto-binary check the well-formedness of the passed in goto\n" + " binary and then exit\n" + " --interpreter do concrete execution\n" + "\n" + "Data-flow analyses:\n" + " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*) // NOLINTNEXTLINE(whitespace/line_length) " --show-threaded show instructions that may be executed by more than one thread\n" " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*) " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*) " *and* used as a dereference operand\n" // NOLINT(*) - HELP_VALIDATE - // NOLINTNEXTLINE(whitespace/line_length) - " --validate-goto-binary check the well-formedness of the passed in goto\n" - " binary and then exit\n" + " --show-value-sets show points-to information (using value sets)\n" // NOLINT(*) + " --show-global-may-alias show may-alias information over globals\n" + " --show-local-bitvector-analysis\n" + " show procedure-local pointer analysis\n" + " --escape-analysis perform escape analysis\n" + " --show-escape-analysis show results of escape analysis\n" + " --custom-bitvector-analysis perform configurable bitvector analysis\n" + " --show-custom-bitvector-analysis\n" + " show results of configurable bitvector analysis\n" // NOLINT(*) + " --interval-analysis perform interval analysis\n" + " --show-intervals show results of interval analysis\n" + " --show-uninitialized show maybe-uninitialized variables\n" + " --show-points-to show points-to information\n" + " --show-rw-set show read-write sets\n" + " --show-call-sequences show function call sequences\n" + " --show-reaching-definitions show reaching definitions\n" + " --show-dependence-graph show program-dependence graph\n" + " --show-sese-regions show single-entry-single-exit regions\n" "\n" "Safety checks:\n" " --no-assertions ignore user assertions\n" @@ -1795,33 +1814,66 @@ void goto_instrument_parse_optionst::help() "\n" "Semantic transformations:\n" << HELP_NONDET_VOLATILE << - HELP_UNWINDSET - " --unwindset-file read unwindset from file\n" - " --partial-loops permit paths with partial loops\n" - " --unwinding-assertions generate unwinding assertions\n" - " --continue-as-loops add loop for remaining iterations after unwound part\n" // NOLINT(*) " --isr instruments an interrupt service routine\n" " --mmio instruments memory-mapped I/O\n" " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*) " --nondet-static-exclude e same as nondet-static except for the variable e\n" //NOLINT(*) " (use multiple times if required)\n" " --check-invariant function instruments invariant checking function\n" - HELP_REMOVE_POINTERS + " --function-enter , --function-exit , --branch \n" + " instruments a call to at the beginning,\n" // NOLINT(*) + " the exit, or a branch point, respectively\n" " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*) + " --check-call-sequence instruments checks to assert that all call\n" + " sequences match \n" " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length) " convert each call to an undefined function to assume(false)\n" HELP_INSERT_FINAL_ASSERT_FALSE HELP_REPLACE_FUNCTION_BODY + HELP_RESTRICT_FUNCTION_POINTER + HELP_REMOVE_CALLS_NO_BODY + " --add-library add models of C library functions\n" + HELP_CONFIG_LIBRARY + " --model-argc-argv model up to command line arguments\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --remove-function-body remove the implementation of function (may be repeated)\n" + HELP_REPLACE_CALLS HELP_ANSI_C_LANGUAGE "\n" - "Loop transformations:\n" + "Semantics-preserving transformations:\n" + " --ensure-one-backedge-per-target\n" + " transform loop bodies such that there is a\n" + " single edge back to the loop head\n" + " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) + HELP_REMOVE_POINTERS + " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*) + " --inline perform full inlining\n" + " --partial-inline perform partial inlining\n" + " --function-inline transitively inline all calls makes\n" // NOLINT(*) + " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*) + " --log log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*) + " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*) + HELP_REMOVE_CONST_FUNCTION_POINTERS + " --value-set-fi-fp-removal build flow-insensitive value set and replace function pointers by a case statement\n" // NOLINT(*) + " over the possible assignments. If the set of possible assignments is empty the function pointer\n" // NOLINT(*) + " is removed using the standard remove-function-pointers pass. \n" // NOLINT(*) + "\n" + "Loop information and transformations:\n" + HELP_UNWINDSET + " --unwindset-file read unwindset from file\n" + " --partial-loops permit paths with partial loops\n" + " --unwinding-assertions generate unwinding assertions\n" + " --continue-as-loops add loop for remaining iterations after unwound part\n" // NOLINT(*) " --k-induction check loops with k-induction\n" " --step-case k-induction: do step-case\n" " --base-case k-induction: do base-case\n" " --havoc-loops over-approximate all loops\n" " --accelerate add loop accelerators\n" + " --z3 use Z3 when computing loop accelerators\n" " --skip-loops add gotos to skip selected loops during execution\n" // NOLINT(*) + " --show-lexical-loops show single-entry-single-back-edge loops\n" + " --show-natural-loops show natural loop heads\n" "\n" "Memory model instrumentations:\n" HELP_WMM_FULL @@ -1838,43 +1890,22 @@ void goto_instrument_parse_optionst::help() " of the functions on the shortest path\n" " --aggressive-slice-preserve-function \n" " force the aggressive slicer to preserve function \n" // NOLINT(*) - " --aggressive-slice-preserve-function containing \n" + " --aggressive-slice-preserve-functions-containing \n" " force the aggressive slicer to preserve all functions with names containing \n" // NOLINT(*) - "--aggressive-slice-preserve-all-direct-paths \n" + " --aggressive-slice-preserve-all-direct-paths \n" " force aggressive slicer to preserve all direct paths\n" // NOLINT(*) "\n" - "Further transformations:\n" - " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*) - " --inline perform full inlining\n" - " --partial-inline perform partial inlining\n" - " --function-inline transitively inline all calls makes\n" // NOLINT(*) - " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*) - " --log log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*) - " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*) - " --value-set-fi-fp-removal build flow-insensitive value set and replace function pointers by a case statement\n" // NOLINT(*) - " over the possible assignments. If the set of possible assignments is empty the function pointer\n" // NOLINT(*) - " is removed using the standard remove-function-pointers pass. \n" // NOLINT(*) - HELP_RESTRICT_FUNCTION_POINTER - HELP_REMOVE_CALLS_NO_BODY - HELP_REMOVE_CONST_FUNCTION_POINTERS - " --add-library add models of C library functions\n" - HELP_CONFIG_LIBRARY - " --model-argc-argv model up to command line arguments\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --remove-function-body remove the implementation of function (may be repeated)\n" - HELP_REPLACE_CALLS - "\n" "Code contracts:\n" HELP_LOOP_CONTRACTS HELP_REPLACE_CALL HELP_ENFORCE_CONTRACT "\n" - "Other options:\n" - " --version show version and exit\n" + "User-interface options:\n" HELP_FLUSH " --xml output files in XML where supported\n" " --xml-ui use XML-formatted output\n" " --json-ui use JSON-formatted output\n" + " --verbosity # verbosity level\n" HELP_TIMESTAMP "\n"; // clang-format on diff --git a/src/goto-instrument/wmm/weak_memory.h b/src/goto-instrument/wmm/weak_memory.h index bbb7bb596ad..311aadfa5b9 100644 --- a/src/goto-instrument/wmm/weak_memory.h +++ b/src/goto-instrument/wmm/weak_memory.h @@ -97,9 +97,21 @@ void introduce_temporaries( " --one-event-per-cycle only instruments one event per cycle\n" \ " --minimum-interference instruments an optimal number of events\n" \ " --my-events only instruments events whose ids appear in inst.evt\n" /* NOLINT(whitespace/line_length) */ \ + " --read-first|--write-first only instrument cycles where a read or \n" \ + " write occurs as first event, respectively\n" \ + " --max-var N limit cycles to N variables read/written\n" \ + " --max-po-trans N limit cycles to N program-order edges\n" \ + " --ignore-arrays instrument arrays as a single object\n" \ + " --cav11 always instrument shared variables, even\n" \ + " when they are not part of any cycle\n" \ + " --force-loop-duplication|--no-loop-duplication\n" \ + " optional program transformation to\n" \ + " construct cycles in program loops\n" \ " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" /* NOLINT(whitespace/line_length) */ \ " --no-dependencies no dependency analysis\n" \ " --no-po-rendering no representation of the threads in the dot\n"\ + " --hide-internals do not include thread-internal (Rfi)\n" \ + " events in dot output\n" \ " --render-cluster-file clusterises the dot by files\n" \ " --render-cluster-function clusterises the dot by functions\n" diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h index 13c44d74c7e..afb6ddbfe0b 100644 --- a/src/goto-programs/restrict_function_pointers.h +++ b/src/goto-programs/restrict_function_pointers.h @@ -58,7 +58,13 @@ class optionst; " --" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \ " \n" \ " add function pointer restrictions from " \ - "file\n" + "file\n" \ + " --" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT \ + " /target[targets]*>\n" \ + " restrict a function pointer where " \ + " \n" \ + " is the unmangled name, before labelling " \ + "function pointers\n" void parse_function_pointer_restriction_options_from_cmdline( const cmdlinet &cmdline, diff --git a/src/util/config.h b/src/util/config.h index 99549013784..aac573ff2e0 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -63,6 +63,7 @@ class symbol_tablet; " --malloc-may-fail allow malloc calls to return a null pointer\n" \ " --malloc-fail-assert set malloc failure mode to assert-then-assume\n"\ " --malloc-fail-null set malloc failure mode to return null\n" \ +" --string-abstraction track C string lengths and zero-termination\n" \ #define OPT_CONFIG_JAVA \