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 <iostream>
15 
16 #include <util/xml.h>
17 #include <util/json.h>
18 #include <util/json_expr.h>
19 #include <util/xml_expr.h>
20 #include <util/cprover_prefix.h>
21 #include <util/prefix.h>
22 
23 #include <langapi/language_util.h>
26 
27 #include "goto_functions.h"
28 #include "goto_model.h"
29 
31  const namespacet &ns,
34  const goto_functionst &goto_functions,
35  bool list_only)
36 {
38  switch(ui)
39  {
41  {
42  show_goto_functions_xmlt xml_show_functions(ns, list_only);
43  msg.status() << xml_show_functions.convert(goto_functions);
44  }
45  break;
46 
48  {
49  show_goto_functions_jsont json_show_functions(ns, list_only);
50  msg.status() << json_show_functions.convert(goto_functions);
51  }
52  break;
53 
55  if(list_only)
56  {
57  for(const auto &fun : goto_functions.function_map)
58  {
59  const symbolt &symbol = ns.lookup(fun.first);
60  msg.status() << '\n'
61  << symbol.display_name() << " /* " << symbol.name
62  << (fun.second.body_available() ? ""
63  : ", body not available")
64  << " */";
65  }
66 
67  msg.status() << messaget::eom;
68  }
69  else
70  {
71  goto_functions.output(ns, msg.status());
72  msg.status() << messaget::eom;
73  }
74 
75  break;
76  }
77 }
78 
80  const goto_modelt &goto_model,
83  bool list_only)
84 {
85  const namespacet ns(goto_model.symbol_table);
87  ns, message_handler, ui, goto_model.goto_functions, list_only);
88 }
irep_idt name
The unique identifier.
Definition: symbol.h:43
Show the goto functions.
Goto Programs with Functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
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...
void output(const namespacet &ns, std::ostream &out) const
Expressions in JSON.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const irep_idt & display_name() const
Definition: symbol.h:57
mstreamt & status() const
Definition: message.h:317
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
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...