Merge pull request diffblue#467 from diffblue/save_goto_binary_without_analysis

SEC-513: Added: Java -> GOTO binary.

Author: marek-trtik

src/driver/sec_driver_parse_options.cpp

@@ -20,6 +20,7 @@
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
+#include <goto-programs/write_goto_binary.h>
 #include <java_bytecode/java_bytecode_language.h>
 #include <jsil/jsil_language.h>
 #include <linking/static_lifetime_init.h>
@@ -221,6 +222,21 @@ int sec_driver_parse_optionst::doit()
     local_value_sett::do_not_use_precise_access_paths = true;
   }
 
+  if(cmdline.isset("output-goto-binary"))
+  {
+    const irep_idt &binary_pathname = cmdline.get_value("goto-binary");
+    status() << "Saving loaded program as GOTO binary."  << messaget::eom;
+    const bool fail = write_goto_binary(
+      as_string(binary_pathname), goto_model, get_message_handler());
+    if(fail)
+    {
+      error()
+        << "ERROR: Call to 'write_goto_binary' has FAILED." << messaget::eom;
+      return CPROVER_EXIT_EXCEPTION;
+    }
+    return CPROVER_EXIT_SUCCESS;
+  }
+
   if(cmdline.isset("security-scanner"))
   {
     try
@@ -631,6 +647,8 @@ void sec_driver_parse_optionst::help()
     "                                  a directory. Pass a non existing directory\n"
     "                                  path-name with this option. The directory\n"
     "                                  will be created with the dumped program.\n"
+    " --output-goto-binary             save the input Java program as GOTO binary\n"
+    "                                  and exit.\n"
     "\n"
     "Other options:\n"
     " --version                        show version and exit\n"

src/driver/sec_driver_parse_options.h

@@ -53,6 +53,7 @@ class optionst;
   "(java-max-input-array-length):" \
   "(string-max-input-length):" \
   "(java-max-input-tree-depth):" \
+  "(output-goto-binary):" \
   UI_MESSAGE_OPTIONS \
   JAVA_BYTECODE_LANGUAGE_OPTIONS \
   // End of options