cprover
show_goto_functions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Show goto functions
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "show_goto_functions.h"
13 
14 #include <util/xml.h>
15 #include <util/json.h>
16 #include <util/cprover_prefix.h>
17 #include <util/prefix.h>
18 
19 #include <langapi/language_util.h>
22 
23 #include "goto_functions.h"
24 #include "goto_model.h"
25 
27  const namespacet &ns,
28  ui_message_handlert &ui_message_handler,
29  const goto_functionst &goto_functions,
30  bool list_only)
31 {
32  ui_message_handlert::uit ui = ui_message_handler.get_ui();
33  messaget msg(ui_message_handler);
34  switch(ui)
35  {
37  {
38  show_goto_functions_xmlt xml_show_functions(ns, list_only);
39  msg.status() << xml_show_functions.convert(goto_functions);
40  }
41  break;
42 
44  {
45  show_goto_functions_jsont json_show_functions(ns, list_only);
46  msg.status() << json_show_functions.convert(goto_functions);
47  }
48  break;
49 
51  {
52  // sort alphabetically
53  const auto sorted = goto_functions.sorted();
54 
55  for(const auto &fun : sorted)
56  {
57  const symbolt &symbol = ns.lookup(fun->first);
58  const bool has_body = fun->second.body_available();
59 
60  if(list_only)
61  {
62  msg.status() << '\n'
63  << symbol.display_name() << " /* " << symbol.name
64  << (has_body ? "" : ", body not available") << " */";
65  msg.status() << messaget::eom;
66  }
67  else if(has_body)
68  {
69  msg.status() << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";
70 
71  msg.status() << messaget::bold << symbol.display_name()
72  << messaget::reset << " /* " << symbol.name << " */\n";
73  fun->second.body.output(ns, symbol.name, msg.status());
74  msg.status() << messaget::eom;
75  }
76  }
77  }
78 
79  break;
80  }
81 }
82 
84  const goto_modelt &goto_model,
85  ui_message_handlert &ui_message_handler,
86  bool list_only)
87 {
88  const namespacet ns(goto_model.symbol_table);
90  ns, ui_message_handler, goto_model.goto_functions, list_only);
91 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
ui_message_handlert
Definition: ui_message.h:20
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:343
show_goto_functions_json.h
Goto Program.
ui_message_handlert::uit::XML_UI
@ XML_UI
symbolt::display_name
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
messaget::status
mstreamt & status() const
Definition: message.h:414
prefix.h
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
show_goto_functions.h
Show the goto functions.
show_goto_functions_xmlt::convert
xmlt convert(const goto_functionst &goto_functions)
Walks through all of the functions in the program and returns an xml object representing all their fu...
Definition: show_goto_functions_xml.cpp:44
messaget::eom
static eomt eom
Definition: message.h:297
xml.h
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
ui_message_handlert::uit
uit
Definition: ui_message.h:22
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
messaget::bold
static const commandt bold
render text with bold font
Definition: message.h:382
ui_message_handlert::uit::JSON_UI
@ JSON_UI
show_goto_functions_xml.h
Goto Program.
language_util.h
show_goto_functions_jsont::convert
json_objectt convert(const goto_functionst &goto_functions)
Walks through all of the functions in the program and returns a JSON object representing all their fu...
Definition: show_goto_functions_json.cpp:38
show_goto_functions_jsont
Definition: show_goto_functions_json.h:21
show_goto_functions
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
Definition: show_goto_functions.cpp:26
cprover_prefix.h
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
ui_message_handlert::uit::PLAIN
@ PLAIN
symbolt
Symbol table entry.
Definition: symbol.h:28
json.h
show_goto_functions_xmlt
Definition: show_goto_functions_xml.h:21
goto_functions.h
Goto Programs with Functions.
goto_functionst::sorted
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
Definition: goto_functions.cpp:62
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40