Add LVSA summary dump-to-JSON

Author: smowton

src/analyses/static_analysis.cpp

@@ -110,6 +110,30 @@ void static_analysis_baset::output(
   }
 }
 
+jsont static_analysis_baset::output_json(
+  const goto_programt &goto_program,
+  const irep_idt &identifier) const
+{
+  json_arrayt retval;
+
+  forall_goto_program_instructions(i_it, goto_program)
+  {
+    std::ostringstream out;
+    out << "**** " << i_it->location_number << " "
+        << i_it->source_location << "\n";
+
+    get_state(i_it).output(ns, out);
+    out << "\n";
+    #if 1
+    goto_program.output_instruction(ns, identifier, out, i_it);
+    out << "\n";
+    #endif
+    retval.push_back(json_stringt(out.str()));
+  }
+
+  return retval;
+}
+
 void static_analysis_baset::generate_states(
   const goto_functionst &goto_functions)
 {

src/analyses/static_analysis.h

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 #include <unordered_set>
 
+#include <util/json.h>
 #include <util/make_unique.h>
 
 #include <goto-programs/goto_functions.h>
@@ -157,6 +158,11 @@ class static_analysis_baset
     output(goto_program, "", out);
   }
 
+  jsont output_json(const goto_programt &goto_program) const
+  {
+    return output_json(goto_program, "");
+  }
+
   virtual bool has_location(locationt l) const=0;
 
   void insert(locationt l)
@@ -183,6 +189,10 @@ class static_analysis_baset
     const irep_idt &identifier,
     std::ostream &out) const;
 
+  virtual jsont output_json(
+    const goto_programt &goto_program,
+    const irep_idt &identifier) const;
+
   typedef std::map<unsigned, locationt> working_sett;
 
   locationt get_next(working_sett &working_set);

src/util/ui_message.h

@@ -12,6 +12,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "message.h"
 
+#define UI_MESSAGE_OPTIONS \
+  "(json-ui)" \
+  "(xml-ui)" \
+  // End of options
+
 class ui_message_handlert:public message_handlert
 {
 public: