58 for(
auto &arg :
call->arguments())
101 const exprt &e = it->second;
109 static_cast<exprt &
>(s) = e;
116 const exprt &expr)
const
123 const typet &type)
const
144 const typet &type)
const
150 std::string result=
followed.id_string();
158 result +=
" (incomplete)";
166 const typet &subtype =
c.type();
171 if(!
c.get_base_name().empty())
206 log.debug() <<
"<BEGIN DEPTH " << depth <<
">" <<
messaget::eom;
216 msg=
"type classes differ";
238 msg=
"pointer types differ";
240 msg=
"array types differ";
255 msg=
"number of members is different (";
269 msg=
"names of member "+std::to_string(i)+
" differ (";
276 typedef std::unordered_set<typet, irep_hash>
type_sett;
316 " differs (recursive)";
337 msg=
"enum value types are different (";
348 msg=
"number of enum members is different (";
349 msg+=std::to_string(
members1.size())+
'/';
350 msg+=std::to_string(
members2.size())+
')';
355 for(std::size_t i=0; i<
members1.size(); ++i)
359 msg=
"names of member "+std::to_string(i)+
" differ (";
366 msg=
"values of member "+std::to_string(i)+
" differ (";
377 msg+=
"\nenum declarations at\n";
378 msg+=
t1.source_location().as_string()+
" and\n";
379 msg+=
t1.source_location().as_string();
394 msg=
"parameter counts differ (";
417 msg=
"return types differ";
444 msg=
"parameter types differ";
454 msg=
"conflict on POD";
464 log.error() <<
"reason for conflict at "
475 log.debug() <<
"<END DEPTH " << depth <<
">" <<
messaget::eom;
484 const std::string &msg)
487 log.error().source_location = new_symbol.
location;
489 log.error() <<
"error: " << msg <<
" '" << old_symbol.
display_name() <<
"'"
491 log.error() <<
"old definition in module '" << old_symbol.module <<
"' "
494 log.error() <<
"new definition in module '" << new_symbol.module <<
"' "
502 const std::string &msg)
505 log.warning().source_location = new_symbol.
location;
507 log.warning() <<
"warning: " << msg <<
" \"" << old_symbol.
display_name()
509 log.warning() <<
"old definition in module " << old_symbol.module <<
" "
512 log.warning() <<
"new definition in module " << new_symbol.module <<
" "
561 if(old_symbol.
type != new_symbol.
type)
568 link_warning(old_symbol, new_symbol,
"implicit function declaration");
580 "ignoring conflicting implicit function declaration");
583 else if(((
old_t.parameters().empty() &&
old_t.has_ellipsis() &&
585 (
new_t.parameters().empty() &&
new_t.has_ellipsis() &&
588 if(
old_t.parameters().empty() &&
589 old_t.has_ellipsis() &&
604 "function declaration conflicts with with weak definition");
618 "ignoring conflicting weak function declaration");
632 "ignoring conflicting function alias declaration");
641 "ignoring conflicting function declarations");
643 if(
old_t.parameters().size()<
new_t.parameters().size())
651 else if((
old_t.parameters().size()<
new_t.parameters().size() &&
653 !
old_t.has_ellipsis()) ||
654 (
old_t.parameters().size()>
new_t.parameters().size() &&
656 !
new_t.has_ellipsis()))
661 "conflicting parameter counts of function declarations");
672 typedef std::deque<std::pair<typet, typet> >
conflictst;
675 if(
old_t.return_type() !=
new_t.return_type())
677 link_warning(old_symbol, new_symbol,
"conflicting return types");
682 code_typet::parameterst::const_iterator
692 std::make_pair(
o_it->type(),
n_it->type()));
701 "conflicting parameter counts of function declarations");
716 "conflicting parameter counts of function declarations");
737 warn_msg=
"different pointer types in extern function";
748 warn_msg=
"pointer parameter types differ between "
749 "declaration and definition";
780 warn_msg=
"conflict on transparent union parameter in function";
794 warn_msg=
"non-pointer parameter types differ between "
795 "declaration and definition";
815 "conflicting function declarations");
859 else if(old_symbol.
type == new_symbol.
type)
863 log.debug().source_location = new_symbol.
location;
864 log.debug() <<
"function '" << old_symbol.
name <<
"' in module '"
866 <<
"' is shadowed by a definition in module '"
873 "duplicate definition of function");
891 if(
info.o_symbols.insert(identifier).second)
895 info.o_symbols.erase(identifier);
908 if(
info.n_symbols.insert(identifier).second)
912 info.n_symbols.erase(identifier);
921 info.set_to_new=
true;
934 info.set_to_new=
true;
942 info.set_to_new =
true;
960 else if(
t1.id()!=
t2.id())
969 bool s=
info.set_to_new;
975 "conflicting pointer types for variable");
982 "conflicting pointer types for variable");
985 if(
info.old_symbol.is_extern && !
info.new_symbol.is_extern)
987 info.set_to_new =
true;
1003 info.old_symbol.is_weak)
1005 info.set_to_new=
true;
1009 info.new_symbol.is_weak)
1020 "conflicting array sizes for variable");
1033 "conflicting array sizes for variable");
1050 struct_union_typet::componentst::const_iterator
1056 if(
it1->get_name()!=
it2->get_name() ||
1079 set_to_new=
info.set_to_new;
1089 bool set_to_new =
false;
1091 if(old_symbol.
type != new_symbol.
type)
1115 "conflicting types for variable");
1154 log.warning().source_location = new_symbol.
location;
1156 log.warning() <<
"warning: conflicting initializers for"
1157 <<
" variable \"" << old_symbol.
name <<
"\"\n";
1158 log.warning() <<
"using old value in module " << old_symbol.module
1161 log.warning() <<
"ignoring new value in module " << new_symbol.module
1185 old_symbol.
type != new_symbol.
type))
1187 link_error(old_symbol, new_symbol,
"conflict on code contract");
1200 "conflicting definition for symbol");
1231 "conflicting definition for symbol");
1237 if(old_symbol.
type==new_symbol.
type)
1312 "unexpected difference between type symbols");
1324 if(old_symbol.
type==new_symbol.
type)
1381 std::unordered_map<irep_idt, std::unordered_set<irep_idt>>
used_by;
1398 std::deque<irep_idt> queue(
1401 while(!queue.empty())
1406 const std::unordered_set<irep_idt> &
u =
used_by[id];
1408 for(
const auto &
dep :
u)
1411 queue.push_back(
dep);
1414 log.debug() <<
"LINKING: needs to be renamed (dependency): " <<
dep
1443 log.debug() <<
"LINKING: renaming " <<
id <<
" to " <<
new_identifier
1470 symbol.
name = it->second;
1514 !it->second.is_type && !it->second.is_macro &&
1515 it->second.value.is_not_nil())
1537 symbol_table_baset::symbolst::const_iterator
m_it =
1547 log.debug() <<
"LINKING: needs to be renamed: " <<
symbol_pair.first
1572 return linking.link(new_symbol_table);
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::vector< c_enum_membert > memberst
bool replace_symbol_expr(symbol_exprt &dest) const override
bool replace(exprt &dest) const override
std::vector< parametert > parameterst
const typet & return_type() const
A constant literal expression.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
typet & type()
Return the type of the expression.
Unbounded, signed integers (mathematical integers, not bitvectors)
bool get_bool(const irep_idt &name) const
const irep_idt & id() const
std::unordered_map< irep_idt, irep_idt > rename_symbols(const symbol_table_baset &, const std::unordered_set< irep_idt > &needs_to_be_renamed)
void duplicate_non_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
bool adjust_object_type(const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new)
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...
bool needs_renaming_type(const symbolt &old_symbol, const symbolt &new_symbol)
rename_symbolt rename_symbol
bool adjust_object_type_rec(const typet &type1, const typet &type2, adjust_type_infot &info)
bool needs_renaming_non_type(const symbolt &old_symbol, const symbolt &new_symbol)
void copy_symbols(const symbol_table_baset &, const std::unordered_map< irep_idt, irep_idt > &)
irep_idt rename(const symbol_table_baset &, const irep_idt &)
symbol_table_baset & main_symbol_table
std::string expr_to_string(const irep_idt &identifier, const exprt &expr) const
void link_warning(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
void duplicate_object_symbol(symbolt &old_symbol, symbolt &new_symbol)
casting_replace_symbolt object_type_updates
std::string type_to_string(const irep_idt &identifier, const typet &type) const
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...
void duplicate_type_symbol(symbolt &old_symbol, const symbolt &new_symbol)
std::string type_to_string_verbose(const symbolt &symbol, const typet &type) const
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)
message_handlert & message_handler
void link_error(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Extract member of struct or union.
std::size_t get_message_count(unsigned level) const
Class that provides messages with a built-in verbosity 'level'.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
void insert_type(const irep_idt &old_id, const irep_idt &new_id)
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
virtual bool replace(exprt &dest) const
std::size_t erase(const irep_idt &id)
bool have_to_replace(const exprt &dest) const
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
std::vector< componentt > componentst
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
virtual iteratort begin()=0
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual iteratort end()=0
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
const irep_idt & display_name() const
Return language specific display name if present.
exprt value
Initial value of symbol.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
Find identifiers of the sub expressions with id ID_symbol, considering both free and bound variables,...
std::unordered_set< irep_idt > find_symbols_sett
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string type_to_name(const namespacet &ns, const irep_idt &identifier, const typet &type)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
static void do_type_dependencies(const symbol_table_baset &src_symbol_table, std::unordered_set< irep_idt > &needs_to_be_renamed, message_handlert &message_handler)
static const typet & follow_tags_symbols(const namespacet &ns, const typet &type)
bool linking(symbol_table_baset &dest_symbol_table, const symbol_table_baset &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
bool is_true(const literalt &l)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)