Adding computation and save of goto program statistics.

Author: marek-trtik

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -42,6 +42,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/parameter_assignments.h>
 #include <goto-programs/slice_global_inits.h>
 #include <goto-programs/show_symbol_table.h>
+#include <goto-programs/goto_statistics.h>
 
 #include <pointer-analysis/value_set_analysis.h>
 #include <pointer-analysis/goto_program_dereference.h>
@@ -61,6 +62,8 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/constant_propagator.h>
 #include <analyses/is_threaded.h>
 
+#include <util/file_util.h>
+
 #include <cbmc/version.h>
 
 #include "document_properties.h"
@@ -738,6 +741,32 @@ int goto_instrument_parse_optionst::doit()
       undefined_function_abort_path(goto_model);
     }
 
+    if(cmdline.isset("save-code-statistics"))
+    {
+      goto_statisticst stats;
+      stats.extend(goto_model);
+      const std::string out_json_file_pathname=
+        cmdline.get_value("save-code-statistics");
+      if(fileutl_is_directory(out_json_file_pathname))
+      {
+        error() << "The path-name '" << cmdline.args[1]
+                << "'passed to the option '--save-code-statistics' "
+                  "represents an existing directory."
+                << eom;
+        return 12;
+      }
+      if(fileutl_parse_extension_in_pathname(out_json_file_pathname)!=".json")
+      {
+        error() << "The file of the path-name '" << cmdline.args[1]
+                << "'passed to the option '--save-code-statistics' does "
+                  "not have '.json' extension."
+                << eom;
+        return 13;
+      }
+      std::ofstream ofile(out_json_file_pathname);
+      ofile << to_json(stats);
+    }
+
     // write new binary?
     if(cmdline.args.size()==2)
     {
@@ -1450,6 +1479,9 @@ void goto_instrument_parse_optionst::help()
     " --list-calls-args            list all function calls with their arguments\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --print-path-lengths         print statistics about control-flow graph paths\n"
+    " --save-code-statistics       saves a json file with basic statistical data of"
+    "                              the analysed program after all analyses and\n"
+    "                              transformations have been performed on it.\n"
     "\n"
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -59,6 +59,7 @@ Author: Daniel Kroening, [email protected]
   "(show-uninitialized)(show-locations)" \
   "(full-slice)(reachability-slice)(slice-global-inits)" \
   "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
+  "(save-code-statistics):" \
   OPT_REMOVE_CONST_FUNCTION_POINTERS \
   "(print-internal-representation)" \
   "(remove-function-pointers)" \