From 7f651e1172614ca8d9afaf5db3c9178117db78c6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 17 Feb 2016 23:45:22 +0000 Subject: [PATCH 1/4] Detailed linking conflict report in case of enums --- src/linking/linking.cpp | 83 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 78 insertions(+), 5 deletions(-) diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index acce135258b..724ae91b8b7 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -64,6 +64,34 @@ std::string linkingt::type_to_string( /*******************************************************************\ +Function: follow_tags_symbols + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static const typet &follow_tags_symbols( + const namespacet &ns, + const typet &type) +{ + if(type.id()==ID_symbol) + return ns.follow(type); + else if(type.id()==ID_c_enum_tag) + return ns.follow_tag(to_c_enum_tag_type(type)); + else if(type.id()==ID_struct_tag) + return ns.follow_tag(to_struct_tag_type(type)); + else if(type.id()==ID_union_tag) + return ns.follow_tag(to_union_tag_type(type)); + else + return type; +} + +/*******************************************************************\ + Function: linkingt::type_to_string_verbose Inputs: @@ -79,7 +107,7 @@ std::string linkingt::type_to_string_verbose( const symbolt &symbol, const typet &type) const { - const typet &followed=ns.follow(type); + const typet &followed=follow_tags_symbols(ns, type); if(followed.id()==ID_struct || followed.id()==ID_union) { @@ -154,8 +182,8 @@ void linkingt::detailed_conflict_report_rec( std::string msg; - const typet &t1=ns.follow(type1); - const typet &t2=ns.follow(type2); + const typet &t1=follow_tags_symbols(ns, type1); + const typet &t2=follow_tags_symbols(ns, type2); if(t1.id()!=t2.id()) msg="type classes differ"; @@ -231,6 +259,49 @@ void linkingt::detailed_conflict_report_rec( } } } + else if(t1.id()==ID_c_enum) + { + const c_enum_typet::memberst &members1= + to_c_enum_type(t1).members(); + + const c_enum_typet::memberst &members2= + to_c_enum_type(t2).members(); + + if(t1.subtype()!=t2.subtype()) + { + msg="enum value types are different ("; + msg+=type_to_string(ns, old_symbol.name, t1.subtype())+'/'; + msg+=type_to_string(ns, new_symbol.name, t2.subtype())+')'; + } + else if(members1.size()!=members2.size()) + { + msg="number of enum members is different ("; + msg+=i2string(members1.size())+'/'; + msg+=i2string(members2.size())+')'; + } + else + for(std::size_t i=0; i Date: Wed, 24 Feb 2016 00:25:02 +0000 Subject: [PATCH 2/4] Linking cleanup --- src/goto-cc/compile.cpp | 1 - src/linking/linking.cpp | 12 ++++++------ src/util/message_stream.h | 7 +++++++ 3 files changed, 13 insertions(+), 7 deletions(-) diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index d3824591933..c27ffb18c71 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -25,7 +25,6 @@ Date: June 2006 #include -#include #include #include diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 724ae91b8b7..66f27847c67 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -177,7 +177,7 @@ void linkingt::detailed_conflict_report_rec( { #ifdef DEBUG str << ""; - debug(); + debug_msg(); #endif std::string msg; @@ -380,7 +380,7 @@ void linkingt::detailed_conflict_report_rec( #ifdef DEBUG str << ""; - debug(); + debug_msg(); #endif } @@ -1113,8 +1113,8 @@ void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed) { queue.push(*d_it); #ifdef DEBUG - str << "LINKING: needs to be renamed (dependency): " << s_it->first; - debug(); + str << "LINKING: needs to be renamed (dependency): " << *d_it; + debug_msg(); #endif } } @@ -1147,7 +1147,7 @@ void linkingt::rename_symbols(const id_sett &needs_to_be_renamed) #ifdef DEBUG str << "LINKING: renaming " << *it << " to " << new_identifier; - debug(); + debug_msg(); #endif if(new_symbol.is_type) @@ -1255,7 +1255,7 @@ void linkingt::typecheck() needs_to_be_renamed.insert(s_it->first); #ifdef DEBUG str << "LINKING: needs to be renamed: " << s_it->first; - debug(); + debug_msg(); #endif } } diff --git a/src/util/message_stream.h b/src/util/message_stream.h index 4b451d19785..9c6c3e4216c 100644 --- a/src/util/message_stream.h +++ b/src/util/message_stream.h @@ -86,6 +86,13 @@ class message_streamt:public message_clientt sequence_number++; } + void debug_msg() + { + send_msg(9, str.str()); + clear_err(); + sequence_number++; + } + std::ostringstream str; bool get_error_found() const From c56ae13f92659fab2be40decd48af49e06677d42 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 24 Feb 2016 00:25:43 +0000 Subject: [PATCH 3/4] Rename types to their canonical name --- src/linking/linking.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 66f27847c67..26b2590c26d 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -1134,6 +1134,8 @@ Function: linkingt::rename_symbols void linkingt::rename_symbols(const id_sett &needs_to_be_renamed) { + namespacet src_ns(src_symbol_table); + for(id_sett::const_iterator it=needs_to_be_renamed.begin(); it!=needs_to_be_renamed.end(); @@ -1141,7 +1143,13 @@ void linkingt::rename_symbols(const id_sett &needs_to_be_renamed) { symbolt &new_symbol=src_symbol_table.symbols[*it]; - irep_idt new_identifier=rename(*it); + irep_idt new_identifier; + + if(new_symbol.is_type) + new_identifier=type_to_name(src_ns, *it, new_symbol.type); + else + new_identifier=rename(*it); + new_symbol.name=new_identifier; #ifdef DEBUG From e0516ba2d768f87445e9d916d779a5e1e85c8f47 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Mar 2016 09:05:47 +0000 Subject: [PATCH 4/4] Follow all tags (and symbol types), better warning message --- src/linking/linking.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 26b2590c26d..58a73fb6c91 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -598,8 +598,8 @@ void linkingt::duplicate_code_symbol( while(!conflicts.empty()) { - const typet &t1=ns.follow(conflicts.front().first); - const typet &t2=ns.follow(conflicts.front().second); + const typet &t1=follow_tags_symbols(ns, conflicts.front().first); + const typet &t2=follow_tags_symbols(ns, conflicts.front().second); // void vs. non-void return type may be acceptable if the // return value is never used @@ -626,7 +626,8 @@ void linkingt::duplicate_code_symbol( old_symbol.value.is_nil()!=new_symbol.value.is_nil()) { if(warn_msg.empty()) - warn_msg="different pointer types in function"; + warn_msg="pointer parameter types differ between " + "declaration and definition"; replace=new_symbol.value.is_not_nil(); } // transparent union with (or entirely without) implementation is @@ -812,7 +813,7 @@ void linkingt::duplicate_object_symbol( if(old_type.id()==ID_struct || old_type.id()==ID_union || old_type.id()==ID_array || - old_type.id()==ID_c_enum_tag) + old_type.id()==ID_c_enum) detailed_conflict_report( old_symbol, new_symbol,