cprover
get_module.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Find module symbol using name
4
5Author: 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 "range.h"
19#include "symbol_table.h"
20
21typedef std::list<const symbolt *> symbolptr_listt;
22
24 const symbol_tablet &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_tablet::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_tablet &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:396
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
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.
The symbol table.
Definition: symbol_table.h:14
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_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
Definition: get_module.cpp:69
const symbolt & get_module_by_name(const symbol_tablet &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:47
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:541
Author: Diffblue Ltd.