Merge pull request #6930 from tautschnig/github/jbmc-help

Complete JBMC help output

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -78,6 +78,8 @@ Author: Daniel Kroening, [email protected]
   " --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(*) */ \

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -944,8 +944,12 @@ void jbmc_parse_optionst::help()
     " --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"
+    "Platform options:\n"
+    HELP_CONFIG_PLATFORM
+    "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show loaded symbol table\n"
@@ -960,6 +964,7 @@ void jbmc_parse_optionst::help()
     " --no-assumptions             ignore user assumptions\n"
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
     HELP_REACHABILITY_SLICER
+    HELP_REACHABILITY_SLICER_FB
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
     "\n"
     "Java Bytecode frontend options:\n"