16 #include <unordered_set> 30 const exprt &expr)
const 38 const typet &type)
const 47 if(type.
id()==ID_symbol)
49 else if(type.
id()==ID_c_enum_tag)
51 else if(type.
id()==ID_struct_tag)
53 else if(type.
id()==ID_union_tag)
62 const typet &type)
const 66 if(followed.
id()==ID_struct || followed.
id()==ID_union)
70 const std::string &tag=followed.
get_string(ID_tag);
78 for(struct_union_typet::componentst::const_iterator
79 it=components.begin();
83 const typet &subtype=it->type();
88 if(it->get_base_name()!=
"")
100 else if(followed.
id()==ID_pointer)
104 else if(followed.
id()==ID_incomplete_struct ||
105 followed.
id()==ID_incomplete_union)
119 exprt &conflict_path)
122 debug() <<
"<BEGIN DEPTH " << depth <<
">" <<
eom;
131 msg=
"type classes differ";
132 else if(t1.
id()==ID_pointer ||
148 else if(t1.
id()==ID_pointer)
149 msg=
"pointer types differ";
151 msg=
"array types differ";
153 else if(t1.
id()==ID_struct ||
162 exprt conflict_path_before=conflict_path;
164 if(components1.size()!=components2.size())
166 msg=
"number of members is different (";
172 for(std::size_t i=0; i<components1.size(); ++i)
174 const typet &subtype1=components1[i].type();
175 const typet &subtype2=components2[i].type();
177 if(components1[i].get_name()!=components2[i].get_name())
180 msg+=
id2string(components1[i].get_name())+
'/';
181 msg+=
id2string(components2[i].get_name())+
')';
186 typedef std::unordered_set<typet, irep_hash> type_sett;
187 type_sett parent_types;
189 exprt e=conflict_path_before;
190 while(e.
id()==ID_dereference ||
194 parent_types.insert(e.
type());
198 conflict_path=conflict_path_before;
199 conflict_path.
type()=t1;
204 parent_types.find(t1)==parent_types.end())
214 msg=
"type of member "+
233 if(parent_types.find(t1)==parent_types.end())
239 else if(t1.
id()==ID_c_enum)
249 msg=
"enum value types are different (";
253 else if(members1.size()!=members2.size())
255 msg=
"number of enum members is different (";
261 for(std::size_t i=0; i<members1.size(); ++i)
270 else if(members1[i].get_value()!=members2[i].get_value())
273 msg+=
id2string(members1[i].get_value())+
'/';
274 msg+=
id2string(members2[i].get_value())+
')';
280 msg+=
"\nenum declarations at\n";
284 else if(t1.
id()==ID_code)
295 if(parameters1.size()!=parameters2.size())
297 msg=
"parameter counts differ (";
316 msg=
"return types differ";
320 for(std::size_t i=0; i<parameters1.size(); i++)
322 const typet &subtype1=parameters1[i].type();
323 const typet &subtype2=parameters2[i].type();
340 msg=
"parameter types differ";
348 msg=
"conflict on POD";
353 error() <<
"reason for conflict at " 355 <<
": " << msg <<
'\n';
363 debug() <<
"<END DEPTH " << depth <<
">" <<
eom;
370 const std::string &msg)
374 error() <<
"error: " << msg <<
" `" 377 error() <<
"old definition in module `" << old_symbol.
module 378 <<
"' " << old_symbol.
location <<
'\n' 380 error() <<
"new definition in module `" << new_symbol.
module 381 <<
"' " << new_symbol.
location <<
'\n' 388 const std::string &msg)
392 warning() <<
"warning: " << msg <<
" \"" 395 warning() <<
"old definition in module " << old_symbol.
module 396 <<
" " << old_symbol.
location <<
'\n' 398 warning() <<
"new definition in module " << new_symbol.
module 399 <<
" " << new_symbol.
location <<
'\n' 423 return new_identifier;
462 "implicit function declaration");
467 "implicit function declaration");
480 "ignoring conflicting implicit function declaration");
485 "implicit function declaration");
512 "function declaration conflicts with with weak definition");
526 "ignoring conflicting weak function declaration");
540 "ignoring conflicting function alias declaration");
551 "ignoring conflicting function declarations");
571 "conflicting parameter counts of function declarations");
580 std::string warn_msg;
582 typedef std::deque<std::pair<typet, typet> > conflictst;
583 conflictst conflicts;
589 code_typet::parameterst::const_iterator
599 std::make_pair(o_it->type(), n_it->type()));
608 "conflicting parameter counts of function declarations");
623 "conflicting parameter counts of function declarations");
632 while(!conflicts.empty())
639 if((t1.
id()==ID_empty || t2.id()==ID_empty) &&
643 warn_msg=
"void/non-void return type conflict on function";
649 else if((t1.
id()==ID_pointer || t2.id()==ID_pointer) &&
654 warn_msg=
"different pointer types in extern function";
659 else if((t1.
id()==ID_pointer || t2.id()==ID_pointer) &&
664 warn_msg=
"pointer parameter types differ between " 665 "declaration and definition";
671 else if((t1.
id()==ID_union &&
672 (t1.
get_bool(ID_C_transparent_union) ||
673 conflicts.front().first.get_bool(ID_C_transparent_union))) ||
674 (t2.id()==ID_union &&
675 (t2.get_bool(ID_C_transparent_union) ||
676 conflicts.front().second.get_bool(ID_C_transparent_union))))
680 (t1.
get_bool(ID_C_transparent_union) ||
681 conflicts.front().first.get_bool(ID_C_transparent_union)) &&
686 const typet &src_type=t1.
id()==ID_union?t2:t1;
689 for(union_typet::componentst::const_iterator
697 warn_msg=
"conflict on transparent union parameter in function";
707 conflicts.pop_front();
710 if(!conflicts.empty())
715 conflicts.front().first,
716 conflicts.front().second);
721 "conflicting function declarations");
762 warning() <<
"function `" << old_symbol.
name <<
"' in module `" 763 << new_symbol.
module <<
"' is shadowed by a definition in module `" 770 "duplicate definition of function");
782 if(t1.
id()==ID_symbol ||
783 t1.
id()==ID_struct_tag ||
784 t1.
id()==ID_union_tag ||
785 t1.
id()==ID_c_enum_tag)
789 if(info.
o_symbols.insert(identifier).second)
800 else if(t2.
id()==ID_symbol ||
801 t2.
id()==ID_struct_tag ||
802 t2.
id()==ID_union_tag ||
803 t2.
id()==ID_c_enum_tag)
807 if(info.
n_symbols.insert(identifier).second)
818 else if(t1.
id()==ID_pointer && t2.
id()==ID_array)
824 else if(t1.
id()==ID_array && t2.
id()==ID_pointer)
829 else if((t1.
id()==ID_incomplete_struct && t2.
id()==ID_struct) ||
830 (t1.
id()==ID_incomplete_union && t2.
id()==ID_union))
836 else if((t1.
id()==ID_struct && t2.
id()==ID_incomplete_struct) ||
837 (t1.
id()==ID_union && t2.
id()==ID_incomplete_union))
842 else if(t1.
id()!=t2.
id())
848 if(t1.
id()==ID_pointer)
857 "conflicting pointer types for variable");
864 "conflicting pointer types for variable");
869 else if(t1.
id()==ID_array &&
882 else if(new_size.
is_nil() ||
897 "conflicting array sizes for variable");
906 else if(t1.
id()==ID_struct || t1.
id()==ID_union)
914 struct_union_typet::componentst::const_iterator
915 it1=components1.begin(), it2=components2.begin();
917 it1!=components1.end() && it2!=components2.end();
920 if(it1->get_name()!=it2->get_name() ||
924 if(it1!=components1.end() || it2!=components2.end())
956 bool set_to_new=
false;
966 if(old_type.
id()==ID_struct ||
967 old_type.
id()==ID_union ||
968 old_type.
id()==ID_array ||
969 old_type.
id()==ID_c_enum)
979 "conflicting types for variable");
1007 tmp_new=new_symbol.
value;
1020 warning() <<
"warning: conflicting initializers for" 1021 <<
" variable \"" << old_symbol.
name <<
"\"\n";
1022 warning() <<
"using old value in module " 1023 << old_symbol.
module <<
" " 1027 warning() <<
"ignoring new value in module " 1028 << new_symbol.
module <<
" " 1043 bool is_code_old_symbol=old_symbol.
type.
id()==ID_code;
1044 bool is_code_new_symbol=new_symbol.
type.
id()==ID_code;
1046 if(is_code_old_symbol!=is_code_new_symbol)
1051 "conflicting definition for symbol");
1057 if(is_code_old_symbol)
1082 "conflicting definition for symbol");
1088 if(old_symbol.
type==new_symbol.
type)
1091 if(old_symbol.
type.
id()==ID_incomplete_struct &&
1092 new_symbol.
type.
id()==ID_struct)
1099 if(old_symbol.
type.
id()==ID_struct &&
1100 new_symbol.
type.
id()==ID_incomplete_struct)
1106 if(old_symbol.
type.
id()==ID_incomplete_union &&
1107 new_symbol.
type.
id()==ID_union)
1114 if(old_symbol.
type.
id()==ID_union &&
1115 new_symbol.
type.
id()==ID_incomplete_union)
1121 if(old_symbol.
type.
id()==ID_array &&
1122 new_symbol.
type.
id()==ID_array &&
1150 "unexpected difference between type symbols");
1162 if(old_symbol.
type==new_symbol.
type)
1165 if(old_symbol.
type.
id()==ID_incomplete_struct &&
1166 new_symbol.
type.
id()==ID_struct)
1169 if(old_symbol.
type.
id()==ID_struct &&
1170 new_symbol.
type.
id()==ID_incomplete_struct)
1173 if(old_symbol.
type.
id()==ID_incomplete_union &&
1174 new_symbol.
type.
id()==ID_union)
1177 if(old_symbol.
type.
id()==ID_union &&
1178 new_symbol.
type.
id()==ID_incomplete_union)
1181 if(old_symbol.
type.
id()==ID_array &&
1182 new_symbol.
type.
id()==ID_array &&
1198 std::unordered_set<irep_idt> &needs_to_be_renamed)
1207 if(symbol_pair.second.is_type)
1213 for(
const auto &symbol_used : symbols_used)
1215 used_by[symbol_used].insert(symbol_pair.first);
1220 std::deque<irep_idt> queue(
1221 needs_to_be_renamed.begin(), needs_to_be_renamed.end());
1223 while(!queue.empty())
1228 const std::unordered_set<irep_idt> &u = used_by[id];
1230 for(
const auto &dep : u)
1231 if(needs_to_be_renamed.insert(dep).second)
1233 queue.push_back(dep);
1235 debug() <<
"LINKING: needs to be renamed (dependency): " 1243 const std::unordered_set<irep_idt> &needs_to_be_renamed)
1247 for(
const irep_idt &
id : needs_to_be_renamed)
1256 new_identifier=
rename(
id);
1258 new_symbol.
name=new_identifier;
1261 debug() <<
"LINKING: renaming " <<
id <<
" to " 1262 << new_identifier <<
eom;
1274 std::map<irep_idt, symbolt> src_symbols;
1278 symbolt symbol=named_symbol.second;
1283 src_symbols.emplace(named_symbol.first, std::move(symbol));
1287 std::unordered_set<irep_idt> collisions;
1289 for(
const auto &named_symbol : src_symbols)
1292 if(named_symbol.first!=named_symbol.second.name)
1305 collisions.insert(named_symbol.first);
1310 for(
const irep_idt &collision : collisions)
1313 symbolt &new_symbol=src_symbols.at(collision);
1324 if(!named_symbol.second.is_type &&
1325 !named_symbol.second.is_macro &&
1326 named_symbol.second.value.is_not_nil())
1342 std::unordered_set<irep_idt> needs_to_be_renamed;
1346 symbol_tablet::symbolst::const_iterator m_it =
1353 needs_to_be_renamed.insert(symbol_pair.first);
1355 debug() <<
"LINKING: needs to be renamed: " << symbol_pair.first <<
eom;
1378 return linking.typecheck_main();
void do_type_dependencies(std::unordered_set< irep_idt > &)
The type of an expression.
irep_idt name
The unique identifier.
bool is_true(const literalt &l)
const std::string & id2string(const irep_idt &d)
void link_error(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
exprt simplify_expr(const exprt &src, const namespacet &ns)
void detailed_conflict_report(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
bool has_ellipsis() const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void insert_type(const irep_idt &old_id, const irep_idt &new_id)
const irep_idt & get_function() const
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
std::string as_string() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< componentt > componentst
std::vector< parametert > parameterst
exprt value
Initial value of symbol.
const componentst & components() const
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
const memberst & members() const
irep_idt module
Name of module the symbol belongs to.
symbol_tablet & main_symbol_table
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
void link_warning(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
std::string expr_to_string(const namespacet &ns, const irep_idt &identifier, const exprt &expr) const
A constant literal expression.
static mstreamt & eom(mstreamt &m)
bool get_bool(const irep_namet &name) const
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
const typet & follow_tag(const union_tag_typet &) const
void detailed_conflict_report_rec(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2, unsigned depth, exprt &conflict_path)
bool needs_renaming_non_type(const symbolt &old_symbol, const symbolt &new_symbol)
Extract member of struct or union.
mstreamt & warning() const
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
const symbolt & new_symbol
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > used_byt
std::unordered_set< irep_idt > n_symbols
const irep_idt & id() const
bool needs_renaming(const symbolt &old_symbol, const symbolt &new_symbol)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
std::string type_to_name(const namespacet &ns, const irep_idt &identifier, const typet &type)
const source_locationt & find_source_location() const
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
source_locationt source_location
std::unordered_set< irep_idt > renamed_ids
Operator to dereference a pointer.
const irep_idt & get(const irep_namet &name) const
const symbolt & old_symbol
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
const exprt & size() const
const typet & follow(const typet &) const
bool needs_renaming_type(const symbolt &old_symbol, const symbolt &new_symbol)
irep_idt rename(irep_idt)
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
std::string type_to_string(const namespacet &ns, const irep_idt &identifier, const typet &type) const
static const typet & follow_tags_symbols(const namespacet &ns, const typet &type)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
replace_symbolt object_type_updates
void duplicate_code_symbol(symbolt &old_symbol, symbolt &new_symbol)
const source_locationt & source_location() const
const irep_idt & display_name() const
bool adjust_object_type_rec(const typet &type1, const typet &type2, adjust_type_infot &info)
Unbounded, signed integers.
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
mstreamt & result() const
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
symbol_tablet & src_symbol_table
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
void duplicate_non_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
const parameterst & parameters() const
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
rename_symbolt rename_symbol
void duplicate_object_symbol(symbolt &old_symbol, symbolt &new_symbol)
const std::string & get_string(const irep_namet &name) const
const std::string & id_string() const
void insert(const irep_idt &identifier, const exprt &expr)
std::string type_to_string_verbose(const namespacet &ns, const symbolt &symbol, const typet &type) const
bool adjust_object_type(const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new)
Expression to hold a symbol (variable)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
goto_programt coverage_criteriont message_handlert & message_handler
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
std::unordered_set< irep_idt > find_symbols_sett
std::unordered_set< irep_idt > o_symbols
const typet & subtype() const
void rename_symbols(const std::unordered_set< irep_idt > &needs_to_be_renamed)
std::vector< c_enum_membert > memberst
const typet & return_type() const
void duplicate_type_symbol(symbolt &old_symbol, const symbolt &new_symbol)
bool simplify(exprt &expr, const namespacet &ns)