cprover
Loading...
Searching...
No Matches
linking_class.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Linking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_LINKING_LINKING_CLASS_H
13#define CPROVER_LINKING_LINKING_CLASS_H
14
15#include <util/namespace.h>
16#include <util/rename_symbol.h>
17#include <util/replace_symbol.h>
18#include <util/std_expr.h>
19#include <util/symbol.h>
20
21#include <unordered_set>
22
24
26{
27public:
28 bool replace(exprt &dest) const override;
29
30private:
31 bool replace_symbol_expr(symbol_exprt &dest) const override;
32};
33
35{
36public:
45
50
53
54protected:
56 const symbolt &old_symbol,
57 const symbolt &new_symbol);
58
60 const symbolt &old_symbol,
61 const symbolt &new_symbol);
62
64 const symbolt &old_symbol,
65 const symbolt &new_symbol)
66 {
67 if(new_symbol.is_type)
68 return needs_renaming_type(old_symbol, new_symbol);
69 else
70 return needs_renaming_non_type(old_symbol, new_symbol);
71 }
72
73 std::unordered_map<irep_idt, irep_idt> rename_symbols(
74 const symbol_table_baset &,
75 const std::unordered_set<irep_idt> &needs_to_be_renamed);
76 void copy_symbols(
77 const symbol_table_baset &,
78 const std::unordered_map<irep_idt, irep_idt> &);
79
81 symbolt &old_symbol,
82 symbolt &new_symbol);
83
85 symbolt &old_symbol,
86 symbolt &new_symbol);
87
89 symbolt &old_symbol,
90 symbolt &new_symbol);
91
93 const symbolt &old_symbol,
94 const symbolt &new_symbol,
95 bool &set_to_new);
96
98 {
107
111 std::unordered_set<irep_idt> o_symbols;
112 std::unordered_set<irep_idt> n_symbols;
113 };
114
116 const typet &type1,
117 const typet &type2,
119
121 symbolt &old_symbol,
122 const symbolt &new_symbol);
123
124 std::string expr_to_string(
125 const irep_idt &identifier,
126 const exprt &expr) const;
127
128 std::string type_to_string(
129 const irep_idt &identifier,
130 const typet &type) const;
131
132 std::string type_to_string_verbose(
133 const symbolt &symbol,
134 const typet &type) const;
135
137 const symbolt &symbol) const
138 {
139 return type_to_string_verbose(symbol, symbol.type);
140 }
141
146 const symbolt &old_symbol,
147 const symbolt &new_symbol,
148 const typet &type1,
149 const typet &type2,
150 unsigned depth,
152
154 const symbolt &old_symbol,
155 const symbolt &new_symbol,
156 const typet &type1,
157 const typet &type2)
158 {
161 old_symbol,
162 new_symbol,
163 type1,
164 type2,
165 10, // somewhat arbitrary limit
167 }
168
169 void link_error(
170 const symbolt &old_symbol,
171 const symbolt &new_symbol,
172 const std::string &msg);
173
174 void link_warning(
175 const symbolt &old_symbol,
176 const symbolt &new_symbol,
177 const std::string &msg);
178
180 const struct_typet &old_type,
181 const struct_typet &new_type);
182
186
187 irep_idt rename(const symbol_table_baset &, const irep_idt &);
188
189 // the new IDs created by renaming
190 std::unordered_set<irep_idt> renamed_ids;
191};
192
193#endif // CPROVER_LINKING_LINKING_CLASS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
bool replace_symbol_expr(symbol_exprt &dest) const override
Definition linking.cpp:94
bool replace(exprt &dest) const override
Definition linking.cpp:29
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
std::unordered_map< irep_idt, irep_idt > rename_symbols(const symbol_table_baset &, const std::unordered_set< irep_idt > &needs_to_be_renamed)
Definition linking.cpp:1421
void duplicate_non_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition linking.cpp:1176
bool adjust_object_type(const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new)
Definition linking.cpp:1069
bool link(const symbol_table_baset &src_symbol_table)
Merges the symbol table src_symbol_table into main_symbol_table, renaming symbols from src_symbol_tab...
Definition linking.cpp:1522
bool needs_renaming_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition linking.cpp:1315
rename_symbolt rename_symbol
linkingt(symbol_table_baset &_main_symbol_table, message_handlert &_message_handler)
std::string type_to_string_verbose(const symbolt &symbol) const
namespacet ns
bool adjust_object_type_rec(const typet &type1, const typet &type2, adjust_type_infot &info)
Definition linking.cpp:877
bool needs_renaming_non_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition linking.cpp:542
void copy_symbols(const symbol_table_baset &, const std::unordered_map< irep_idt, irep_idt > &)
Definition linking.cpp:1456
irep_idt rename(const symbol_table_baset &, const irep_idt &)
Definition linking.cpp:518
void show_struct_diff(const struct_typet &old_type, const struct_typet &new_type)
symbol_table_baset & main_symbol_table
std::string expr_to_string(const irep_idt &identifier, const exprt &expr) const
Definition linking.cpp:114
void link_warning(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition linking.cpp:499
void duplicate_object_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition linking.cpp:1084
casting_replace_symbolt object_type_updates
std::string type_to_string(const irep_idt &identifier, const typet &type) const
Definition linking.cpp:121
std::unordered_set< irep_idt > renamed_ids
bool detailed_conflict_report_rec(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2, unsigned depth, exprt &conflict_path)
Returns true iff the conflict report on a particular branch of the tree of types was a definitive res...
Definition linking.cpp:194
void duplicate_type_symbol(symbolt &old_symbol, const symbolt &new_symbol)
Definition linking.cpp:1220
std::string type_to_string_verbose(const symbolt &symbol, const typet &type) const
Definition linking.cpp:142
void detailed_conflict_report(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2)
bool needs_renaming(const symbolt &old_symbol, const symbolt &new_symbol)
void duplicate_code_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition linking.cpp:556
message_handlert & message_handler
void link_error(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition linking.cpp:481
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Replace a symbol expression by a given expression.
Structure type, corresponds to C style structs.
Definition std_types.h:231
Expression to hold a symbol (variable)
Definition std_expr.h:113
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition std_expr.h:132
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
bool is_type
Definition symbol.h:61
typet type
Type of symbol.
Definition symbol.h:31
The type of an expression, extends irept.
Definition type.h:29
API to expression classes.
adjust_type_infot(const symbolt &_old_symbol, const symbolt &_new_symbol)
std::unordered_set< irep_idt > o_symbols
std::unordered_set< irep_idt > n_symbols
Symbol table entry.