CBMC
Loading...
Searching...
No Matches
show_goto_functions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Show goto functions
4
5Author: 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 {
33 msg.status() << xml_show_functions.convert(goto_functions);
34 }
35 break;
36
38 {
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}
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
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:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Symbol table entry.
Definition symbol.h:28
irep_idt name
The unique identifier.
Definition symbol.h:40
const irep_idt & display_name() const
Return language specific display name if present.
Definition symbol.h:55
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.