Option for listing the goto functions

src/cbmc/cbmc_parse_options.cpp

@@ -636,9 +636,15 @@ int cbmc_parse_optionst::get_goto_program(
     }
 
     // show it?
-    if(cmdline.isset("show-goto-functions"))
+    if(
+      cmdline.isset("show-goto-functions") ||
+      cmdline.isset("list-goto-functions"))
     {
-      show_goto_functions(goto_model, ui_message_handler.get_ui());
+      show_goto_functions(
+        goto_model,
+        get_message_handler(),
+        ui_message_handler.get_ui(),
+        cmdline.isset("list-goto-functions"));
       return CPROVER_EXIT_SUCCESS;
     }
 
@@ -897,6 +903,7 @@ int cbmc_parse_optionst::do_bmc(bmct &bmc)
 /// display command line help
 void cbmc_parse_optionst::help()
 {
+  // clang-format off
   std::cout <<
     "\n"
     "* *   CBMC " CBMC_VERSION " - Copyright (C) 2001-2017 ";
@@ -1025,4 +1032,5 @@ void cbmc_parse_optionst::help()
     HELP_GOTO_TRACE
     " --verbosity #                verbosity level\n"
     "\n";
+  // clang-format on
 }

src/cbmc/cbmc_parse_options.h

@@ -26,6 +26,7 @@ class bmct;
 class goto_functionst;
 class optionst;
 
+// clang-format off
 #define CBMC_OPTIONS \
   "(program-only)(preprocess)(slice-by-trace):" \
   OPT_FUNCTIONS \
@@ -50,7 +51,8 @@ class optionst;
   "(string-max-input-length):" \
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
-  "(show-goto-functions)(show-loops)" \
+  OPT_SHOW_GOTO_FUNCTIONS \
+  "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)(show-vcc)" \
   "(show-claims)(claim):(show-properties)" \
   "(drop-unused-functions)" \
@@ -69,6 +71,7 @@ class optionst;
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
+// clang-format on
 
 class cbmc_parse_optionst:
   public parse_options_baset,

src/clobber/clobber_parse_options.cpp

@@ -136,9 +136,15 @@ int clobber_parse_optionst::doit()
     }
 
     // show it?
-    if(cmdline.isset("show-goto-functions"))
+    if(
+      cmdline.isset("show-goto-functions") ||
+      cmdline.isset("list-goto-functions"))
     {
-      show_goto_functions(goto_model, get_ui());
+      show_goto_functions(
+        goto_model,
+        get_message_handler(),
+        ui_message_handler.get_ui(),
+        cmdline.isset("list-goto-functions"));
       return 6;
     }
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -431,9 +431,15 @@ int goto_analyzer_parse_optionst::doit()
   }
 
   // show it?
-  if(cmdline.isset("show-goto-functions"))
-  {
-    show_goto_functions(goto_model, get_ui());
+  if(
+    cmdline.isset("show-goto-functions") ||
+    cmdline.isset("list-goto-functions"))
+  {
+    show_goto_functions(
+      goto_model,
+      get_message_handler(),
+      get_ui(),
+      cmdline.isset("list-goto-functions"));
     return CPROVER_EXIT_SUCCESS;
   }
 

src/goto-diff/goto_diff_parse_options.cpp

@@ -280,10 +280,27 @@ int goto_diff_parse_optionst::doit()
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
 
-  if(cmdline.isset("show-goto-functions"))
+  if(cmdline.isset("show-loops"))
   {
-    show_goto_functions(goto_model1, get_ui());
-    show_goto_functions(goto_model2, get_ui());
+    show_loop_ids(get_ui(), goto_model1);
+    show_loop_ids(get_ui(), goto_model2);
+    return true;
+  }
+
+  if(
+    cmdline.isset("show-goto-functions") ||
+    cmdline.isset("list-goto-functions"))
+  {
+    show_goto_functions(
+      goto_model1,
+      get_message_handler(),
+      ui_message_handler.get_ui(),
+      cmdline.isset("list-goto-functions"));
+    show_goto_functions(
+      goto_model2,
+      get_message_handler(),
+      ui_message_handler.get_ui(),
+      cmdline.isset("list-goto-functions"));
     return 0;
   }
 
@@ -430,20 +447,6 @@ bool goto_diff_parse_optionst::process_goto_program(
 
     // add loop ids
     goto_functions.compute_loop_numbers();
-
-    // show it?
-    if(cmdline.isset("show-loops"))
-    {
-      show_loop_ids(get_ui(), goto_model);
-      return true;
-    }
-
-    // show it?
-    if(cmdline.isset("show-goto-functions"))
-    {
-      show_goto_functions(goto_model, get_ui());
-      return true;
-    }
   }
 
   catch(const char *e)

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -575,10 +575,15 @@ int goto_instrument_parse_optionst::doit()
       return CPROVER_EXIT_SUCCESS;
     }
 
-    if(cmdline.isset("show-goto-functions"))
+    if(
+      cmdline.isset("show-goto-functions") ||
+      cmdline.isset("list-goto-functions"))
     {
-      namespacet ns(goto_model.symbol_table);
-      show_goto_functions(goto_model, get_ui());
+      show_goto_functions(
+        goto_model,
+        get_message_handler(),
+        ui_message_handler.get_ui(),
+        cmdline.isset("list-goto-functions"));
       return CPROVER_EXIT_SUCCESS;
     }
 

src/goto-programs/show_goto_functions.cpp

@@ -29,35 +29,60 @@ Author: Peter Schrammel
 
 void show_goto_functions(
   const namespacet &ns,
+  message_handlert &message_handler,
   ui_message_handlert::uit ui,
-  const goto_functionst &goto_functions)
+  const goto_functionst &goto_functions,
+  bool list_only)
 {
+  messaget msg(message_handler);
   switch(ui)
   {
   case ui_message_handlert::uit::XML_UI:
   {
-    show_goto_functions_xmlt xml_show_functions(ns);
-    xml_show_functions(goto_functions, std::cout);
+    show_goto_functions_xmlt xml_show_functions(ns, list_only);
+    msg.status() << xml_show_functions.convert(goto_functions);
   }
   break;
 
   case ui_message_handlert::uit::JSON_UI:
   {
-    show_goto_functions_jsont json_show_functions(ns);
-    json_show_functions(goto_functions, std::cout);
+    show_goto_functions_jsont json_show_functions(ns, list_only);
+    msg.status() << json_show_functions.convert(goto_functions);
   }
   break;
 
   case ui_message_handlert::uit::PLAIN:
-    goto_functions.output(ns, std::cout);
+    if(list_only)
+    {
+      for(const auto &fun : goto_functions.function_map)
+      {
+        const symbolt &symbol = ns.lookup(fun.first);
+        msg.status() << '\n'
+                     << symbol.display_name() << " /* " << symbol.name
+                     << (fun.second.body_available() ? ""
+                                                     : ", body not available")
+                     << " */";
+      }
+
+      msg.status() << messaget::eom;
+    }
+    else
+    {
+      goto_functions.output(ns, msg.status());
+      msg.status() << messaget::eom;
+    }
+
     break;
   }
 }
 
 void show_goto_functions(
   const goto_modelt &goto_model,
-  ui_message_handlert::uit ui)
+  message_handlert &message_handler,
+  ui_message_handlert::uit ui,
+  bool list_only)
 {
   const namespacet ns(goto_model.symbol_table);
-  show_goto_functions(ns, ui, goto_model.goto_functions);
+  show_goto_functions(
+    ns, message_handler, ui, goto_model.goto_functions, list_only);
 }

src/goto-programs/show_goto_functions.h

@@ -18,19 +18,27 @@ class namespacet;
 class goto_modelt;
 class goto_functionst;
 
+// clang-format off
 #define OPT_SHOW_GOTO_FUNCTIONS \
-  "(show-goto-functions)"
+  "(show-goto-functions)" \
+  "(list-goto-functions)"
 
 #define HELP_SHOW_GOTO_FUNCTIONS \
-  " --show-goto-functions        show goto program\n"
+  " --show-goto-functions        show goto program\n" \
+  " --list-goto-functions        list goto functions\n"
+// clang-format on
 
 void show_goto_functions(
   const namespacet &ns,
+  message_handlert &message_handler,
   ui_message_handlert::uit ui,
-  const goto_functionst &goto_functions);
+  const goto_functionst &goto_functions,
+  bool list_only = false);
 
 void show_goto_functions(
   const goto_modelt &,
-  ui_message_handlert::uit ui);
+  message_handlert &message_handler,
+  ui_message_handlert::uit ui,
+  bool list_only = false);
 
 #endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_H

src/goto-programs/show_goto_functions_json.cpp

@@ -26,8 +26,11 @@ Author: Thomas Kiley
 
 /// For outputting the GOTO program in a readable JSON format.
 /// \param ns: the namespace to use to resolve names with
-show_goto_functions_jsont::show_goto_functions_jsont(const namespacet &ns):
-  ns(ns)
+/// \param list_only: output only list of functions, but not their bodies
+show_goto_functions_jsont::show_goto_functions_jsont(
+  const namespacet &_ns,
+  bool _list_only)
+  : ns(_ns), list_only(_list_only)
 {}
 
 /// Walks through all of the functions in the program and returns a JSON object
@@ -55,6 +58,9 @@ json_objectt show_goto_functions_jsont::convert(
       has_prefix(id2string(function_name), "java::java");
     json_function["isInternal"]=jsont::json_boolean(is_internal);
 
+    if(list_only)
+      continue;
+
     if(function.body_available())
     {
       json_arrayt json_instruction_array=json_arrayt();

src/goto-programs/show_goto_functions_json.h

@@ -20,14 +20,17 @@ class namespacet;
 class show_goto_functions_jsont
 {
 public:
-  explicit show_goto_functions_jsont(const namespacet &ns);
+  explicit show_goto_functions_jsont(
+    const namespacet &_ns,
+    bool _list_only = false);
 
   json_objectt convert(const goto_functionst &goto_functions);
   void operator()(
     const goto_functionst &goto_functions, std::ostream &out, bool append=true);
 
 private:
   const namespacet &ns;
+  bool list_only;
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_JSON_H

src/goto-programs/show_goto_functions_xml.cpp

@@ -25,8 +25,11 @@ Author: Thomas Kiley
 
 /// For outputting the GOTO program in a readable xml format.
 /// \param ns: the namespace to use to resolve names with
-show_goto_functions_xmlt::show_goto_functions_xmlt(const namespacet &ns):
-  ns(ns)
+/// \param list_only: output only list of functions, but not their bodies
+show_goto_functions_xmlt::show_goto_functions_xmlt(
+  const namespacet &_ns,
+  bool _list_only)
+  : ns(_ns), list_only(_list_only)
 {}
 
 /// Walks through all of the functions in the program and returns an xml object
@@ -56,6 +59,9 @@ xmlt show_goto_functions_xmlt::convert(
       has_prefix(id2string(function_name), "java::java");
     xml_function.set_attribute_bool("is_internal", is_internal);
 
+    if(list_only)
+      continue;
+
     if(function.body_available())
     {
       xmlt &xml_instructions=xml_function.new_element("instructions");

src/goto-programs/show_goto_functions_xml.h

@@ -20,14 +20,17 @@ class namespacet;
 class show_goto_functions_xmlt
 {
 public:
-  explicit show_goto_functions_xmlt(const namespacet &ns);
+  explicit show_goto_functions_xmlt(
+    const namespacet &_ns,
+    bool _list_only = false);
 
   xmlt convert(const goto_functionst &goto_functions);
   void operator()(
     const goto_functionst &goto_functions, std::ostream &out, bool append=true);
 
 private:
   const namespacet &ns;
+  bool list_only;
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_XML_H

src/jbmc/jbmc_parse_options.cpp

@@ -601,9 +601,15 @@ int jbmc_parse_optionst::get_goto_program(
     }
 
     // show it?
-    if(cmdline.isset("show-goto-functions"))
+    if(
+      cmdline.isset("show-goto-functions") ||
+      cmdline.isset("list-goto-functions"))
     {
-      show_goto_functions(*goto_model, ui_message_handler.get_ui());
+      show_goto_functions(
+        *goto_model,
+        get_message_handler(),
+        ui_message_handler.get_ui(),
+        cmdline.isset("list-goto-functions"));
       return 0;
     }
 

src/jbmc/jbmc_parse_options.h

@@ -26,6 +26,7 @@ class bmct;
 class goto_functionst;
 class optionst;
 
+// clang-format off
 #define JBMC_OPTIONS \
   "(program-only)(preprocess)(slice-by-trace):" \
   OPT_FUNCTIONS \
@@ -49,7 +50,8 @@ class optionst;
   "(string-max-length):" \
   "(string-max-input-length):" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
-  "(show-goto-functions)(show-loops)" \
+  OPT_SHOW_GOTO_FUNCTIONS \
+  "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)(show-vcc)" \
   "(show-properties)" \
   "(drop-unused-functions)" \
@@ -66,6 +68,7 @@ class optionst;
   "(java-unwind-enum-static)" \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE
+// clang-format on
 
 class jbmc_parse_optionst:
   public parse_options_baset,