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/json_expr.h>
17 #include <util/xml_expr.h>
18 #include <util/cprover_prefix.h>
19 #include <util/prefix.h>
20 
21 #include <langapi/language_util.h>
24 
25 #include "goto_functions.h"
26 #include "goto_model.h"
27 
29  const namespacet &ns,
30  message_handlert &message_handler,
32  const goto_functionst &goto_functions,
33  bool list_only)
34 {
35  messaget msg(message_handler);
36  switch(ui)
37  {
39  {
40  show_goto_functions_xmlt xml_show_functions(ns, list_only);
41  msg.status() << xml_show_functions.convert(goto_functions);
42  }
43  break;
44 
46  {
47  show_goto_functions_jsont json_show_functions(ns, list_only);
48  msg.status() << json_show_functions.convert(goto_functions);
49  }
50  break;
51 
53  {
54  // sort alphabetically
55  const auto sorted = goto_functions.sorted();
56 
57  for(const auto &fun : sorted)
58  {
59  const symbolt &symbol = ns.lookup(fun->first);
60  const bool has_body = fun->second.body_available();
61 
62  if(list_only)
63  {
64  msg.status() << '\n'
65  << symbol.display_name() << " /* " << symbol.name
66  << (has_body ? "" : ", body not available") << " */";
67  msg.status() << messaget::eom;
68  }
69  else if(has_body)
70  {
71  msg.status() << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";
72 
73  msg.status() << messaget::bold << symbol.display_name()
74  << messaget::reset << " /* " << symbol.name << " */\n";
75  fun->second.body.output(ns, symbol.name, msg.status());
76  msg.status() << messaget::eom;
77  }
78  }
79  }
80 
81  break;
82  }
83 }
84 
86  const goto_modelt &goto_model,
87  message_handlert &message_handler,
89  bool list_only)
90 {
91  const namespacet ns(goto_model.symbol_table);
93  ns, message_handler, ui, goto_model.goto_functions, list_only);
94 }
irep_idt name
The unique identifier.
Definition: symbol.h:40
static const commandt bold
render text with bold font
Definition: message.h:369
Show the goto functions.
Goto Programs with Functions.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:330
Symbol Table + CFG.
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...
Expressions in JSON.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
A collection of goto functions.
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
static eomt eom
Definition: message.h:284
mstreamt & status() const
Definition: message.h:401
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
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...