Merge pull request #5662 from tautschnig/stop-on-fail-help-msg

Help output: document that stop-on-fail implies trace

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -1070,8 +1070,9 @@ void jbmc_parse_optionst::help()
     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"
-    " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
     " --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"
     HELP_JAVA_TRACE_VALIDATION
     "\n"
     "Program representations:\n"

src/cbmc/README.md

@@ -48,7 +48,8 @@ formula using two different possible procedures:
 
 1. When `--stop-on-fail` is passed on the command-line, the formula is solved
    once to find any violated assertion. This is implemented directly in
-   class `bmct`.
+   class `bmct`. If the formula is satisfiable, a counter-example trace is
+   generated.
 2. When `--stop-on-fail` is not passed, BMC is run in "all-properties" mode.
    This categorises the assertions into groups that represent the same property,
    and the solver is run repeatedly to try to satisfy each property at least

src/cbmc/cbmc_parse_options.cpp

@@ -1064,8 +1064,9 @@ void cbmc_parse_optionst::help()
     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"
-    " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
     " --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"
     "\n"
     "C/C++ frontend options:\n"
     " -I path                      set include path (C/C++)\n"