cprover
|
#include <linking_class.h>
Classes | |
struct | adjust_type_infot |
Public Member Functions | |
linkingt (symbol_tablet &_main_symbol_table, symbol_tablet &_src_symbol_table, message_handlert &_message_handler) | |
virtual void | typecheck () |
![]() | |
typecheckt (message_handlert &_message_handler) | |
virtual | ~typecheckt () |
void | err_location (const source_locationt &loc) |
void | err_location (const exprt &src) |
void | err_location (const typet &src) |
virtual bool | typecheck_main () |
Public Attributes | |
rename_symbolt | rename_symbol |
replace_symbolt | object_type_updates |
Protected Types | |
typedef std::unordered_set< irep_idt, irep_id_hash > | id_sett |
typedef std::unordered_map< irep_idt, id_sett, irep_id_hash > | used_byt |
Protected Member Functions | |
bool | needs_renaming_type (const symbolt &old_symbol, const symbolt &new_symbol) |
bool | needs_renaming_non_type (const symbolt &old_symbol, const symbolt &new_symbol) |
bool | needs_renaming (const symbolt &old_symbol, const symbolt &new_symbol) |
void | do_type_dependencies (id_sett &) |
void | rename_symbols (const id_sett &needs_to_be_renamed) |
void | copy_symbols () |
void | duplicate_non_type_symbol (symbolt &old_symbol, symbolt &new_symbol) |
void | duplicate_code_symbol (symbolt &old_symbol, symbolt &new_symbol) |
void | duplicate_object_symbol (symbolt &old_symbol, symbolt &new_symbol) |
bool | adjust_object_type (const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new) |
bool | adjust_object_type_rec (const typet &type1, const typet &type2, adjust_type_infot &info) |
void | duplicate_type_symbol (symbolt &old_symbol, symbolt &new_symbol) |
std::string | expr_to_string (const namespacet &ns, const irep_idt &identifier, const exprt &expr) const |
std::string | type_to_string (const namespacet &ns, const irep_idt &identifier, const typet &type) const |
std::string | type_to_string_verbose (const namespacet &ns, const symbolt &symbol, const typet &type) const |
std::string | type_to_string_verbose (const namespacet &ns, const symbolt &symbol) 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) |
void | detailed_conflict_report (const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2) |
void | link_error (const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg) |
void | link_warning (const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg) |
void | show_struct_diff (const struct_typet &old_type, const struct_typet &new_type) |
irep_idt | rename (irep_idt) |
Protected Attributes | |
symbol_tablet & | main_symbol_table |
symbol_tablet & | src_symbol_table |
namespacet | ns |
id_sett | renamed_ids |
Additional Inherited Members |
Definition at line 21 of file linking_class.h.
|
protected |
Definition at line 41 of file linking_class.h.
|
protected |
Definition at line 176 of file linking_class.h.
|
inline |
Definition at line 24 of file linking_class.h.
References typecheck().
|
protected |
Definition at line 901 of file linking.cpp.
References adjust_object_type_rec(), follow_tags_symbols(), ns, messaget::result(), linkingt::adjust_type_infot::set_to_new, and symbolt::type.
Referenced by duplicate_object_symbol(), and needs_renaming().
|
protected |
Definition at line 747 of file linking.cpp.
References base_type_eq(), struct_union_typet::components(), follow_tags_symbols(), irept::get(), irept::id(), irept::is_nil(), irept::is_not_nil(), symbolt::is_weak, exprt::is_zero(), link_error(), link_warning(), linkingt::adjust_type_infot::n_symbols, linkingt::adjust_type_infot::new_symbol, ns, linkingt::adjust_type_infot::o_symbols, linkingt::adjust_type_infot::old_symbol, messaget::result(), linkingt::adjust_type_infot::set_to_new, simplify_expr(), array_typet::size(), typet::subtype(), to_array_type(), and to_struct_union_type().
Referenced by adjust_object_type().
|
protected |
Definition at line 1239 of file linking.cpp.
References symbol_tablet::add(), duplicate_non_type_symbol(), duplicate_type_symbol(), Forall_symbols, symbolt::is_type, main_symbol_table, object_type_updates, rename_symbol, src_symbol_table, and symbol_tablet::symbols.
Referenced by needs_renaming(), and typecheck().
|
inlineprotected |
Definition at line 140 of file linking_class.h.
References detailed_conflict_report_rec(), link_error(), link_warning(), and show_struct_diff().
Referenced by duplicate_code_symbol(), duplicate_object_symbol(), and duplicate_type_symbol().
|
protected |
Definition at line 115 of file linking.cpp.
References source_locationt::as_string(), base_type_eq(), struct_union_typet::components(), messaget::debug(), messaget::eom(), messaget::error(), expr_to_string(), follow_tags_symbols(), get_base_name(), irept::id(), id2string(), c_enum_typet::members(), symbolt::name, ns, exprt::op0(), code_typet::parameters(), code_typet::return_type(), typet::source_location(), typet::subtype(), to_c_enum_type(), to_code_type(), to_struct_union_type(), exprt::type(), type_to_string(), and type_to_string_verbose().
Referenced by detailed_conflict_report(), and type_to_string_verbose().
|
protected |
Definition at line 1152 of file linking.cpp.
References messaget::debug(), messaget::eom(), find_type_and_expr_symbols(), forall_symbols, languaget::id(), src_symbol_table, and symbol_tablet::symbols.
Referenced by needs_renaming(), and typecheck().
Definition at line 445 of file linking.cpp.
References base_type_eq(), struct_union_typet::components(), detailed_conflict_report(), dstringt::empty(), messaget::eom(), follow_tags_symbols(), irept::get_bool(), source_locationt::get_function(), code_typet::get_inlined(), code_typet::has_ellipsis(), irept::id(), symbolt::is_macro, irept::is_nil(), irept::is_not_nil(), symbolt::is_weak, link_error(), link_warning(), symbolt::location, irept::make_nil(), symbolt::module, symbolt::name, ns, code_typet::parameters(), pointer_offset_bits(), rename_symbol, code_typet::return_type(), messaget::mstreamt::source_location, to_code_type(), to_union_type(), symbolt::type, symbolt::value, and messaget::warning().
Referenced by duplicate_non_type_symbol(), and needs_renaming().
Definition at line 1002 of file linking.cpp.
References duplicate_code_symbol(), duplicate_object_symbol(), irept::id(), symbolt::is_extern, link_error(), symbolt::location, and symbolt::type.
Referenced by copy_symbols(), and needs_renaming().
Definition at line 916 of file linking.cpp.
References adjust_object_type(), base_type_eq(), detailed_conflict_report(), messaget::eom(), expr_to_string(), exprt::find_source_location(), follow_tags_symbols(), irept::get_bool(), irept::id(), replace_symbolt::insert(), symbolt::is_macro, irept::is_nil(), symbolt::is_weak, link_error(), symbolt::location, symbolt::module, symbolt::name, ns, object_type_updates, simplify(), messaget::mstreamt::source_location, symbolt::symbol_expr(), symbolt::type, symbolt::value, and messaget::warning().
Referenced by duplicate_non_type_symbol(), and needs_renaming().
Definition at line 1031 of file linking.cpp.
References base_type_eq(), detailed_conflict_report(), irept::id(), irept::is_nil(), irept::is_not_nil(), symbolt::is_type, link_error(), symbolt::location, ns, array_typet::size(), typet::subtype(), to_array_type(), and symbolt::type.
Referenced by copy_symbols().
|
protected |
Definition at line 29 of file linking.cpp.
References from_expr().
Referenced by detailed_conflict_report_rec(), and duplicate_object_symbol().
|
protected |
Definition at line 369 of file linking.cpp.
References symbolt::display_name(), messaget::eom(), messaget::error(), symbolt::location, symbolt::module, ns, messaget::mstreamt::source_location, and type_to_string_verbose().
Referenced by adjust_object_type_rec(), detailed_conflict_report(), duplicate_code_symbol(), duplicate_non_type_symbol(), duplicate_object_symbol(), and duplicate_type_symbol().
|
protected |
Definition at line 389 of file linking.cpp.
References symbolt::display_name(), messaget::eom(), symbolt::location, symbolt::module, ns, messaget::mstreamt::source_location, type_to_string_verbose(), and messaget::warning().
Referenced by adjust_object_type_rec(), detailed_conflict_report(), and duplicate_code_symbol().
|
inlineprotected |
Definition at line 51 of file linking_class.h.
References adjust_object_type(), copy_symbols(), do_type_dependencies(), duplicate_code_symbol(), duplicate_non_type_symbol(), duplicate_object_symbol(), symbolt::is_type, needs_renaming_non_type(), needs_renaming_type(), and rename_symbols().
Referenced by typecheck().
|
protected |
Definition at line 431 of file linking.cpp.
References symbolt::is_file_local.
Referenced by needs_renaming().
|
protected |
Definition at line 1108 of file linking.cpp.
References base_type_eq(), irept::id(), irept::is_nil(), irept::is_not_nil(), symbolt::is_type, ns, array_typet::size(), typet::subtype(), to_array_type(), and symbolt::type.
Referenced by needs_renaming().
Definition at line 407 of file linking.cpp.
References id2string(), main_symbol_table, renamed_ids, src_symbol_table, and symbol_tablet::symbols.
Referenced by rename_symbols().
|
protected |
Definition at line 1207 of file linking.cpp.
References messaget::debug(), messaget::eom(), rename_symbolt::insert_expr(), rename_symbolt::insert_type(), symbolt::is_type, symbolt::name, rename(), rename_symbol, src_symbol_table, symbol_tablet::symbols, symbolt::type, and type_to_name().
Referenced by needs_renaming(), and typecheck().
|
protected |
Referenced by detailed_conflict_report().
|
protected |
Definition at line 37 of file linking.cpp.
References from_type().
Referenced by detailed_conflict_report_rec(), and type_to_string_verbose().
|
protected |
Definition at line 61 of file linking.cpp.
References struct_union_typet::components(), follow_tags_symbols(), irept::get_string(), irept::id(), id2string(), irept::id_string(), symbolt::name, messaget::result(), typet::subtype(), to_struct_union_type(), and type_to_string().
Referenced by detailed_conflict_report_rec(), link_error(), link_warning(), and type_to_string_verbose().
|
inlineprotected |
Definition at line 125 of file linking_class.h.
References detailed_conflict_report_rec(), symbolt::type, and type_to_string_verbose().
|
virtual |
Implements typecheckt.
Definition at line 1300 of file linking.cpp.
References copy_symbols(), messaget::debug(), do_type_dependencies(), messaget::eom(), forall_symbols, main_symbol_table, needs_renaming(), rename_symbols(), src_symbol_table, and symbol_tablet::symbols.
Referenced by linkingt().
|
protected |
Definition at line 170 of file linking_class.h.
Referenced by copy_symbols(), rename(), and typecheck().
|
protected |
Definition at line 173 of file linking_class.h.
Referenced by adjust_object_type(), adjust_object_type_rec(), detailed_conflict_report_rec(), duplicate_code_symbol(), duplicate_object_symbol(), duplicate_type_symbol(), link_error(), link_warning(), and needs_renaming_type().
replace_symbolt linkingt::object_type_updates |
Definition at line 38 of file linking_class.h.
Referenced by copy_symbols(), duplicate_object_symbol(), and read_object_and_link().
rename_symbolt linkingt::rename_symbol |
Definition at line 37 of file linking_class.h.
Referenced by copy_symbols(), duplicate_code_symbol(), read_object_and_link(), and rename_symbols().
|
protected |
Definition at line 181 of file linking_class.h.
Referenced by rename().
|
protected |
Definition at line 171 of file linking_class.h.
Referenced by copy_symbols(), do_type_dependencies(), rename(), rename_symbols(), and typecheck().