CBMC
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/ui_message.h>
15 
16 #include "goto_model.h"
19 
21  const namespacet &ns,
22  ui_message_handlert &ui_message_handler,
23  const goto_functionst &goto_functions,
24  bool list_only)
25 {
26  ui_message_handlert::uit ui = ui_message_handler.get_ui();
27  messaget msg(ui_message_handler);
28  switch(ui)
29  {
31  {
32  show_goto_functions_xmlt xml_show_functions(list_only);
33  msg.status() << xml_show_functions.convert(goto_functions);
34  }
35  break;
36 
38  {
39  show_goto_functions_jsont json_show_functions(list_only);
40  msg.status() << json_show_functions.convert(goto_functions);
41  }
42  break;
43 
45  {
46  // sort alphabetically
47  const auto sorted = goto_functions.sorted();
48 
49  for(const auto &fun : sorted)
50  {
51  const symbolt &symbol = ns.lookup(fun->first);
52  const bool has_body = fun->second.body_available();
53 
54  if(list_only)
55  {
56  msg.status() << '\n'
57  << symbol.display_name() << " /* " << symbol.name
58  << (has_body ? "" : ", body not available") << " */";
59  msg.status() << messaget::eom;
60  }
61  else if(has_body)
62  {
63  msg.status() << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";
64 
65  msg.status() << messaget::bold << symbol.display_name()
66  << messaget::reset << " /* " << symbol.name << " */\n";
67  fun->second.body.output(msg.status());
68  msg.status() << messaget::eom;
69  }
70  }
71  }
72 
73  break;
74  }
75 }
76 
78  const goto_modelt &goto_model,
79  ui_message_handlert &ui_message_handler,
80  bool list_only)
81 {
82  const namespacet ns(goto_model.symbol_table);
84  ns, ui_message_handler, goto_model.goto_functions, list_only);
85 }
A collection of goto functions.
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:335
mstreamt & status() const
Definition: message.h:406
static const commandt bold
render text with bold font
Definition: message.h:374
static eomt eom
Definition: message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
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...
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...
Symbol table entry.
Definition: symbol.h:28
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
irep_idt name
The unique identifier.
Definition: symbol.h:40
virtual uit get_ui() const
Definition: ui_message.h:33
Symbol Table + CFG.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
Show the goto functions.