cprover
get_module.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Find module symbol using name
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "get_module.h"
13 
14 #include <list>
15 #include <set>
16 
17 #include "message.h"
18 #include "symbol_table.h"
19 
20 typedef std::list<const symbolt *> symbolptr_listt;
21 
23  const symbol_tablet &symbol_table,
24  const std::string &module,
25  message_handlert &message_handler)
26 {
27  symbolptr_listt symbolptr_list;
28  messaget message(message_handler);
29 
30  forall_symbol_base_map(it, symbol_table.symbol_base_map, module)
31  {
32  symbol_tablet::symbolst::const_iterator it2=
33  symbol_table.symbols.find(it->second);
34 
35  if(it2==symbol_table.symbols.end())
36  continue;
37 
38  const symbolt &s=it2->second;
39 
40  if(s.is_type || s.type.id()!=ID_module)
41  continue;
42 
43  symbolptr_list.push_back(&s);
44  }
45 
46  if(symbolptr_list.empty())
47  {
48  message.error() << "module '" << module << "' not found" << messaget::eom;
49  throw 0;
50  }
51  else if(symbolptr_list.size()>=2)
52  {
53  message.error() << "module '" << module << "' does not uniquely resolve:\n";
54 
55  for(const symbolt *symbol_ptr : symbolptr_list)
56  message.error() << " " << symbol_ptr->name << '\n';
57 
58  message.error() << messaget::eom;
59  throw 0;
60  }
61 
62  // symbolptr_list has exactly one element
63 
64  return *symbolptr_list.front();
65 }
66 
68  const symbol_tablet &symbol_table,
69  const std::string &module,
70  message_handlert &message_handler)
71 {
72  if(!module.empty())
73  return get_module_by_name(symbol_table, module, message_handler);
74 
75  symbolptr_listt symbolptr_list, main_symbolptr_list;
76  messaget message(message_handler);
77 
78  for(const auto &symbol_pair : symbol_table.symbols)
79  {
80  const symbolt &s = symbol_pair.second;
81 
82  if(s.type.id()!=ID_module)
83  continue;
84 
85  // this is our default
86  if(s.base_name==ID_main)
87  return get_module_by_name(symbol_table, "main", message_handler);
88 
89  symbolptr_list.push_back(&s);
90  }
91 
92  if(symbolptr_list.empty())
93  {
94  message.error() << "no module found" << messaget::eom;
95  throw 0;
96  }
97  else if(symbolptr_list.size()>=2)
98  {
99  // sorted alphabetically
100  std::set<std::string> modules;
101 
102  for(const symbolt *symbol_ptr : symbolptr_list)
103  modules.insert(id2string(symbol_ptr->pretty_name));
104 
105  message.error() << "multiple modules found, please select one:\n";
106 
107  for(const auto &s_it : modules)
108  message.error() << " " << s_it << '\n';
109 
110  message.error() << messaget::eom;
111  throw 0;
112  }
113 
114  // symbolptr_list has exactly one element
115 
116  const symbolt &symbol=*symbolptr_list.front();
117 
118  message.status() << "Using module '" << symbol.pretty_name << "'"
119  << messaget::eom;
120 
121  return symbol;
122 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbol_table_baset::symbol_base_map
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
Definition: symbol_table_base.h:33
messaget::status
mstreamt & status() const
Definition: message.h:414
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
get_module.h
Find module symbol using name.
get_module
const symbolt & get_module(const symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
Definition: get_module.cpp:67
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
messaget::eom
static eomt eom
Definition: message.h:297
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
get_module_by_name
const symbolt & get_module_by_name(const symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
Definition: get_module.cpp:22
message.h
messaget::error
mstreamt & error() const
Definition: message.h:399
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
symbolptr_listt
std::list< const symbolt * > symbolptr_listt
Definition: get_module.cpp:20
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
forall_symbol_base_map
#define forall_symbol_base_map(it, expr, base_name)
Definition: symbol_table.h:11
symbol_table.h
Author: Diffblue Ltd.