Merge pull request diffblue#232 from diffblue/feature/option_dump-html-program

SEC-41 : Introducing the option --dump-html-program to security-analyser.

Author: marek-trtik

src/driver/sec_driver_parse_options.cpp

@@ -31,6 +31,7 @@
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/remove_exceptions.h>
+#include <analyses/call_graph.h>
 
 #include <analyses/goto_check.h>
 #include <analyses/local_may_alias.h>
@@ -253,6 +254,45 @@ int sec_driver_parse_optionst::doit()
     return 0;
   }
 
+  if(cmdline.isset("dump-html-program"))
+  {
+    status()
+      << "Dumping GOTO program in HTML format under directory: '"
+      << cmdline.get_value("dump-html-program")
+      << "'..."
+      << eom;
+    if(fileutl_file_exists(cmdline.get_value("dump-html-program")))
+    {
+      error()
+        << "ERROR: The output path '"
+        << cmdline.get_value("dump-html-program")
+        << "' for the HTML dump exists."
+        << eom;
+      return -1;
+    }
+    class_hierarchyt class_hierarchy;
+    class_hierarchy(goto_model.symbol_table);
+    call_grapht call_graph(goto_model.goto_functions);
+    std::vector<irep_idt> inverted_topological_order;
+    {
+      std::unordered_set<irep_idt, dstring_hash> processed;
+      for(const auto &elem : goto_model.goto_functions.function_map)
+        inverted_partial_topological_order(
+          call_graph,
+          elem.first,
+          processed,
+          inverted_topological_order);
+    }
+    dump_goto_program_in_html(
+      goto_model,
+      call_graph,
+      class_hierarchy,
+      goto_model.symbol_table,
+      inverted_topological_order,
+      cmdline.get_value("dump-html-program"));
+    return 0;
+  }
+
   error() << "no analysis option given -- consider reading --help"
           << eom;
   return 6;
@@ -416,6 +456,10 @@ void sec_driver_parse_optionst::help()
     " --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"
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"

src/driver/sec_driver_parse_options.h

@@ -25,6 +25,7 @@ class optionst;
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-loops)" \
   "(show-symbol-table)(show-parse-tree)" \
+  "(dump-html-program):" \
   "(show-properties)(show-reachable-properties)(property):" \
   "(verbosity):(version)" \
   "(gcc)(arch):" \