CBMC
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 "message.h"
15 #include "range.h"
16 #include "symbol_table_base.h"
17 
18 #include <list>
19 #include <set>
20 
21 typedef std::list<const symbolt *> symbolptr_listt;
22 
24  const symbol_table_baset &symbol_table,
25  const std::string &module,
26  message_handlert &message_handler)
27 {
28  symbolptr_listt symbolptr_list;
29  messaget message(message_handler);
30 
31  for(const auto &symbol_name_entry :
32  equal_range(symbol_table.symbol_base_map, module))
33  {
34  symbol_table_baset::symbolst::const_iterator it2 =
35  symbol_table.symbols.find(symbol_name_entry.second);
36 
37  if(it2==symbol_table.symbols.end())
38  continue;
39 
40  const symbolt &s=it2->second;
41 
42  if(s.is_type || s.type.id()!=ID_module)
43  continue;
44 
45  symbolptr_list.push_back(&s);
46  }
47 
48  if(symbolptr_list.empty())
49  {
50  message.error() << "module '" << module << "' not found" << messaget::eom;
51  throw 0;
52  }
53  else if(symbolptr_list.size()>=2)
54  {
55  message.error() << "module '" << module << "' does not uniquely resolve:\n";
56 
57  for(const symbolt *symbol_ptr : symbolptr_list)
58  message.error() << " " << symbol_ptr->name << '\n';
59 
60  message.error() << messaget::eom;
61  throw 0;
62  }
63 
64  // symbolptr_list has exactly one element
65 
66  return *symbolptr_list.front();
67 }
68 
70  const symbol_table_baset &symbol_table,
71  const std::string &module,
72  message_handlert &message_handler)
73 {
74  if(!module.empty())
75  return get_module_by_name(symbol_table, module, message_handler);
76 
77  symbolptr_listt symbolptr_list, main_symbolptr_list;
78  messaget message(message_handler);
79 
80  for(const auto &symbol_pair : symbol_table.symbols)
81  {
82  const symbolt &s = symbol_pair.second;
83 
84  if(s.type.id()!=ID_module)
85  continue;
86 
87  // this is our default
88  if(s.base_name==ID_main)
89  return get_module_by_name(symbol_table, "main", message_handler);
90 
91  symbolptr_list.push_back(&s);
92  }
93 
94  if(symbolptr_list.empty())
95  {
96  message.error() << "no module found" << messaget::eom;
97  throw 0;
98  }
99  else if(symbolptr_list.size()>=2)
100  {
101  // sorted alphabetically
102  std::set<std::string> modules;
103 
104  for(const symbolt *symbol_ptr : symbolptr_list)
105  modules.insert(id2string(symbol_ptr->pretty_name));
106 
107  message.error() << "multiple modules found, please select one:\n";
108 
109  for(const auto &s_it : modules)
110  message.error() << " " << s_it << '\n';
111 
112  message.error() << messaget::eom;
113  throw 0;
114  }
115 
116  // symbolptr_list has exactly one element
117 
118  const symbolt &symbol=*symbolptr_list.front();
119 
120  message.status() << "Using module '" << symbol.pretty_name << "'"
121  << messaget::eom;
122 
123  return symbol;
124 }
const irep_idt & id() const
Definition: irep.h:384
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
mstreamt & status() const
Definition: message.h:414
static eomt eom
Definition: message.h:297
The symbol table base class interface.
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_type
Definition: symbol.h:61
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
std::list< const symbolt * > symbolptr_listt
Definition: get_module.cpp:21
const symbolt & get_module(const symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
Definition: get_module.cpp:69
const symbolt & get_module_by_name(const symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
Definition: get_module.cpp:23
Find module symbol using name.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< typename multimapt::const_iterator > equal_range(const multimapt &multimap, const typename multimapt::key_type &key)
Utility function to make equal_range method of multimap easier to use by returning a ranget object.
Definition: range.h:539
Author: Diffblue Ltd.