Merge pull request diffblue#413 from diffblue/cleanup/sec_driver_options

Cleanup sec driver options

Author: NathanJPhillips

src/driver/sec_driver_parse_options.cpp

@@ -72,7 +72,7 @@
 sec_driver_parse_optionst::sec_driver_parse_optionst(int argc, const char **argv):
   parse_options_baset(SEC_DRIVER_OPTIONS, argc, argv),
   language_uit(cmdline, ui_message_handler),
-  ui_message_handler(cmdline, "Diffblue Security Analyzer " CBMC_VERSION)
+  ui_message_handler(cmdline, "Diffblue Security Analyzer " SEC_DRIVER_VERSION)
 {
 }
 
@@ -134,11 +134,14 @@ static irep_idt get_cprover_start_main_callee(const goto_modelt &goto_model)
 /// invoke main modules
 int sec_driver_parse_optionst::doit()
 {
+  // Print a banner
+  status() << "Diffblue Security Analyzer version " SEC_DRIVER_VERSION " "
+           << sizeof(void *) * 8 << "-bit "
+           << config.this_architecture() << " "
+           << config.this_operating_system() << eom;
+
   if(cmdline.isset("version"))
-  {
-    std::cout << CBMC_VERSION << std::endl;
     return CPROVER_EXIT_SUCCESS;
-  }
 
   //
   // command line options
@@ -156,14 +159,6 @@ int sec_driver_parse_optionst::doit()
   get_command_line_options(options);
   eval_verbosity();
 
-  //
-  // Print a banner
-  //
-  status() << "Diffblue Security Analyzer version " CBMC_VERSION " "
-           << sizeof(void *)*8 << "-bit "
-           << config.this_architecture() << " "
-           << config.this_operating_system() << eom;
-
   register_languages();
   register_evs_pretty_printer();
 
@@ -536,78 +531,49 @@ bool sec_driver_parse_optionst::process_goto_functions(
 /// display command line help
 void sec_driver_parse_optionst::help()
 {
-  std::cout <<
-    "\n"
-    "* * Diffblue Security Analyzer " CBMC_VERSION " - Copyright (C) 2016 ";
-
-  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
-
-  std::cout << " * *\n";
-
-  std::cout <<
-    "* *                Daniel Kroening, Diffblue                * *\n"
-    "* *                 [email protected]                   * *\n"
-    "\n"
+  std::cout
+    << "\n  Diffblue Security Analyzer " SEC_DRIVER_VERSION " ("
+    << (sizeof(void *) * 8) << "-bit version)\n"
+    "  Copyright © 2016–2018\n\n"
     "Usage:                       Purpose:\n"
     "\n"
-    " sec-driver [-h] [--help]  show help\n"
-    " sec-driver file.c ...     source file names\n"
+    " security-analyzer [-h] [--help]  show help\n"
+    " security-analyzer file.class ... source file names\n"
     "\n"
     "Analyses:\n"
     "\n"
-    " --security-scanner file_name perform taint analysis using configuration "
-    "                              in given JSON file\n"
-    " --unreachable-instructions   list dead code\n"
-    " --intervals                  interval analysis\n"
-    " --non-null                   non-null analysis\n"
+    " --security-scanner config.json   perform taint analysis using configuration\n"
+    "                                  in given JSON file\n"
+    " --local-value-set-analysis       perform local value set analysis only\n"
+    " --unreachable-instructions       list dead code\n"
+    " --intervals                      interval analysis\n"
+    " --non-null                       non-null analysis\n"
     "\n"
     "Analysis options:\n"
-    " --json file_name             output results in JSON format to given file\n"
-    " --xml file_name              output results in XML format to given file\n"
-    " --function                   set main function name\n"
-    "\n"
-    "C/C++ frontend options:\n"
-    " -I path                      set include path (C/C++)\n"
-    " -D macro                     define preprocessor macro (C/C++)\n"
-    " --arch X                     set architecture (default: "
-                                   << configt::this_architecture() << ")\n"
-    " --os                         set operating system (default: "
-                                   << configt::this_operating_system() << ")\n"
-    " --c89/99/11                  set C language standard (default: "
-                                   << (configt::ansi_ct::default_c_standard()==
-                                       configt::ansi_ct::c_standardt::C89?"c89":
-                                       configt::ansi_ct::default_c_standard()==
-                                       configt::ansi_ct::c_standardt::C99?"c99":
-                                       configt::ansi_ct::default_c_standard()==
-                                       configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n"
-    " --cpp98/03/11                set C++ language standard (default: "
-                                   << (configt::cppt::default_cpp_standard()==
-                                       configt::cppt::cpp_standardt::CPP98?"cpp98":
-                                       configt::cppt::default_cpp_standard()==
-                                       configt::cppt::cpp_standardt::CPP03?"cpp03":
-                                       configt::cppt::default_cpp_standard()==
-                                       configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n"
-    #ifdef _WIN32
-    " --gcc                        use GCC as preprocessor\n"
-    #endif
-    " --no-library                 disable built-in abstract C library\n"
+    " --json file_name                 output results in JSON format to given file\n"
+    " --xml file_name                  output results in XML format to given file\n"
+    " --function                       set main function name\n"
+    " --lvsa-function                  set function to analyze with LVSA\n"
+    " --lvsa-summary-directory         directory to store LVSA summaries\n"
     "\n"
     "Java Bytecode frontend options:\n"
-    " --classpath dir/jar          set the classpath\n"
-    " --main-class class-name      set the name of the main class\n"
+    " --classpath dir/jar              set the classpath\n"
+    " --main-class class-name          set the name of the main class\n"
     JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
     "\n"
     "Program representations:\n"
-    " --show-parse-tree            show parse tree\n"
-    " --show-symbol-table          show symbol table\n"
-    " --show-goto-functions        show goto program\n"
-    " --show-properties            show the properties, but don't run analysis\n"
-    " --dump-html-program          dump goto program in HTML format into\n"
-    "                              a directory. Pass a non existing directory\n"
-    "                              path-name with this option. The directory\n"
-    "                              will be created with the dumped program.\n"
+    " --show-parse-tree                show parse tree\n"
+    " --show-symbol-table              show symbol table\n"
+    " --show-goto-functions            show goto program\n"
+    " --show-properties                show the properties, but don't run analysis\n"
+    " --show-value-sets                show value set for entry point\n"
+    " --show-value-sets-all            show all value sets\n"
+    " --dump-html-program              dump goto program in HTML format into\n"
+    "                                  a directory. Pass a non existing directory\n"
+    "                                  path-name with this option. The directory\n"
+    "                                  will be created with the dumped program.\n"
     "\n"
     "Other options:\n"
-    " --version                    show version and exit\n"
+    " --version                        show version and exit\n"
     "\n";
 }

src/driver/sec_driver_parse_options.h

@@ -20,9 +20,10 @@
 class bmct;
 class optionst;
 
+#define SEC_DRIVER_VERSION "0.1"
+
 #define SEC_DRIVER_OPTIONS \
   "(function):" \
-  "D:I:(std89)(std99)(std11)" \
   "(classpath):(cp):(main-class):" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
@@ -31,7 +32,6 @@ class optionst;
   "(dump-html-program):" \
   "(show-properties)(show-reachable-properties)(property):" \
   "(verbosity):(version)" \
-  "(gcc)(arch):" \
   "(taint):(show-taint)" \
   "(taint-use-summaries):" \
   "(show-local-may-alias)" \