Show goto functions

src/cbmc/cbmc_parse_options.cpp

@@ -38,6 +38,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/show_goto_functions.h>
 
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>
@@ -965,7 +966,7 @@ bool cbmc_parse_optionst::process_goto_program(
     if(cmdline.isset("show-goto-functions"))
     {
       namespacet ns(symbol_table);
-      goto_functions.output(ns, std::cout);
+      show_goto_functions(ns, get_ui(), goto_functions);
       return true;
     }
   }

src/goto-programs/show_goto_functions.cpp

@@ -0,0 +1,104 @@
+/*******************************************************************\
+
+Module: Show goto functions
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+#include <iostream>
+
+#include <util/xml.h>
+#include <util/json.h>
+#include <util/i2string.h>
+#include <util/xml_expr.h>
+
+#include <langapi/language_util.h>
+
+#include "show_goto_functions.h"
+#include "goto_functions.h"
+#include "goto_model.h"
+
+/*******************************************************************\
+
+Function: cbmc_parseoptionst::show_goto_functions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void show_goto_functions(
+  const namespacet &ns,
+  ui_message_handlert::uit ui,
+  const goto_functionst &goto_functions)
+{
+  switch(ui)
+  {
+  case ui_message_handlert::XML_UI:
+  {
+    //This only prints the list of functions
+    xmlt xml_functions("functions");
+    for(goto_functionst::function_mapt::const_iterator
+          it=goto_functions.function_map.begin();
+        it!=goto_functions.function_map.end();
+        it++)
+    {
+      xmlt &xml_function=xml_functions.new_element("function");
+      xml_function.set_attribute("name", id2string(it->first)); 
+    }
+
+    std::cout << xml_functions << std::endl;
+  }
+  break;
+
+  case ui_message_handlert::JSON_UI:
+  {
+    //This only prints the list of functions
+    json_arrayt json_functions;
+    for(goto_functionst::function_mapt::const_iterator
+          it=goto_functions.function_map.begin();
+        it!=goto_functions.function_map.end();
+        it++)
+    {
+      json_objectt &json_function=
+        json_functions.push_back(jsont()).make_object();
+      json_function["name"]=json_stringt(id2string(it->first));
+    }
+    json_objectt json_result;
+    json_result["functions"]=json_functions;
+    std::cout << ",\n" << json_result;
+  }
+  break;
+
+  case ui_message_handlert::PLAIN:
+    goto_functions.output(ns, std::cout);
+    break;
+  }
+}
+
+/*******************************************************************\
+
+Function: show_goto_functions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void show_goto_functions(
+  const goto_modelt &goto_model,
+  ui_message_handlert::uit ui)
+{
+  const namespacet ns(goto_model.symbol_table);
+  show_goto_functions(ns, ui, goto_model.goto_functions);
+}
+
+
+

src/goto-programs/show_goto_functions.h

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Show the goto functions
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_H
+#define CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_H
+
+#include <util/ui_message.h>
+
+class goto_functionst;
+class namespacet;
+class goto_modelt;
+
+void show_goto_functions(
+  const namespacet &ns,
+  ui_message_handlert::uit ui,
+  const goto_functionst &goto_functions);
+
+void show_goto_functions(
+  const goto_modelt &,
+  ui_message_handlert::uit ui);
+
+#endif