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 
22 #define forall_symbolptr_list(it, list) \
23  for(symbolptr_listt::const_iterator it=(list).begin(); \
24  it!=(list).end(); ++it)
25 
26 #define Forall_symbolptr_list(it, list) \
27  for(symbolptr_listt::iterator it=(list).begin(); \
28  it!=(list).end(); ++it)
29 
31  const symbol_tablet &symbol_table,
32  const std::string &module,
33  message_handlert &message_handler)
34 {
35  symbolptr_listt symbolptr_list;
36  messaget message(message_handler);
37 
38  forall_symbol_base_map(it, symbol_table.symbol_base_map, module)
39  {
40  symbol_tablet::symbolst::const_iterator it2=
41  symbol_table.symbols.find(it->second);
42 
43  if(it2==symbol_table.symbols.end())
44  continue;
45 
46  const symbolt &s=it2->second;
47 
48  if(s.is_type || s.type.id()!=ID_module)
49  continue;
50 
51  symbolptr_list.push_back(&s);
52  }
53 
54  if(symbolptr_list.empty())
55  {
56  message.error() << "module '" << module << "' not found" << messaget::eom;
57  throw 0;
58  }
59  else if(symbolptr_list.size()>=2)
60  {
61  message.error() << "module '" << module << "' does not uniquely resolve:\n";
62 
63  forall_symbolptr_list(it, symbolptr_list)
64  message.error() << " " << (*it)->name << '\n';
65 
66  message.error() << messaget::eom;
67  throw 0;
68  }
69 
70  // symbolptr_list has exactly one element
71 
72  return *symbolptr_list.front();
73 }
74 
76  const symbol_tablet &symbol_table,
77  const std::string &module,
78  message_handlert &message_handler)
79 {
80  if(!module.empty())
81  return get_module_by_name(symbol_table, module, message_handler);
82 
83  symbolptr_listt symbolptr_list, main_symbolptr_list;
84  messaget message(message_handler);
85 
86  for(const auto &symbol_pair : symbol_table.symbols)
87  {
88  const symbolt &s = symbol_pair.second;
89 
90  if(s.type.id()!=ID_module)
91  continue;
92 
93  // this is our default
94  if(s.base_name==ID_main)
95  return get_module_by_name(symbol_table, "main", message_handler);
96 
97  symbolptr_list.push_back(&s);
98  }
99 
100  if(symbolptr_list.empty())
101  {
102  message.error() << "no module found" << messaget::eom;
103  throw 0;
104  }
105  else if(symbolptr_list.size()>=2)
106  {
107  // sorted alphabetically
108  std::set<std::string> modules;
109 
110  forall_symbolptr_list(it, symbolptr_list)
111  modules.insert(id2string((*it)->pretty_name));
112 
113  message.error() << "multiple modules found, please select one:\n";
114 
115  for(const auto &s_it : modules)
116  message.error() << " " << s_it << '\n';
117 
118  message.error() << messaget::eom;
119  throw 0;
120  }
121 
122  // symbolptr_list has exactly one element
123 
124  const symbolt &symbol=*symbolptr_list.front();
125 
126  message.status() << "Using module '" << symbol.pretty_name << "'"
127  << messaget::eom;
128 
129  return symbol;
130 }
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
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:75
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:30
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
forall_symbolptr_list
#define forall_symbolptr_list(it, list)
Definition: get_module.cpp:22
message.h
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbolptr_listt
std::list< const symbolt * > symbolptr_listt
Definition: get_module.cpp:20
irept::id
const irep_idt & id() const
Definition: irep.h:418
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.