diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index fc25290079a..47dfd3e03d3 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -72,7 +72,7 @@ void record_function_outputs( codet output(ID_output); output.operands().resize(2); - const symbolt &return_symbol=symbol_table.lookup("return'"); + const symbolt &return_symbol=*symbol_table.lookup("return'"); output.op0()= address_of_exprt( @@ -212,7 +212,7 @@ bool generate_ansi_c_start_function( // build call to initialization function { - symbol_tablet::symbolst::iterator init_it= + symbol_tablet::symbolst::const_iterator init_it= symbol_table.symbols.find(INITIALIZE_FUNCTION); if(init_it==symbol_table.symbols.end()) @@ -478,11 +478,11 @@ bool generate_ansi_c_start_function( new_symbol.value.swap(init_code); new_symbol.mode=symbol.mode; - if(symbol_table.move(new_symbol)) + if(!symbol_table.insert(std::move(new_symbol)).second) { messaget message; message.set_message_handler(message_handler); - message.error() << "failed to move main symbol" << messaget::eom; + message.error() << "failed to insert main symbol" << messaget::eom; return true; } diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index b0a8f1734c3..1d213aa8f0a 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -100,7 +100,7 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol) } // see if we have it already - symbol_tablet::symbolst::iterator old_it= + symbol_tablet::symbolst::const_iterator old_it= symbol_table.symbols.find(symbol.name); if(old_it==symbol_table.symbols.end()) @@ -121,10 +121,11 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol) throw 0; } + symbolt & existing_symbol=*symbol_table.get_writeable(symbol.name); if(symbol.is_type) - typecheck_redefinition_type(old_it->second, symbol); + typecheck_redefinition_type(existing_symbol, symbol); else - typecheck_redefinition_non_type(old_it->second, symbol); + typecheck_redefinition_non_type(existing_symbol, symbol); } } @@ -350,10 +351,10 @@ void c_typecheck_baset::typecheck_redefinition_non_type( { const irep_idt &identifier=p_it->get_identifier(); - symbol_tablet::symbolst::iterator p_s_it= + symbol_tablet::symbolst::const_iterator p_s_it= symbol_table.symbols.find(identifier); if(p_s_it!=symbol_table.symbols.end()) - symbol_table.symbols.erase(p_s_it); + symbol_table.erase(p_s_it); } } else @@ -732,10 +733,7 @@ void c_typecheck_baset::typecheck_declaration( // add code contract (if any); we typecheck this after the // function body done above, so as to have parameter symbols // available - symbol_tablet::symbolst::iterator s_it= - symbol_table.symbols.find(identifier); - assert(s_it!=symbol_table.symbols.end()); - symbolt &new_symbol=s_it->second; + symbolt &new_symbol=*symbol_table.get_writeable(identifier); typecheck_spec_expr(contract, ID_C_spec_requires); diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index a45420839a4..5529ab6213b 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -287,7 +287,7 @@ void c_typecheck_baset::typecheck_decl(codet &code) irep_idt identifier=d_it->get_name(); // look it up - symbol_tablet::symbolst::iterator s_it= + symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find(identifier); if(s_it==symbol_table.symbols.end()) @@ -298,7 +298,7 @@ void c_typecheck_baset::typecheck_decl(codet &code) throw 0; } - symbolt &symbol=s_it->second; + const symbolt &symbol=s_it->second; // This must not be an incomplete type, unless it's 'extern' // or a typedef. diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index c41a2240309..00d68f46c35 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -485,7 +485,7 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr) symbol.name=ID_gcc_builtin_va_arg; symbol.type=symbol_type; - symbol_table.move(symbol); + symbol_table.insert(std::move(symbol)); } void c_typecheck_baset::typecheck_expr_cw_va_arg_typeof(exprt &expr) @@ -704,7 +704,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr) declaration.declarators().front().get_name(); // look it up - symbol_tablet::symbolst::iterator s_it= + symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find(identifier); if(s_it==symbol_table.symbols.end()) @@ -715,7 +715,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr) throw 0; } - symbolt &symbol=s_it->second; + const symbolt &symbol=s_it->second; if(symbol.is_type || symbol.is_extern || symbol.is_static_lifetime || !is_complete_type(symbol.type) || symbol.type.id()==ID_code) diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index a047108d1b0..1cc2ac95cc0 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -208,12 +208,7 @@ void c_typecheck_baset::typecheck_type(typet &type) { const irep_idt &tag_name= to_c_enum_tag_type(type.subtype()).get_identifier(); - - symbol_tablet::symbolst::iterator entry= - symbol_table.symbols.find(tag_name); - assert(entry!=symbol_table.symbols.end()); - - entry->second.type.subtype()=result; + symbol_table.get_writeable(tag_name)->get().type.subtype()=result; } type=result; @@ -736,7 +731,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) identifier=type.find(ID_tag).get(ID_identifier); // does it exist already? - symbol_tablet::symbolst::iterator s_it= + symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find(identifier); if(s_it==symbol_table.symbols.end()) @@ -787,7 +782,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) type.set(ID_tag, base_name); typecheck_compound_body(type); - s_it->second.type.swap(type); + symbol_table.get_writeable(s_it->first)->get().type.swap(type); } } else if(have_body) @@ -1213,19 +1208,19 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type) enum_tag_symbol.type.subtype()=underlying_type; // is it in the symbol table already? - symbol_tablet::symbolst::iterator s_it= + symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find(identifier); if(s_it!=symbol_table.symbols.end()) { // Yes. - symbolt &symbol=s_it->second; + const symbolt &symbol=s_it->second; if(symbol.type.id()==ID_incomplete_c_enum) { // Ok, overwrite the type in the symbol table. // This gives us the members and the subtype. - symbol.type=enum_tag_symbol.type; + symbol_table.get_writeable(symbol.name)->get().type=enum_tag_symbol.type; } else if(symbol.type.id()==ID_c_enum) { diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index 2ea5732f436..bdc977eff6f 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -98,10 +98,10 @@ symbolt &cpp_declarator_convertert::convert( } // try static first - symbol_tablet::symbolst::iterator c_it= - cpp_typecheck.symbol_table.symbols.find(final_identifier); + symbol_tablet::opt_symbol_reft maybe_symbol= + cpp_typecheck.symbol_table.get_writeable(final_identifier); - if(c_it==cpp_typecheck.symbol_table.symbols.end()) + if(!maybe_symbol) { // adjust type if it's a non-static member function if(final_type.id()==ID_code) @@ -111,9 +111,8 @@ symbolt &cpp_declarator_convertert::convert( get_final_identifier(); // try again - c_it=cpp_typecheck.symbol_table.symbols.find(final_identifier); - - if(c_it==cpp_typecheck.symbol_table.symbols.end()) + maybe_symbol=cpp_typecheck.symbol_table.get_writeable(final_identifier); + if(!maybe_symbol) { cpp_typecheck.error().source_location= declarator.name().source_location(); @@ -125,9 +124,7 @@ symbolt &cpp_declarator_convertert::convert( } } - assert(c_it!=cpp_typecheck.symbol_table.symbols.end()); - - symbolt &symbol=c_it->second; + symbolt &symbol=*maybe_symbol; combine_types(declarator.name().source_location(), final_type, symbol); enforce_rules(symbol); @@ -194,13 +191,11 @@ symbolt &cpp_declarator_convertert::convert( } // already there? - symbol_tablet::symbolst::iterator c_it= - cpp_typecheck.symbol_table.symbols.find(final_identifier); - - if(c_it==cpp_typecheck.symbol_table.symbols.end()) + symbol_tablet::opt_symbol_reft maybe_symbol= + cpp_typecheck.symbol_table.get_writeable(final_identifier); + if(!maybe_symbol) return convert_new_symbol(storage_spec, member_spec, declarator); - - symbolt &symbol=c_it->second; + symbolt &symbol=*maybe_symbol; if(!storage_spec.is_extern()) symbol.is_extern = false; diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index c80c757298e..50da8557d3b 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -372,7 +372,7 @@ const symbolt &cpp_typecheckt::instantiate_template( // been instantiated using these arguments { // need non-const handle on template symbol - symbolt &s=symbol_table.symbols.find(template_symbol.name)->second; + symbolt &s=*symbol_table.get_writeable(template_symbol.name); irept &instantiated_with=s.value.add("instantiated_with"); instantiated_with.get_sub().push_back(specialization_template_args); } @@ -451,12 +451,7 @@ const symbolt &cpp_typecheckt::instantiate_template( if(is_template_method) { - symbol_tablet::symbolst::iterator it = - symbol_table.symbols.find(class_name); - - assert(it!=symbol_table.symbols.end()); - - symbolt &symb = it->second; + symbolt &symb=*symbol_table.get_writeable(class_name); assert(new_decl.declarators().size() == 1); diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index b1be4281d3b..570acc0aa1a 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -151,9 +151,9 @@ void cpp_typecheckt::static_and_dynamic_initialization() disable_access_control = true; - for(const auto &d_it : dynamic_initializations) + for(const irep_idt &d_it : dynamic_initializations) { - symbolt &symbol=symbol_table.symbols.find(d_it)->second; + const symbolt &symbol=*symbol_table.lookup(d_it); if(symbol.is_extern) continue; @@ -178,7 +178,7 @@ void cpp_typecheckt::static_and_dynamic_initialization() // Make it nil to get zero initialization by // __CPROVER_initialize - symbol.value.make_nil(); + symbol_table.get_writeable(d_it)->get().value.make_nil(); } else { @@ -210,7 +210,7 @@ void cpp_typecheckt::static_and_dynamic_initialization() init_symbol.is_type=false; init_symbol.is_macro=false; - symbol_table.move(init_symbol); + symbol_table.insert(std::move(init_symbol)); disable_access_control=false; } @@ -223,14 +223,15 @@ void cpp_typecheckt::do_not_typechecked() { cont = false; - Forall_symbols(s_it, symbol_table.symbols) + for(const auto &named_symbol : symbol_table.symbols) { - symbolt &symbol=s_it->second; + const symbolt &symbol=named_symbol.second; if(symbol.value.id()=="cpp_not_typechecked" && symbol.value.get_bool("is_used")) { assert(symbol.type.id()==ID_code); + symbolt &symbol=*symbol_table.get_writeable(named_symbol.first); if(symbol.base_name=="operator=") { @@ -256,37 +257,36 @@ void cpp_typecheckt::do_not_typechecked() } while(cont); - Forall_symbols(s_it, symbol_table.symbols) + for(const auto &named_symbol : symbol_table.symbols) { - symbolt &symbol=s_it->second; - if(symbol.value.id()=="cpp_not_typechecked") - symbol.value.make_nil(); + if(named_symbol.second.value.id()=="cpp_not_typechecked") + symbol_table.get_writeable(named_symbol.first)->get().value.make_nil(); } } void cpp_typecheckt::clean_up() { - symbol_tablet::symbolst::iterator it=symbol_table.symbols.begin(); + symbol_tablet::symbolst::const_iterator it=symbol_table.symbols.begin(); while(it!=symbol_table.symbols.end()) { - symbol_tablet::symbolst::iterator cur_it = it; + symbol_tablet::symbolst::const_iterator cur_it = it; it++; - symbolt &symbol = cur_it->second; + const symbolt &symbol=cur_it->second; // erase templates if(symbol.type.get_bool(ID_is_template)) { - symbol_table.symbols.erase(cur_it); + symbol_table.erase(cur_it); continue; } else if(symbol.type.id()==ID_struct || symbol.type.id()==ID_union) { // remove methods from 'components' - struct_union_typet &struct_union_type= - to_struct_union_type(symbol.type); + struct_union_typet &struct_union_type=to_struct_union_type( + symbol_table.get_writeable(cur_it->first)->get().type); const struct_union_typet::componentst &components= struct_union_type.components(); diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 6b5c7c1625b..4796f5e3d76 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -159,20 +159,19 @@ void cpp_typecheckt::typecheck_compound_type( // check if we have it already - symbol_tablet::symbolst::iterator previous_symbol= - symbol_table.symbols.find(symbol_name); - - if(previous_symbol!=symbol_table.symbols.end()) + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(symbol_name); + if(maybe_symbol) { // we do! - - symbolt &symbol=previous_symbol->second; + const symbolt &symbol=*maybe_symbol; if(has_body) { if(symbol.type.id()=="incomplete_"+type.id_string()) { // a previously incomplete struct/union becomes complete + symbolt &symbol=*symbol_table.get_writeable(symbol_name); symbol.type.swap(type); typecheck_compound_body(symbol); } @@ -523,10 +522,7 @@ void cpp_typecheckt::typecheck_compound_declarator( // get the virtual-table symbol type irep_idt vt_name="virtual_table::"+id2string(symbol.name); - symbol_tablet::symbolst::iterator vtit = - symbol_table.symbols.find(vt_name); - - if(vtit==symbol_table.symbols.end()) + if(!symbol_table.has_symbol(vt_name)) { // first time: create a virtual-table symbol type symbolt vt_symb_type; @@ -540,9 +536,8 @@ void cpp_typecheckt::typecheck_compound_declarator( vt_symb_type.type.set(ID_name, vt_symb_type.name); vt_symb_type.is_type=true; - bool failed=symbol_table.move(vt_symb_type); + const bool failed=!symbol_table.insert(std::move(vt_symb_type)).second; assert(!failed); - vtit=symbol_table.symbols.find(vt_name); // add a virtual-table pointer struct_typet::componentt compo; @@ -558,10 +553,9 @@ void cpp_typecheckt::typecheck_compound_declarator( put_compound_into_scope(compo); } - assert(vtit->second.type.id()==ID_struct); - - struct_typet &virtual_table= - to_struct_type(vtit->second.type); + typet &vt=symbol_table.get_writeable(vt_name)->get().type; + INVARIANT(vt.id()==ID_struct, "Virtual tables must be stored as struct"); + struct_typet &virtual_table=to_struct_type(vt); component.set("virtual_name", virtual_name); component.set("is_virtual", is_virtual); @@ -569,7 +563,7 @@ void cpp_typecheckt::typecheck_compound_declarator( // add an entry to the virtual table struct_typet::componentt vt_entry; vt_entry.type()=pointer_type(component.type()); - vt_entry.set_name(id2string(vtit->first)+"::"+virtual_name); + vt_entry.set_name(id2string(vt_name)+"::"+virtual_name); vt_entry.set(ID_base_name, virtual_name); vt_entry.set(ID_pretty_name, virtual_name); vt_entry.set(ID_access, ID_public); @@ -618,7 +612,7 @@ void cpp_typecheckt::typecheck_compound_declarator( arg.set(ID_C_identifier, arg_symb.name); // add the parameter to the symbol table - bool failed=symbol_table.move(arg_symb); + const bool failed=!symbol_table.insert(std::move(arg_symb)).second; assert(!failed); } @@ -676,7 +670,7 @@ void cpp_typecheckt::typecheck_compound_declarator( // add the function to the symbol table { - bool failed=symbol_table.move(func_symb); + const bool failed=!symbol_table.insert(std::move(func_symb)).second; assert(!failed); } @@ -1416,7 +1410,7 @@ void cpp_typecheckt::convert_anon_struct_union_member( struct_typet::componentst &components) { symbolt &struct_union_symbol= - symbol_table.symbols[follow(declaration.type()).get(ID_name)]; + *symbol_table.get_writeable(follow(declaration.type()).get(ID_name)); if(declaration.storage_spec().is_static() || declaration.storage_spec().is_mutable()) diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index c91c8d979cf..988b4de3568 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -74,7 +74,8 @@ void cpp_typecheckt::convert_anonymous_union( new_code.move_to_operands(decl_statement); // do scoping - symbolt union_symbol=symbol_table.symbols[follow(symbol.type).get(ID_name)]; + symbolt union_symbol= + *symbol_table.get_writeable(follow(symbol.type).get(ID_name)); const irept::subt &components=union_symbol.type.add(ID_components).get_sub(); forall_irep(it, components) @@ -104,7 +105,7 @@ void cpp_typecheckt::convert_anonymous_union( id.is_member=true; } - symbol_table.symbols[union_symbol.name].type.set( + symbol_table.get_writeable(union_symbol.name)->get().type.set( "#unnamed_object", symbol.base_name); code.swap(new_code); diff --git a/src/cpp/cpp_typecheck_enum_type.cpp b/src/cpp/cpp_typecheck_enum_type.cpp index 74a18107622..c7893c3c06a 100644 --- a/src/cpp/cpp_typecheck_enum_type.cpp +++ b/src/cpp/cpp_typecheck_enum_type.cpp @@ -121,14 +121,14 @@ void cpp_typecheckt::typecheck_enum_type(typet &type) // check if we have it - symbol_tablet::symbolst::iterator previous_symbol= + symbol_tablet::symbolst::const_iterator previous_symbol= symbol_table.symbols.find(symbol_name); if(previous_symbol!=symbol_table.symbols.end()) { // we do! - symbolt &symbol=previous_symbol->second; + const symbolt &symbol=previous_symbol->second; if(has_body) { diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index dec8510eb7b..b0a4a450395 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -1238,15 +1238,14 @@ void cpp_typecheckt::typecheck_expr_member( if(expr.type().id()==ID_code) { // Check if the function body has to be typechecked - symbol_tablet::symbolst::iterator it= + symbol_tablet::symbolst::const_iterator it= symbol_table.symbols.find(component_name); assert(it!=symbol_table.symbols.end()); - symbolt &func_symb=it->second; - - if(func_symb.value.id()=="cpp_not_typechecked") - func_symb.value.set("is_used", true); + if(it->second.value.id()=="cpp_not_typechecked") + symbol_table.get_writeable(component_name)->get() + .value.set("is_used", true); } } @@ -2204,10 +2203,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( type.id()==ID_code && type.find(ID_return_type).id()==ID_destructor) { - symbol_tablet::symbolst::iterator s_it= - symbol_table.symbols.find(it->get(ID_name)); - assert(s_it!=symbol_table.symbols.end()); - add_method_body(&(s_it->second)); + add_method_body(&symbol_table.get_writeable(it->get(ID_name))->get()); break; } } @@ -2376,7 +2372,7 @@ void cpp_typecheckt::typecheck_method_application( member_expr.swap(expr.function()); const symbolt &symbol=lookup(member_expr.get(ID_component_name)); - add_method_body(&(symbol_table.symbols.find(symbol.name)->second)); + add_method_body(&symbol_table.get_writeable(symbol.name)->get()); // build new function expression exprt new_function(cpp_symbol_expr(symbol)); @@ -2418,7 +2414,7 @@ void cpp_typecheckt::typecheck_method_application( if(symbol.value.id()=="cpp_not_typechecked" && !symbol.value.get_bool("is_used")) { - symbol_table.symbols[symbol.name].value.set("is_used", true); + symbol_table.get_writeable(symbol.name)->get().value.set("is_used", true); } } @@ -2681,15 +2677,13 @@ void cpp_typecheckt::typecheck_expr_function_identifier(exprt &expr) if(expr.id()==ID_symbol) { // Check if the function body has to be typechecked - symbol_tablet::symbolst::iterator it= + symbol_tablet::symbolst::const_iterator it= symbol_table.symbols.find(expr.get(ID_identifier)); assert(it != symbol_table.symbols.end()); - symbolt &func_symb=it->second; - - if(func_symb.value.id()=="cpp_not_typechecked") - func_symb.value.set("is_used", true); + if(it->second.value.id()=="cpp_not_typechecked") + symbol_table.get_writeable(it->first)->get().value.set("is_used", true); } c_typecheck_baset::typecheck_expr_function_identifier(expr); diff --git a/src/cpp/cpp_typecheck_namespace.cpp b/src/cpp/cpp_typecheck_namespace.cpp index c3ae770ad90..c64d6020a82 100644 --- a/src/cpp/cpp_typecheck_namespace.cpp +++ b/src/cpp/cpp_typecheck_namespace.cpp @@ -73,7 +73,7 @@ void cpp_typecheckt::convert(cpp_namespace_spect &namespace_spec) symbol.module=module; symbol.type=typet(ID_namespace); - if(symbol_table.move(symbol)) + if(!symbol_table.insert(std::move(symbol)).second) { error().source_location=symbol.location; error() << "cpp_typecheckt::convert_namespace: symbol_table.move() failed" diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index 4fb722f011e..feecc6ea169 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -107,14 +107,14 @@ void cpp_typecheckt::typecheck_class_template( // check if we have it already - symbol_tablet::symbolst::iterator previous_symbol= - symbol_table.symbols.find(symbol_name); - - if(previous_symbol!=symbol_table.symbols.end()) + symbol_tablet::opt_symbol_reft maybe_symbol= + symbol_table.get_writeable(symbol_name); + if(maybe_symbol) { // there already + symbolt &previous_symbol=*maybe_symbol; cpp_declarationt &previous_declaration= - to_cpp_declaration(previous_symbol->second.type); + to_cpp_declaration(previous_symbol.type); bool previous_has_body= previous_declaration.type().find(ID_body).is_not_nil(); @@ -126,7 +126,7 @@ void cpp_typecheckt::typecheck_class_template( error() << "template struct `" << base_name << "' defined previously\n" << "location of previous definition: " - << previous_symbol->second.location << eom; + << previous_symbol.location << eom; throw 0; } @@ -138,7 +138,7 @@ void cpp_typecheckt::typecheck_class_template( previous_declaration.template_type(), declaration.template_type()); - previous_symbol->second.type.swap(declaration); + previous_symbol.type.swap(declaration); #if 0 std::cout << "*****\n"; @@ -244,7 +244,7 @@ void cpp_typecheckt::typecheck_function_template( // check if we have it already - symbol_tablet::symbolst::iterator previous_symbol= + symbol_tablet::symbolst::const_iterator previous_symbol= symbol_table.symbols.find(symbol_name); if(previous_symbol!=symbol_table.symbols.end()) @@ -265,7 +265,7 @@ void cpp_typecheckt::typecheck_function_template( if(has_value) { - previous_symbol->second.type.swap(declaration); + symbol_table.get_writeable(symbol_name)->get().type.swap(declaration); cpp_scopes.id_map[symbol_name]=&template_scope; } @@ -384,7 +384,7 @@ void cpp_typecheckt::typecheck_class_template_member( const cpp_idt &cpp_id=**(id_set.begin()); symbolt &template_symbol= - symbol_table.symbols.find(cpp_id.identifier)->second; + *symbol_table.get_writeable(cpp_id.identifier); exprt &template_methods=static_cast( template_symbol.value.add("template_methods")); @@ -576,12 +576,12 @@ void cpp_typecheckt::convert_class_template_specialization( throw 0; } - symbol_tablet::symbolst::iterator s_it= + symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find((*id_set.begin())->identifier); assert(s_it!=symbol_table.symbols.end()); - symbolt &template_symbol=s_it->second; + const symbolt &template_symbol=s_it->second; if(!template_symbol.type.get_bool(ID_is_template)) { diff --git a/src/cpp/cpp_typecheck_virtual_table.cpp b/src/cpp/cpp_typecheck_virtual_table.cpp index ade9c5c1568..328efabbcaf 100644 --- a/src/cpp/cpp_typecheck_virtual_table.cpp +++ b/src/cpp/cpp_typecheck_virtual_table.cpp @@ -95,7 +95,7 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol) } vt_symb_var.value=values; - bool failed=symbol_table.move(vt_symb_var); + bool failed=!symbol_table.insert(std::move(vt_symb_var)).second; assert(!failed); } } diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 03cdd8544f6..530e074bd88 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -704,8 +704,8 @@ void compilet::convert_symbols(goto_functionst &dest) typedef std::set symbols_sett; symbols_sett symbols; - Forall_symbols(it, symbol_table.symbols) - symbols.insert(it->first); + for(const auto &named_symbol : symbol_table.symbols) + symbols.insert(named_symbol.first); // the symbol table iterators aren't stable for(symbols_sett::const_iterator @@ -713,7 +713,8 @@ void compilet::convert_symbols(goto_functionst &dest) it!=symbols.end(); ++it) { - symbol_tablet::symbolst::iterator s_it=symbol_table.symbols.find(*it); + symbol_tablet::symbolst::const_iterator s_it= + symbol_table.symbols.find(*it); assert(s_it!=symbol_table.symbols.end()); if(s_it->second.type.id()==ID_code && @@ -724,7 +725,7 @@ void compilet::convert_symbols(goto_functionst &dest) { debug() << "Compiling " << s_it->first << eom; converter.convert_function(s_it->first); - s_it->second.value=exprt("compiled"); + symbol_table.get_writeable(*it)->get().value=exprt("compiled"); } } } diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index f7ee9e0b057..8d683aa4418 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -168,17 +168,19 @@ int linker_script_merget::pointerize_linker_defined_symbols( // First, pointerize the actual linker-defined symbols for(const auto &pair : linker_values) { - const auto &entry=symbol_table.symbols.find(pair.first); - if(entry==symbol_table.symbols.end()) + symbol_tablet::opt_symbol_reft maybe_symbol= + symbol_table.get_writeable(pair.first); + if(!maybe_symbol) continue; - entry->second.type=pointer_type(char_type()); - entry->second.is_extern=false; - entry->second.value=pair.second.second; + symbolt &entry=*maybe_symbol; + entry.type=pointer_type(char_type()); + entry.is_extern=false; + entry.value=pair.second.second; } // Next, find all occurrences of linker-defined symbols that are _values_ // of some symbol in the symbol table, and pointerize them too - for(auto &pair : symbol_table.symbols) + for(const auto &pair : symbol_table.symbols) { std::list to_pointerize; symbols_to_pointerize(linker_values, pair.second.value, to_pointerize); @@ -188,7 +190,9 @@ int linker_script_merget::pointerize_linker_defined_symbols( debug() << "Pointerizing the symbol-table value of symbol " << pair.first << eom; int fail=pointerize_subexprs_of( - pair.second.value, to_pointerize, linker_values); + symbol_table.get_writeable(pair.first)->get().value, + to_pointerize, + linker_values); if(to_pointerize.empty() && fail==0) continue; ret=1; diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index 199ea59de21..518765e11ab 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -428,7 +428,7 @@ bool acceleratet::is_underapproximate(path_acceleratort &accelerator) if(it->id()==ID_symbol && it->type() == bool_typet()) { const irep_idt &id=to_symbol_expr(*it).get_identifier(); - const symbolt &sym=symbol_table.lookup(id); + const symbolt &sym=*symbol_table.lookup(id); if(sym.module=="scratch") { diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index b275be15bab..9a3ac8651f5 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -233,7 +233,7 @@ void acceleration_utilst::stash_variables( it!=vars.end(); ++it) { - symbolt orig=symbol_table.lookup(*it); + symbolt orig=*symbol_table.lookup(*it); symbolt stashed_sym=fresh_symbol("polynomial::stash", orig.type); substitution[orig.symbol_expr()]=stashed_sym.symbol_expr(); program.assign(stashed_sym.symbol_expr(), orig.symbol_expr()); diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index ccd3691560f..7ff1a9e5679 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -773,7 +773,7 @@ void polynomial_acceleratort::stash_variables( it!=vars.end(); ++it) { - symbolt orig=symbol_table.lookup(*it); + symbolt orig=*symbol_table.lookup(*it); symbolt stashed_sym=utils.fresh_symbol("polynomial::stash", orig.type); substitution[orig.symbol_expr()]=stashed_sym.symbol_expr(); program.assign(stashed_sym.symbol_expr(), orig.symbol_expr()); diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 0b210d966d1..2384f225513 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -47,14 +47,15 @@ void dump_ct::operator()(std::ostream &os) // add copies of struct types when ID_C_transparent_union is only // annotated to parameter symbol_tablet symbols_transparent; - Forall_symbols(it, copied_symbol_table.symbols) + for(const auto &named_symbol : copied_symbol_table.symbols) { - symbolt &symbol=it->second; + const symbolt &symbol=named_symbol.second; if(symbol.type.id()!=ID_code) continue; - code_typet &code_type=to_code_type(symbol.type); + code_typet &code_type=to_code_type( + copied_symbol_table.get_writeable(named_symbol.first)->get().type); code_typet::parameterst ¶meters=code_type.parameters(); for(code_typet::parameterst::iterator @@ -90,9 +91,9 @@ void dump_ct::operator()(std::ostream &os) // add tags to anonymous union/struct/enum, // and prepare lexicographic order std::set symbols_sorted; - Forall_symbols(it, copied_symbol_table.symbols) + for(const auto &named_symbol : copied_symbol_table.symbols) { - symbolt &symbol=it->second; + symbolt &symbol=*copied_symbol_table.get_writeable(named_symbol.first); bool tag_added=false; // TODO we could get rid of some of the ID_anonymous by looking up @@ -113,7 +114,7 @@ void dump_ct::operator()(std::ostream &os) tag_added=true; } - const std::string name_str=id2string(it->first); + const std::string name_str=id2string(named_symbol.first); if(symbol.is_type && (symbol.type.id()==ID_union || symbol.type.id()==ID_struct || diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp index 5cf1883fb8f..938f0e83db1 100644 --- a/src/goto-instrument/function.cpp +++ b/src/goto-instrument/function.cpp @@ -45,7 +45,7 @@ code_function_callt function_to_call( new_symbol.base_name=id; new_symbol.type=function_type; - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); s_it=symbol_table.symbols.find(id); assert(s_it!=symbol_table.symbols.end()); diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index e773b91cd02..99444893dfb 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -133,11 +133,8 @@ void goto_program2codet::scan_for_varargs() { system_headers.insert("stdarg.h"); - symbol_tablet::symbolst::iterator it= - symbol_table.symbols.find(func_name); - assert(it!=symbol_table.symbols.end()); - - code_typet &code_type=to_code_type(it->second.type); + code_typet &code_type= + to_code_type(symbol_table.get_writeable(func_name)->get().type); code_typet::parameterst ¶meters=code_type.parameters(); for(code_typet::parameterst::iterator @@ -1671,12 +1668,12 @@ void goto_program2codet::remove_const(typet &type) if(!const_removed.insert(identifier).second) return; - symbol_tablet::symbolst::iterator it= - symbol_table.symbols.find(identifier); - assert(it!=symbol_table.symbols.end()); - assert(it->second.is_type); + symbolt &symbol=*symbol_table.get_writeable(identifier); + INVARIANT( + symbol.is_type, + "Symbol "+id2string(identifier)+" should be a type"); - remove_const(it->second.type); + remove_const(symbol.type); } else if(type.id()==ID_array) remove_const(type.subtype()); @@ -1959,7 +1956,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) symbol.type=code_type; id=symbol.name; - symbol_table.move(symbol); + symbol_table.insert(std::move(symbol)); } const symbolt &symbol=ns.lookup(id); diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-instrument/remove_function.cpp index 2ec053ccac4..f9344f68238 100644 --- a/src/goto-instrument/remove_function.cpp +++ b/src/goto-instrument/remove_function.cpp @@ -51,7 +51,7 @@ void remove_function( message.status() << "Removing body of " << identifier << messaget::eom; entry->second.clear(); - goto_model.symbol_table.lookup(identifier).value.make_nil(); + goto_model.symbol_table.get_writeable(identifier)->get().value.make_nil(); } } diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index 2dc96cdf8bd..606a25f40bb 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -38,7 +38,7 @@ symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table) new_symbol.is_thread_local=true; new_symbol.is_lvalue=true; - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); return symbol_exprt(identifier, type); } diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index 5c416946213..188e750b2c9 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -93,7 +93,7 @@ void uninitializedt::add_assertions(goto_programt &goto_program) new_symbol.is_file_local=true; new_symbol.is_lvalue=true; - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); } Forall_goto_program_instructions(i_it, goto_program) diff --git a/src/goto-instrument/wmm/shared_buffers.h b/src/goto-instrument/wmm/shared_buffers.h index 0550291637e..a3b87a26d86 100644 --- a/src/goto-instrument/wmm/shared_buffers.h +++ b/src/goto-instrument/wmm/shared_buffers.h @@ -158,9 +158,12 @@ class shared_bufferst irep_idt choice(const irep_idt &function, const std::string &suffix) { - const std::string function_base_name = (symbol_table.has_symbol(function)? - id2string(symbol_table.lookup(function).base_name): - "main"); + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(function); + const std::string function_base_name = + maybe_symbol + ? id2string(maybe_symbol->get().base_name) + : "main"; return add(function_base_name+"_weak_choice", function_base_name+"_weak_choice", suffix, bool_typet()); } diff --git a/src/goto-programs/goto_convert_exceptions.cpp b/src/goto-programs/goto_convert_exceptions.cpp index d51a16c13ad..14e0ff6208f 100644 --- a/src/goto-programs/goto_convert_exceptions.cpp +++ b/src/goto-programs/goto_convert_exceptions.cpp @@ -264,7 +264,7 @@ symbol_exprt goto_convertt::exception_flag() new_symbol.is_thread_local=true; new_symbol.is_file_local=false; new_symbol.type=bool_typet(); - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); } return symbol_exprt(id, bool_typet()); diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index c65bc472a46..b3ba928bcca 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -444,7 +444,7 @@ typet interpretert::get_type(const irep_idt &id) const { dynamic_typest::const_iterator it=dynamic_types.find(id); if(it==dynamic_types.end()) - return symbol_table.lookup(id).type; + return symbol_table.lookup(id)->get().type; return it->second; } @@ -1041,7 +1041,7 @@ exprt interpretert::get_value(const irep_idt &id) if(findit!=dynamic_types.end()) get_type=findit->second; else - get_type=symbol_table.lookup(id).type; + get_type=symbol_table.lookup(id)->get().type; symbol_exprt symbol_expr(id, get_type); mp_integer whole_lhs_object_address=evaluate_address(symbol_expr); diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 16ffc1063d0..56313c42201 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -118,11 +118,13 @@ void mm_io( irep_idt id_r=CPROVER_PREFIX "mm_io_r"; irep_idt id_w=CPROVER_PREFIX "mm_io_w"; - if(symbol_table.has_symbol(id_r)) - mm_io_r=symbol_table.lookup(id_r).symbol_expr(); + symbol_tablet::opt_const_symbol_reft maybe_symbol=symbol_table.lookup(id_r); + if(maybe_symbol) + mm_io_r=maybe_symbol->get().symbol_expr(); - if(symbol_table.has_symbol(id_w)) - mm_io_w=symbol_table.lookup(id_w).symbol_expr(); + maybe_symbol=symbol_table.lookup(id_w); + if(maybe_symbol) + mm_io_w=maybe_symbol->get().symbol_expr(); for(auto & f : goto_functions.function_map) mm_io(mm_io_r, mm_io_w, f.second, ns); diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp index 76f0deacc2e..230490318dc 100644 --- a/src/goto-programs/rebuild_goto_start_function.cpp +++ b/src/goto-programs/rebuild_goto_start_function.cpp @@ -81,7 +81,7 @@ bool rebuild_goto_start_functiont::operator()() irep_idt rebuild_goto_start_functiont::get_entry_point_mode() const { const symbolt ¤t_entry_point= - symbol_table.lookup(goto_functionst::entry_point()); + *symbol_table.lookup(goto_functionst::entry_point()); return current_entry_point.mode; } diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp index 78b655e4108..141fc4709fc 100644 --- a/src/goto-programs/remove_complex.cpp +++ b/src/goto-programs/remove_complex.cpp @@ -282,8 +282,8 @@ static void remove_complex(symbolt &symbol) /// removes complex data type void remove_complex(symbol_tablet &symbol_table) { - Forall_symbols(it, symbol_table.symbols) - remove_complex(it->second); + for(const auto &named_symbol : symbol_table.symbols) + remove_complex(*symbol_table.get_writeable(named_symbol.first)); } /// removes complex data type diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp index de5649892f2..9b8e67c8b68 100644 --- a/src/goto-programs/remove_const_function_pointers.cpp +++ b/src/goto-programs/remove_const_function_pointers.cpp @@ -68,7 +68,7 @@ exprt remove_const_function_pointerst::replace_const_symbols( if(is_const_expression(expression)) { const symbolt &symbol= - symbol_table.lookup(expression.get(ID_identifier)); + *symbol_table.lookup(expression.get(ID_identifier)); if(symbol.type.id()!=ID_code) { const exprt &symbol_value=symbol.value; @@ -105,7 +105,7 @@ exprt remove_const_function_pointerst::resolve_symbol( const symbol_exprt &symbol_expr) const { const symbolt &symbol= - symbol_table.lookup(symbol_expr.get_identifier()); + *symbol_table.lookup(symbol_expr.get_identifier()); return symbol.value; } diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index d437ddf622b..a2cfcc10947 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -134,10 +134,10 @@ void remove_exceptionst::add_exceptional_returns( const irep_idt &function_id=func_it->first; goto_programt &goto_program=func_it->second.body; - INVARIANT( - symbol_table.has_symbol(function_id), - "functions should be recorded in the symbol table"); - const symbolt &function_symbol=symbol_table.lookup(function_id); + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(function_id); + INVARIANT(maybe_symbol, "functions should be recorded in the symbol table"); + const symbolt &function_symbol=*maybe_symbol; // for now only add exceptional returns for Java if(function_symbol.mode!=ID_java) @@ -148,10 +148,10 @@ void remove_exceptionst::add_exceptional_returns( // some methods (e.g. the entry method) have already been added to // the symbol table; if you find it, initialise it - if(symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX)) + maybe_symbol=symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + if(maybe_symbol) { - const symbolt &symbol= - symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + const symbolt &symbol=*maybe_symbol; symbol_exprt lhs_expr_null=symbol.symbol_expr(); null_pointer_exprt rhs_expr_null((pointer_type(empty_typet()))); goto_programt::targett t_null= @@ -200,7 +200,7 @@ void remove_exceptionst::add_exceptional_returns( || has_uncaught_exceptions) { // look up the function symbol - symbol_tablet::symbolst::iterator s_it= + symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find(function_id); INVARIANT( @@ -255,10 +255,11 @@ void remove_exceptionst::instrument_exception_handler( to_code_landingpad(instr_it->code).catch_expr(); irep_idt thrown_exception_global=id2string(function_id)+EXC_SUFFIX; - if(symbol_table.has_symbol(thrown_exception_global)) + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(thrown_exception_global); + if(maybe_symbol) { - const symbol_exprt thrown_global_symbol= - symbol_table.lookup(thrown_exception_global).symbol_expr(); + const symbol_exprt thrown_global_symbol=maybe_symbol->get().symbol_expr(); // next we reset the exceptional return to NULL null_pointer_exprt null_voidptr((pointer_type(empty_typet()))); @@ -314,7 +315,7 @@ void remove_exceptionst::add_exception_dispatch_sequence( // find the symbol corresponding to the caught exceptions const symbolt &exc_symbol= - symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + *symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); symbol_exprt exc_thrown=exc_symbol.symbol_expr(); // add GOTOs implementing the dynamic dispatch of the @@ -389,7 +390,7 @@ void remove_exceptionst::instrument_throw( // find the symbol where the thrown exception should be stored: const symbolt &exc_symbol= - symbol_table.lookup(id2string(func_it->first)+EXC_SUFFIX); + *symbol_table.lookup(id2string(func_it->first)+EXC_SUFFIX); symbol_exprt exc_thrown=exc_symbol.symbol_expr(); // add the assignment with the appropriate cast @@ -424,19 +425,20 @@ void remove_exceptionst::instrument_function_call( const irep_idt &callee_id= to_symbol_expr(function_call.function()).get_identifier(); - const irep_idt &callee_inflight_exception=id2string(callee_id)+EXC_SUFFIX; - const irep_idt &local_inflight_exception=id2string(function_id)+EXC_SUFFIX; + symbol_tablet::opt_const_symbol_reft callee_inflight_exception= + symbol_table.lookup(id2string(callee_id)+EXC_SUFFIX); + symbol_tablet::opt_const_symbol_reft local_inflight_exception= + symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); - if(symbol_table.has_symbol(callee_inflight_exception) && - symbol_table.has_symbol(local_inflight_exception)) + if(callee_inflight_exception && local_inflight_exception) { add_exception_dispatch_sequence( func_it, instr_it, stack_catch, locals); const symbol_exprt callee_inflight_exception_expr= - symbol_table.lookup(callee_inflight_exception).symbol_expr(); + callee_inflight_exception->get().symbol_expr(); const symbol_exprt local_inflight_exception_expr= - symbol_table.lookup(local_inflight_exception).symbol_expr(); + local_inflight_exception->get().symbol_expr(); // add a null check (so that instanceof can be applied) equal_exprt eq_null( diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index cc3a68440c3..1a22bd72359 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -62,11 +62,7 @@ void remove_returnst::replace_returns( if(has_return_value) { // look up the function symbol - symbol_tablet::symbolst::iterator s_it= - symbol_table.symbols.find(function_id); - - assert(s_it!=symbol_table.symbols.end()); - symbolt &function_symbol=s_it->second; + symbolt &function_symbol=*symbol_table.get_writeable(function_id); // make the return type 'void' f_it->second.type.return_type()=empty_typet(); @@ -251,18 +247,14 @@ bool remove_returnst::restore_returns( // do we have X#return_value? std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX; - symbol_tablet::symbolst::iterator rv_it= + symbol_tablet::symbolst::const_iterator rv_it= symbol_table.symbols.find(rv_name); if(rv_it==symbol_table.symbols.end()) return true; // look up the function symbol - symbol_tablet::symbolst::iterator s_it= - symbol_table.symbols.find(function_id); - - assert(s_it!=symbol_table.symbols.end()); - symbolt &function_symbol=s_it->second; + symbolt &function_symbol=*symbol_table.get_writeable(function_id); // restore the return type f_it->second.type=original_return_type(symbol_table, function_id); @@ -270,7 +262,7 @@ bool remove_returnst::restore_returns( // remove the return_value symbol from the symbol_table irep_idt rv_name_id=rv_it->second.name; - symbol_table.symbols.erase(rv_it); + symbol_table.erase(rv_it); goto_programt &goto_program=f_it->second.body; diff --git a/src/goto-programs/remove_static_init_loops.cpp b/src/goto-programs/remove_static_init_loops.cpp index c0f3c05150f..794ec547fc4 100644 --- a/src/goto-programs/remove_static_init_loops.cpp +++ b/src/goto-programs/remove_static_init_loops.cpp @@ -58,21 +58,23 @@ void remove_static_init_loopst::unwind_enum_static( const std::string &fname=id2string(ins.function); size_t class_prefix_length=fname.find_last_of('.'); // is the function symbol in the symbol table? - if(!symbol_table.has_symbol(ins.function)) + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(ins.function); + if(!maybe_symbol) { message.warning() << "function `" << id2string(ins.function) << "` is not in symbol table" << messaget::eom; continue; } // is Java function and static init? - const symbolt &function_name=symbol_table.lookup(ins.function); + const symbolt &function_name=*maybe_symbol; if(!(function_name.mode==ID_java && has_suffix(fname, java_clinit))) continue; assert( class_prefix_length!=std::string::npos && "could not identify class name"); const std::string &classname=fname.substr(0, class_prefix_length); - const symbolt &class_symbol=symbol_table.lookup(classname); + const symbolt &class_symbol=*symbol_table.lookup(classname); const class_typet &class_type=to_class_type(class_symbol.type); size_t unwinds=class_type.get_size_t(ID_java_enum_static_unwind); diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index a5874999b78..f2e7f5b9fe4 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -190,8 +190,8 @@ static void remove_vector(symbolt &symbol) /// removes vector data type static void remove_vector(symbol_tablet &symbol_table) { - Forall_symbols(it, symbol_table.symbols) - remove_vector(it->second); + for(const auto &named_symbol : symbol_table.symbols) + remove_vector(*symbol_table.get_writeable(named_symbol.first)); } /// removes vector data type diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 26671e18527..e1f8c79444c 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -273,7 +273,7 @@ void remove_virtual_functionst::get_functions( root_function.class_id=resolved_call.get_class_identifier(); const symbolt &called_symbol= - symbol_table.lookup(resolved_call.get_virtual_method_name()); + *symbol_table.lookup(resolved_call.get_virtual_method_name()); root_function.symbol_expr=called_symbol.symbol_expr(); root_function.symbol_expr.set( diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index f7599e16578..05f9371e492 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -174,9 +174,7 @@ void string_abstractiont::add_str_arguments( const irep_idt &name, goto_functionst::goto_functiont &fct) { - symbol_tablet::symbolst::iterator sym_entry=symbol_table.symbols.find(name); - assert(sym_entry!=symbol_table.symbols.end()); - symbolt &fct_symbol=sym_entry->second; + symbolt &fct_symbol=*symbol_table.get_writeable(name); code_typet::parameterst ¶meters= to_code_type(fct.type).parameters(); @@ -234,7 +232,7 @@ void string_abstractiont::add_argument( new_symbol.mode=fct_symbol.mode; new_symbol.pretty_name=str_args.back().get_base_name(); - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); } void string_abstractiont::abstract(goto_programt &dest) @@ -453,7 +451,7 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value( assignment1->code.add_source_location()=ref_instr->source_location; } - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); return sym_expr; } @@ -937,7 +935,7 @@ exprt string_abstractiont::build_unknown(const typet &type, bool write) new_symbol.mode=ID_C; new_symbol.pretty_name=identifier; - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); return ns.lookup(identifier).symbol_expr(); } @@ -989,7 +987,7 @@ void string_abstractiont::build_new_symbol(const symbolt &symbol, new_symbol.is_static_lifetime=symbol.is_static_lifetime; new_symbol.is_thread_local=symbol.is_thread_local; - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); if(symbol.is_static_lifetime) { @@ -1037,7 +1035,7 @@ bool string_abstractiont::build_symbol_constant( assignment1->code=code_assignt(new_symbol.symbol_expr(), value); } - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); } dest=address_of_exprt(symbol_exprt(identifier, string_struct)); diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp index 6e696c30042..a0741d6a7d7 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/goto-programs/string_instrumentation.cpp @@ -809,8 +809,8 @@ void string_instrumentationt::do_strerror( new_symbol_buf.pretty_name=new_symbol_buf.base_name; new_symbol_buf.name=new_symbol_buf.base_name; - symbol_table.move(new_symbol_buf); - symbol_table.move(new_symbol_size); + symbol_table.insert(std::move(new_symbol_buf)); + symbol_table.insert(std::move(new_symbol_size)); } const symbolt &symbol_size=ns.lookup(identifier_size); @@ -885,7 +885,7 @@ void string_instrumentationt::invalidate_buffer( new_symbol.is_lvalue=true; new_symbol.is_static_lifetime=true; - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); } const symbolt &cntr_sym=ns.lookup(cntr_id); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 6dc9a944010..0243f1487c2 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -156,7 +156,7 @@ void goto_symext::parameter_assignments( symbol.base_name="va_arg"+std::to_string(va_count); symbol.type=it1->type(); - new_symbol_table.move(symbol); + new_symbol_table.insert(std::move(symbol)); symbol_exprt lhs=symbol_exprt(id, it1->type()); diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index 41eab823e42..c9ddec10d81 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -144,7 +144,7 @@ bool ci_lazy_methodst::operator()( method_converter( *parsed_method.first, *parsed_method.second, new_lazy_methods); gather_virtual_callsites( - symbol_table.lookup(mname).value, + symbol_table.lookup(mname)->get().value, virtual_callsites); any_new_methods=true; } diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 0942b52fbf7..d27ff99b41b 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -216,7 +216,7 @@ void java_bytecode_convert_classt::convert( // Do we have the static field symbol already? const auto s_it=symbol_table.symbols.find(new_symbol.name); if(s_it!=symbol_table.symbols.end()) - symbol_table.symbols.erase(s_it); // erase, we stubbed it + symbol_table.erase(s_it); // erase, we stubbed it if(symbol_table.add(new_symbol)) assert(false && "failed to add static field symbol"); diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 840b214049a..00652d34618 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -320,7 +320,7 @@ void java_bytecode_convert_methodt::convert( id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.signature; method_id=method_identifier; - const auto &old_sym=symbol_table.lookup(method_identifier); + const symbolt &old_sym=*symbol_table.lookup(method_identifier); // Obtain a std::vector of code_typet::parametert objects from the // (function) type of the symbol @@ -488,7 +488,7 @@ void java_bytecode_convert_methodt::convert( INVARIANT( s_it!=symbol_table.symbols.end(), "the symbol was there earlier on this function; it must be there now"); - symbol_table.symbols.erase(s_it); + symbol_table.erase(s_it); // Insert the method symbol in the symbol table symbol_table.add(method_symbol); @@ -883,14 +883,15 @@ bool java_bytecode_convert_methodt::class_needs_clinit( findit_any.first->second=true; return true; } - auto findit_symbol=symbol_table.symbols.find(classname); + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(classname); // Stub class? - if(findit_symbol==symbol_table.symbols.end()) + if(!maybe_symbol) { warning() << "SKIPPED: " << classname << eom; return false; } - const symbolt &class_symbol=symbol_table.lookup(classname); + const symbolt &class_symbol=*maybe_symbol; for(const auto &base : to_class_type(class_symbol.type).bases()) { if(class_needs_clinit(to_symbol_type(base.type()).get_identifier())) @@ -948,7 +949,7 @@ exprt java_bytecode_convert_methodt::get_or_create_clinit_wrapper( code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt()); init_body.move_to_operands(set_already_run); const irep_idt &real_clinit_name=id2string(classname)+".:()V"; - const symbolt &class_symbol=symbol_table.lookup(classname); + const symbolt &class_symbol=*symbol_table.lookup(classname); auto findsymit=symbol_table.symbols.find(real_clinit_name); if(findsymit!=symbol_table.symbols.end()) @@ -2831,7 +2832,7 @@ bool java_bytecode_convert_methodt::is_method_inherited( if(resolved_call.is_valid()) { const symbolt &function_symbol= - symbol_table.lookup(resolved_call.get_virtual_method_name()); + *symbol_table.lookup(resolved_call.get_virtual_method_name()); INVARIANT(function_symbol.type.id()==ID_code, "Function must be code"); diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index dd29b0b5ec5..1b30f02d037 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -617,5 +617,5 @@ void java_bytecode_instrument( // instrument(...) can add symbols to the table, so it's // not safe to hold a reference to a symbol across a call. for(const auto &symbol : symbols_to_instrument) - instrument(symbol_table.lookup(symbol).value); + instrument(symbol_table.get_writeable(symbol)->get().value); } diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index afda2091079..cd6210bdb8f 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -374,7 +374,7 @@ void java_bytecode_languaget::replace_string_methods( if(generated_code.is_not_nil()) { // Replace body of the function by code generated by string preprocess - symbolt &symbol=context.lookup(id); + symbolt &symbol=*context.get_writeable(id); symbol.value=generated_code; // Specifically instrument the new code, since this comes after the // blanket instrumentation pass called before typechecking. diff --git a/src/java_bytecode/java_bytecode_typecheck.cpp b/src/java_bytecode/java_bytecode_typecheck.cpp index 5b09fcdaf23..e7f096c8333 100644 --- a/src/java_bytecode/java_bytecode_typecheck.cpp +++ b/src/java_bytecode/java_bytecode_typecheck.cpp @@ -48,22 +48,18 @@ void java_bytecode_typecheckt::typecheck() // recursively doing base classes first. for(const irep_idt &id : identifiers) { - symbolt &symbol=symbol_table.symbols[id]; - + symbolt &symbol=*symbol_table.get_writeable(id); if(!symbol.is_type) continue; - typecheck_type_symbol(symbol); } // We now check all non-type symbols for(const irep_idt &id : identifiers) { - symbolt &symbol=symbol_table.symbols[id]; - + symbolt &symbol=*symbol_table.get_writeable(id); if(symbol.is_type) continue; - typecheck_non_type_symbol(symbol); } } diff --git a/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/src/java_bytecode/java_bytecode_typecheck_expr.cpp index f25e988e850..d73525ccc60 100644 --- a/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -291,7 +291,7 @@ void java_bytecode_typecheckt::typecheck_expr_member(member_exprt &expr) // member doesn't exist. In this case struct_type should be an opaque // stub, and we'll add the member to it. symbolt &symbol_table_type= - symbol_table.lookup("java::"+id2string(struct_type.get_tag())); + *symbol_table.get_writeable("java::"+id2string(struct_type.get_tag())); auto &add_to_components= to_struct_type(symbol_table_type.type).components(); add_to_components diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 08c1f44564b..e9863e51152 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -40,7 +40,7 @@ static void create_initialize(symbol_tablet &symbol_table) { // If __CPROVER_initialize already exists, replace it. It may already exist // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend. - symbol_table.symbols.erase(INITIALIZE_FUNCTION); + symbol_table.remove(INITIALIZE_FUNCTION); symbolt initialize; initialize.name=INITIALIZE_FUNCTION; @@ -96,7 +96,7 @@ void java_static_lifetime_init( const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) { - symbolt &initialize_symbol=symbol_table.lookup(INITIALIZE_FUNCTION); + symbolt &initialize_symbol=*symbol_table.get_writeable(INITIALIZE_FUNCTION); code_blockt &code_block=to_code_block(to_code(initialize_symbol.value)); // We need to zero out all static variables, or nondet-initialize if they're @@ -109,7 +109,7 @@ void java_static_lifetime_init( for(const auto &symname : symbol_names) { - const symbolt &sym=symbol_table.lookup(symname); + const symbolt &sym=*symbol_table.lookup(symname); if(should_init_symbol(sym)) { if(sym.value.is_nil() && sym.type!=empty_typet()) @@ -264,7 +264,7 @@ void java_record_outputs( output.operands().resize(2); const symbolt &return_symbol= - symbol_table.lookup(JAVA_ENTRY_POINT_RETURN_SYMBOL); + *symbol_table.lookup(JAVA_ENTRY_POINT_RETURN_SYMBOL); output.op0()= address_of_exprt( @@ -282,7 +282,7 @@ void java_record_outputs( param_number++) { const symbolt &p_symbol= - symbol_table.lookup(parameters[param_number].get_identifier()); + *symbol_table.lookup(parameters[param_number].get_identifier()); if(p_symbol.type.id()==ID_pointer) { @@ -306,7 +306,7 @@ void java_record_outputs( output.operands().resize(2); // retrieve the exception variable - const symbolt exc_symbol=symbol_table.lookup( + const symbolt exc_symbol=*symbol_table.lookup( JAVA_ENTRY_POINT_EXCEPTION_SYMBOL); output.op0()=address_of_exprt( @@ -541,7 +541,7 @@ bool generate_java_start_function( // build call to initialization function { - symbol_tablet::symbolst::iterator init_it= + symbol_tablet::symbolst::const_iterator init_it= symbol_table.symbols.find(INITIALIZE_FUNCTION); if(init_it==symbol_table.symbols.end()) @@ -668,7 +668,7 @@ bool generate_java_start_function( new_symbol.value.swap(init_code); new_symbol.mode=ID_java; - if(symbol_table.move(new_symbol)) + if(!symbol_table.insert(std::move(new_symbol)).second) { message.error() << "failed to move main symbol" << messaget::eom; return true; diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index c4176fd741a..ce053f25185 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -166,9 +166,9 @@ bool java_string_library_preprocesst::is_java_char_array_pointer_type( /// \param symbol_table: a symbol_table containing an entry for java Strings /// \return the type of data fields in java Strings. -typet string_data_type(symbol_tablet symbol_table) +typet string_data_type(const symbol_tablet &symbol_table) { - symbolt sym=symbol_table.lookup("java::java.lang.String"); + symbolt sym=*symbol_table.lookup("java::java.lang.String"); typet concrete_type=sym.type; struct_typet struct_type=to_struct_type(concrete_type); std::size_t index=struct_type.component_number("data"); @@ -384,7 +384,7 @@ typet java_string_library_preprocesst::get_data_type( PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol); if(type.id()==ID_symbol) { - symbolt sym=symbol_table.lookup(to_symbol_type(type).get_identifier()); + symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier()); CHECK_RETURN(sym.type.id()!=ID_symbol); return get_data_type(sym.type, symbol_table); } @@ -403,7 +403,7 @@ typet java_string_library_preprocesst::get_length_type( PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol); if(type.id()==ID_symbol) { - symbolt sym=symbol_table.lookup(to_symbol_type(type).get_identifier()); + symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier()); CHECK_RETURN(sym.type.id()!=ID_symbol); return get_length_type(sym.type, symbol_table); } @@ -711,7 +711,7 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string( code_blockt code; // A String has a field Object with @clsid = String and @lock = false: - const symbolt &jlo_symbol=symbol_table.lookup("java::java.lang.Object"); + const symbolt &jlo_symbol=*symbol_table.lookup("java::java.lang.Object"); const struct_typet &jlo_struct=to_struct_type(jlo_symbol.type); struct_exprt jlo_init(jlo_struct); jlo_init.copy_to_operands(constant_exprt( @@ -797,7 +797,7 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr( typet deref_type; if(rhs.type().subtype().id()==ID_symbol) deref_type=symbol_table.lookup( - to_symbol_type(rhs.type().subtype()).get_identifier()).type; + to_symbol_type(rhs.type().subtype()).get_identifier())->get().type; else deref_type=rhs.type().subtype(); @@ -1252,10 +1252,11 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object( // Check that the type of the object is in the symbol table, // otherwise there is no safe way of finding its value. - if(symbol_table.has_symbol(object_type.get_identifier())) + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(object_type.get_identifier()); + if(maybe_symbol) { - struct_typet struct_type=to_struct_type( - symbol_table.lookup(object_type.get_identifier()).type); + struct_typet struct_type=to_struct_type(maybe_symbol->get().type); // Check that the type has a value field const struct_union_typet::componentt value_comp= struct_type.get_component("value"); @@ -1500,7 +1501,8 @@ codet java_string_library_preprocesst::make_object_get_class_code( // > Class class1; pointer_typet class_type= - java_reference_type(symbol_table.lookup("java::java.lang.Class").type); + java_reference_type( + symbol_table.lookup("java::java.lang.Class")->get().type); symbolt class1_sym=get_fresh_aux_symbol( class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table); symbol_exprt class1=class1_sym.symbol_expr(); @@ -1536,8 +1538,8 @@ codet java_string_library_preprocesst::make_object_get_class_code( code.add(code_assignt(string_expr_sym1, string_expr1)); // string1 = (String*) string_expr - pointer_typet string_ptr_type= - java_reference_type(symbol_table.lookup("java::java.lang.String").type); + pointer_typet string_ptr_type=java_reference_type( + symbol_table.lookup("java::java.lang.String")->get().type); exprt string1=allocate_fresh_string(string_ptr_type, loc, symbol_table, code); code.add( code_assign_string_expr_to_new_java_string( diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index bf41076d84c..9cb7fab0492 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -86,9 +86,9 @@ void generate_class_stub( new_symbol.mode=ID_java; new_symbol.is_type=true; - symbolt *class_symbol; + std::pair res=symbol_table.insert(std::move(new_symbol)); - if(symbol_table.move(new_symbol, class_symbol)) + if(!res.second) { messaget message(message_handler); message.warning() << @@ -99,7 +99,7 @@ void generate_class_stub( else { // create the class identifier etc - java_root_class(*class_symbol); + java_root_class(res.first); } } diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp index 328a1c76223..3bc44fa41e1 100644 --- a/src/jsil/jsil_convert.cpp +++ b/src/jsil/jsil_convert.cpp @@ -48,9 +48,11 @@ bool jsil_convertt::operator()(const jsil_parse_treet &parse_tree) if(convert_code(new_symbol, to_code(new_symbol.value))) return true; - if(symbol_table.has_symbol(new_symbol.name)) + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(new_symbol.name); + if(maybe_symbol) { - symbolt &s=symbol_table.lookup(new_symbol.name); + const symbolt &s=*maybe_symbol; if(s.value.id()=="no-body-just-yet") { symbol_table.remove(s.name); diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp index 2f4d88e1bb3..991ca1c226c 100644 --- a/src/jsil/jsil_entry_point.cpp +++ b/src/jsil/jsil_entry_point.cpp @@ -129,7 +129,7 @@ bool jsil_entry_point( // build call to initialization function { - symbol_tablet::symbolst::iterator init_it= + symbol_tablet::symbolst::const_iterator init_it= symbol_table.symbols.find(CPROVER_PREFIX "initialize"); if(init_it==symbol_table.symbols.end()) @@ -162,7 +162,7 @@ bool jsil_entry_point( new_symbol.type.swap(main_type); new_symbol.value.swap(init_code); - if(symbol_table.move(new_symbol)) + if(!symbol_table.insert(std::move(new_symbol)).second) { messaget message; message.set_message_handler(message_handler); diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp index 81ebf82f87b..ecc36288bae 100644 --- a/src/jsil/jsil_typecheck.cpp +++ b/src/jsil/jsil_typecheck.cpp @@ -42,13 +42,15 @@ void jsil_typecheckt::update_expr_type(exprt &expr, const typet &type) { const irep_idt &id=to_symbol_expr(expr).get_identifier(); - if(!symbol_table.has_symbol(id)) + symbol_tablet::opt_symbol_reft maybe_symbol= + symbol_table.get_writeable(id); + if(!maybe_symbol) { error() << "unexpected symbol: " << id << eom; throw 0; } - symbolt &s=symbol_table.lookup(id); + symbolt &s=*maybe_symbol; if(s.type.id().empty() || s.type.is_nil()) s.type=type; else @@ -747,13 +749,14 @@ void jsil_typecheckt::typecheck_function_call( { const irep_idt &id=to_symbol_expr(f).get_identifier(); - if(symbol_table.has_symbol(id)) + symbol_tablet::opt_const_symbol_reft maybe_symbol=symbol_table.lookup(id); + if(maybe_symbol) { - symbolt &s=symbol_table.lookup(id); + const symbolt &s=*maybe_symbol; if(s.type.id()==ID_code) { - code_typet &codet=to_code_type(s.type); + const code_typet &codet=to_code_type(s.type); for(std::size_t i=0; i src_symbols; // First apply the renaming - Forall_symbols(s_it, src_symbol_table.symbols) + for(const auto &named_symbol : src_symbol_table.symbols) { + symbolt symbol=named_symbol.second; // apply the renaming - rename_symbol(s_it->second.type); - rename_symbol(s_it->second.value); + rename_symbol(symbol.type); + rename_symbol(symbol.value); + // Add to vector + src_symbols.emplace(named_symbol.first, std::move(symbol)); } // Move over all the non-colliding ones id_sett collisions; - Forall_symbols(s_it, src_symbol_table.symbols) + for(const auto &named_symbol : src_symbols) { // renamed? - if(s_it->first!=s_it->second.name) + if(named_symbol.first!=named_symbol.second.name) { // new - main_symbol_table.add(s_it->second); + main_symbol_table.add(named_symbol.second); } else { - symbol_tablet::symbolst::iterator - m_it=main_symbol_table.symbols.find(s_it->first); - - if(m_it==main_symbol_table.symbols.end()) + if(!main_symbol_table.has_symbol(named_symbol.first)) { // new - main_symbol_table.add(s_it->second); + main_symbol_table.add(named_symbol.second); } else - collisions.insert(s_it->first); + collisions.insert(named_symbol.first); } } // Now do the collisions - for(id_sett::const_iterator - i_it=collisions.begin(); - i_it!=collisions.end(); - i_it++) + for(const irep_idt &collision : collisions) { - symbolt &old_symbol=main_symbol_table.symbols[*i_it]; - symbolt &new_symbol=src_symbol_table.symbols[*i_it]; + symbolt &old_symbol=*main_symbol_table.get_writeable(collision); + symbolt &new_symbol=src_symbols.at(collision); if(new_symbol.is_type) duplicate_type_symbol(old_symbol, new_symbol); @@ -1288,12 +1283,15 @@ void linkingt::copy_symbols() } // Apply type updates to initializers - Forall_symbols(s_it, main_symbol_table.symbols) + for(const auto &named_symbol : main_symbol_table.symbols) { - if(!s_it->second.is_type && - !s_it->second.is_macro && - s_it->second.value.is_not_nil()) - object_type_updates(s_it->second.value); + if(!named_symbol.second.is_type && + !named_symbol.second.is_macro && + named_symbol.second.value.is_not_nil()) + { + object_type_updates( + main_symbol_table.get_writeable(named_symbol.first)->get().value); + } } } diff --git a/src/linking/linking_class.h b/src/linking/linking_class.h index d3fa633af2f..70b59f59bc1 100644 --- a/src/linking/linking_class.h +++ b/src/linking/linking_class.h @@ -105,7 +105,7 @@ class linkingt:public typecheckt void duplicate_type_symbol( symbolt &old_symbol, - symbolt &new_symbol); + const symbolt &new_symbol); std::string expr_to_string( const namespacet &ns, diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 4755515200e..11037431b66 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -61,15 +61,16 @@ void get_symbols_rec( } } -/// A symbol is EXPORTED if it is a * non-static function with body that is not -/// extern inline * symbol used in an EXPORTED symbol * type used in an EXPORTED -/// symbol +/// Removes internal symbols from a symbol table +/// A symbol is EXPORTED if it is a +/// * non-static function with body that is not extern inline +/// * symbol used in an EXPORTED symbol +/// * type used in an EXPORTED symbol /// /// Read /// http://gcc.gnu.org/ml/gcc/2006-11/msg00006.html /// on "extern inline" -/// \par parameters: symbol table -/// \return symbol table, with internal symbols removed +/// \param symbol_table: symbol table to clean up void remove_internal_symbols( symbol_tablet &symbol_table) { @@ -148,16 +149,15 @@ void remove_internal_symbols( } // remove all that are _not_ exported! - for(symbol_tablet::symbolst::iterator + for(symbol_tablet::symbolst::const_iterator it=symbol_table.symbols.begin(); it!=symbol_table.symbols.end(); ) // no it++ { if(exported.find(it->first)==exported.end()) { - symbol_tablet::symbolst::iterator next=it; - ++next; - symbol_table.symbols.erase(it); + symbol_tablet::symbolst::const_iterator next=std::next(it); + symbol_table.erase(it); it=next; } else diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 2cacc49b032..4d96670cafd 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -31,13 +31,11 @@ bool static_lifetime_init( { namespacet ns(symbol_table); - symbol_tablet::symbolst::iterator s_it= - symbol_table.symbols.find(INITIALIZE_FUNCTION); - - if(s_it==symbol_table.symbols.end()) + symbol_tablet::opt_symbol_reft maybe_symbol= + symbol_table.get_writeable(INITIALIZE_FUNCTION); + if(!maybe_symbol) return false; - - symbolt &init_symbol=s_it->second; + symbolt &init_symbol=*maybe_symbol; init_symbol.value=code_blockt(); init_symbol.value.add_source_location()=source_location; @@ -104,12 +102,9 @@ bool static_lifetime_init( { // C standard 6.9.2, paragraph 5 // adjust the type to an array of size 1 - symbol_tablet::symbolst::iterator it= - symbol_table.symbols.find(identifier); - assert(it!=symbol_table.symbols.end()); - - it->second.type=type; - it->second.type.set(ID_size, from_integer(1, size_type())); + symbolt &symbol=*symbol_table.get_writeable(identifier); + symbol.type=type; + symbol.type.set(ID_size, from_integer(1, size_type())); } if(type.id()==ID_incomplete_struct || diff --git a/src/pointer-analysis/add_failed_symbols.cpp b/src/pointer-analysis/add_failed_symbols.cpp index e8da3c0d773..16e4131339e 100644 --- a/src/pointer-analysis/add_failed_symbols.cpp +++ b/src/pointer-analysis/add_failed_symbols.cpp @@ -22,12 +22,6 @@ irep_idt failed_symbol_id(const irep_idt &id) void add_failed_symbol(symbolt &symbol, symbol_tablet &symbol_table) { - if(!symbol.is_lvalue) - return; - - if(symbol.type.get(ID_C_failed_symbol)!="") - return; - if(symbol.type.id()==ID_pointer) { symbolt new_symbol; @@ -45,28 +39,32 @@ void add_failed_symbol(symbolt &symbol, symbol_tablet &symbol_table) if(new_symbol.type.id()==ID_pointer) add_failed_symbol(new_symbol, symbol_table); // recursive call - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); } } +void add_failed_symbol(const symbolt &symbol, symbol_tablet &symbol_table) +{ + if(!symbol.is_lvalue) + return; + + if(symbol.type.get(ID_C_failed_symbol)!="") + return; + + add_failed_symbol(*symbol_table.get_writeable(symbol.name), symbol_table); +} + void add_failed_symbols(symbol_tablet &symbol_table) { // the symbol table iterators are not stable, and // we are adding new symbols, this // is why we need a list of pointers - typedef std::list< ::symbolt *> symbol_listt; - symbol_listt symbol_list; - - Forall_symbols(it, symbol_table.symbols) - symbol_list.push_back(&(it->second)); + std::list symbol_list; + for(auto &named_symbol : symbol_table.symbols) + symbol_list.push_back(&(named_symbol.second)); - for(symbol_listt::const_iterator - it=symbol_list.begin(); - it!=symbol_list.end(); - it++) - { - add_failed_symbol(**it, symbol_table); - } + for(const symbolt *symbol : symbol_list) + add_failed_symbol(*symbol, symbol_table); } exprt get_failed_symbol( diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 87712e13bee..1323ee31b59 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -178,7 +178,7 @@ exprt value_set_dereferencet::dereference( failure_value=symbol.symbol_expr(); failure_value.set(ID_C_invalid_object, true); - new_symbol_table.move(symbol); + new_symbol_table.insert(std::move(symbol)); } valuet value; diff --git a/src/util/config.cpp b/src/util/config.cpp index 4048cfd417a..0e8f3d692c8 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1177,10 +1177,11 @@ void configt::set_object_bits_from_symbol_table( return; // set object_bits according to entry point language - if(symbol_table.has_symbol(CPROVER_PREFIX "_start")) + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(CPROVER_PREFIX "_start"); + if(maybe_symbol) { - const symbolt &entry_point_symbol= - symbol_table.lookup(CPROVER_PREFIX "_start"); + const symbolt &entry_point_symbol=*maybe_symbol; if(entry_point_symbol.mode==ID_java) bv_encoding.object_bits=java.default_object_bits; diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp index 71bb64b3ce9..e1795890721 100644 --- a/src/util/fresh_symbol.cpp +++ b/src/util/fresh_symbol.cpp @@ -39,27 +39,22 @@ symbolt &get_fresh_aux_symbol( symbol_tablet &symbol_table) { auxiliary_symbolt new_symbol; - symbolt *symbol_ptr; - do + // Loop until find a name that doesn't clash with a non-auxilliary symbol + while(true) { // Distinguish local variables with the same name new_symbol.base_name= - basename_prefix+ - "$"+ - std::to_string(++temporary_counter); + basename_prefix+"$"+std::to_string(++temporary_counter); if(name_prefix.empty()) new_symbol.name=new_symbol.base_name; else - new_symbol.name= - name_prefix+ - "::"+ - id2string(new_symbol.base_name); + new_symbol.name=name_prefix+"::"+id2string(new_symbol.base_name); new_symbol.type=type; new_symbol.location=source_location; new_symbol.mode=symbol_mode; + std::pair res=symbol_table.insert(std::move(new_symbol)); + if(res.second) + return res.first; } - while(symbol_table.move(new_symbol, symbol_ptr)); - - return *symbol_ptr; } diff --git a/src/util/language.cpp b/src/util/language.cpp index 6bd0211d4a4..62f77edc40b 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -86,7 +86,8 @@ void languaget::generate_opaque_method_stubs(symbol_tablet &symbol_table) { if(is_symbol_opaque_function(symbol_entry.second)) { - symbolt &symbol=symbol_entry.second; + symbolt &symbol= + *symbol_table.get_writeable(symbol_entry.second.name); generate_opaque_parameter_symbols(symbol, symbol_table); diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index c9e42ff5517..0cf07f24683 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -1,14 +1,9 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ +// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved. #include "symbol_table.h" #include +#include /// Add a new symbol to the symbol table /// \param symbol: The symbol to be added to the symbol table @@ -16,15 +11,46 @@ Author: Daniel Kroening, kroening@kroening.com /// there is a symbol with the same name already in the symbol table. bool symbol_tablet::add(const symbolt &symbol) { - if(!symbols.insert(std::pair(symbol.name, symbol)).second) - return true; - - symbol_base_map.insert( - std::pair(symbol.base_name, symbol.name)); - symbol_module_map.insert( - std::pair(symbol.module, symbol.name)); + return !insert(symbol).second; +} - return false; +/// Move or copy a new symbol to the symbol table +/// \remark: This is a nicer interface than move and achieves the same +/// result as both move and add +/// \param symbol: The symbol to be added to the symbol table - can be +/// moved or copied in +/// \return Returns a reference to the newly inserted symbol or to the +/// existing symbol if a symbol with the same name already exists in the +/// symbol table, along with a bool that is true if a new symbol was inserted. +std::pair symbol_tablet::insert(symbolt symbol) +{ + // Add the symbol to the table or retrieve existing symbol with the same name + std::pair result= + internal_symbols.emplace(symbol.name, std::move(symbol)); + symbolt &new_symbol=result.first->second; + if(result.second) + { + try + { + symbol_base_mapt::iterator base_result= + internal_symbol_base_map.emplace(new_symbol.base_name, new_symbol.name); + try + { + internal_symbol_module_map.emplace(new_symbol.module, new_symbol.name); + } + catch(...) + { + internal_symbol_base_map.erase(base_result); + throw; + } + } + catch(...) + { + internal_symbols.erase(result.first); + throw; + } + } + return std::make_pair(std::ref(new_symbol), result.second); } /// Move a symbol into the symbol table. If there is already a symbol with the @@ -44,65 +70,74 @@ bool symbol_tablet::add(const symbolt &symbol) /// location in the symbol table bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol) { - symbolt tmp; - - std::pair result= - symbols.insert(std::pair(symbol.name, tmp)); - - if(!result.second) + // Add an empty symbol to the table or retrieve existing symbol with same name + symbolt temp_symbol; + // This is not copying the symbol, this is passing the three required + // parameters to insert (just in the symbol) + temp_symbol.name=symbol.name; + temp_symbol.base_name=symbol.base_name; + temp_symbol.module=symbol.module; + std::pair result=insert(std::move(temp_symbol)); + if(result.second) { - new_symbol=&result.first->second; - return true; + // Move the provided symbol into the symbol table, this can't be done + // earlier + result.first.swap(symbol); } - - symbol_base_map.insert( - std::pair(symbol.base_name, symbol.name)); - symbol_module_map.insert( - std::pair(symbol.module, symbol.name)); - - result.first->second.swap(symbol); - new_symbol=&result.first->second; - - return false; + // Return the address of the symbol in the table + new_symbol=&result.first; + return !result.second; } /// Remove a symbol from the symbol table /// \param name: The name of the symbol to remove /// \return Returns a boolean indicating whether the process failed +/// i.e. false if the symbol was removed, or true if it didn't exist. bool symbol_tablet::remove(const irep_idt &name) { - symbolst::iterator entry=symbols.find(name); - + symbolst::const_iterator entry=symbols.find(name); if(entry==symbols.end()) return true; - - for(symbol_base_mapt::iterator - it=symbol_base_map.lower_bound(entry->second.base_name), - it_end=symbol_base_map.upper_bound(entry->second.base_name); - it!=it_end; - ++it) - if(it->second==name) - { - symbol_base_map.erase(it); - break; - } - - for(symbol_module_mapt::iterator - it=symbol_module_map.lower_bound(entry->second.module), - it_end=symbol_module_map.upper_bound(entry->second.module); - it!=it_end; - ++it) - if(it->second==name) - { - symbol_module_map.erase(it); - break; - } - - symbols.erase(entry); - + erase(entry); return false; } +/// Remove a symbol from the symbol table +/// \param entry: an iterator pointing at the symbol to remove +void symbol_tablet::erase(const symbolst::const_iterator &entry) +{ + const symbolt &symbol=entry->second; + + symbol_base_mapt::const_iterator + base_it=symbol_base_map.lower_bound(entry->second.base_name); + symbol_base_mapt::const_iterator + base_it_end=symbol_base_map.upper_bound(entry->second.base_name); + while(base_it!=base_it_end && base_it->second!=symbol.name) + ++base_it; + INVARIANT( + base_it!=base_it_end, + "symbolt::base_name should not be changed " + "after it is added to the symbol_table " + "(name: "+id2string(symbol.name)+", " + "current base_name: "+id2string(symbol.base_name)+")"); + internal_symbol_base_map.erase(base_it); + + symbol_module_mapt::const_iterator + module_it=symbol_module_map.lower_bound(entry->second.module), + module_it_end=symbol_module_map.upper_bound(entry->second.module); + while(module_it!=module_it_end && module_it->second!=symbol.name) + ++module_it; + INVARIANT( + module_it!=module_it_end, + "symbolt::module should not be changed " + "after it is added to the symbol_table " + "(name: "+id2string(symbol.name)+", " + "current module: "+id2string(symbol.module)+")"); + internal_symbol_module_map.erase(module_it); + + internal_symbols.erase(entry); +} + /// Print the contents of the symbol table /// \param out: The ostream to direct output to void symbol_tablet::show(std::ostream &out) const @@ -113,32 +148,28 @@ void symbol_tablet::show(std::ostream &out) const out << it->second; } -/// Find a symbol in the symbol table. Throws a string if no such symbol is -/// found. +/// Find a symbol in the symbol table for read-only access. /// \param identifier: The name of the symbol to look for -/// \return The symbol in the symbol table with the correct name -const symbolt &symbol_tablet::lookup(const irep_idt &identifier) const +/// \return an optional reference, set if found, unset otherwise. +symbol_tablet::opt_const_symbol_reft symbol_tablet::lookup( + const irep_idt &identifier) const { symbolst::const_iterator it=symbols.find(identifier); - if(it==symbols.end()) - throw "symbol "+id2string(identifier)+" not found"; - - return it->second; + return opt_const_symbol_reft(); + return std::ref(it->second); } -/// Find a symbol in the symbol table. Throws a string if no such symbol is -/// found. +/// Find a symbol in the symbol table for read-write access. /// \param identifier: The name of the symbol to look for -/// \return The symbol in the symbol table with the correct name -symbolt &symbol_tablet::lookup(const irep_idt &identifier) +/// \return an optional reference, set if found, unset otherwise. +symbol_tablet::opt_symbol_reft symbol_tablet::get_writeable( + const irep_idt &identifier) { - symbolst::iterator it=symbols.find(identifier); - + symbolst::iterator it=internal_symbols.find(identifier); if(it==symbols.end()) - throw "symbol "+id2string(identifier)+" not found"; - - return it->second; + return opt_symbol_reft(); + return std::ref(it->second); } /// Print the contents of the symbol table diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 9a1b0b7f95c..4fb920a179d 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -1,38 +1,26 @@ -/*******************************************************************\ +// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved. -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ +/// \file +/// Symbol table +/// \defgroup gr_symbol_table Symbol Table #ifndef CPROVER_UTIL_SYMBOL_TABLE_H #define CPROVER_UTIL_SYMBOL_TABLE_H -/*! \file util/symbol_table.h - * \brief Symbol table - * - * \author Daniel Kroening -*/ - -/*! \defgroup gr_symbol_table Symbol Table -*/ - #include #include #include +#include + #include "symbol.h" + #define forall_symbols(it, expr) \ for(symbol_tablet::symbolst::const_iterator it=(expr).begin(); \ it!=(expr).end(); ++it) -#define Forall_symbols(it, expr) \ - for(symbol_tablet::symbolst::iterator it=(expr).begin(); \ - it!=(expr).end(); ++it) - typedef std::multimap symbol_base_mapt; typedef std::multimap symbol_module_mapt; @@ -46,51 +34,102 @@ typedef std::multimap symbol_module_mapt; it_end=(expr).upper_bound(module); \ it!=it_end; ++it) -/*! \brief The symbol table - \ingroup gr_symbol_table -*/ + +/// \brief The symbol table +/// \ingroup gr_symbol_table class symbol_tablet { public: typedef std::unordered_map symbolst; + typedef optionalt> + opt_const_symbol_reft; + typedef optionalt> opt_symbol_reft; - symbolst symbols; - symbol_base_mapt symbol_base_map; - symbol_module_mapt symbol_module_map; +private: + symbolst internal_symbols; + symbol_base_mapt internal_symbol_base_map; + symbol_module_mapt internal_symbol_module_map; + +public: + const symbolst &symbols; + const symbol_base_mapt &symbol_base_map; + const symbol_module_mapt &symbol_module_map; + + symbol_tablet() + : symbols(internal_symbols), + symbol_base_map(internal_symbol_base_map), + symbol_module_map(internal_symbol_module_map) + { + } + + symbol_tablet(const symbol_tablet &other) + : internal_symbols(other.internal_symbols), + internal_symbol_base_map(other.internal_symbol_base_map), + internal_symbol_module_map(other.symbol_module_map), + symbols(internal_symbols), + symbol_base_map(internal_symbol_base_map), + symbol_module_map(internal_symbol_module_map) + { + } + + symbol_tablet &operator=(const symbol_tablet &other) + { + // Copy to temp and then call move assignment + return *this=symbol_tablet(other); + } + + symbol_tablet(symbol_tablet &&other) + : internal_symbols(std::move(other.internal_symbols)), + internal_symbol_base_map(std::move(other.internal_symbol_base_map)), + internal_symbol_module_map(std::move(other.symbol_module_map)), + symbols(internal_symbols), + symbol_base_map(internal_symbol_base_map), + symbol_module_map(internal_symbol_module_map) + { + } + + symbol_tablet &operator=(symbol_tablet &&other) + { + internal_symbols=std::move(other.internal_symbols); + internal_symbol_base_map=std::move(other.internal_symbol_base_map); + internal_symbol_module_map=std::move(other.symbol_module_map); + return *this; + } + + bool has_symbol(const irep_idt &name) const + { + return symbols.find(name)!=symbols.end(); + } + + opt_const_symbol_reft lookup(const irep_idt &identifier) const; + + opt_symbol_reft get_writeable(const irep_idt &identifier); bool add(const symbolt &symbol); - bool move(symbolt &symbol, symbolt *&new_symbol); + std::pair insert(symbolt symbol); - // this will go away, use add instead - bool move(symbolt &symbol) - { symbolt *new_symbol; return move(symbol, new_symbol); } + bool move(symbolt &symbol, symbolt *&new_symbol); void clear() { - symbols.clear(); - symbol_base_map.clear(); - symbol_module_map.clear(); + internal_symbols.clear(); + internal_symbol_base_map.clear(); + internal_symbol_module_map.clear(); } bool remove(const irep_idt &name); + void erase(const symbolst::const_iterator &entry); + void show(std::ostream &out) const; void swap(symbol_tablet &other) { - symbols.swap(other.symbols); - symbol_base_map.swap(other.symbol_base_map); - symbol_module_map.swap(other.symbol_module_map); - } - - bool has_symbol(const irep_idt &name) const - { - return symbols.find(name)!=symbols.end(); + internal_symbols.swap(other.internal_symbols); + internal_symbol_base_map.swap(other.internal_symbol_base_map); + internal_symbol_module_map.swap(other.internal_symbol_module_map); } - - symbolt &lookup(const irep_idt &identifier); - const symbolt &lookup(const irep_idt &identifier) const; }; std::ostream &operator << ( diff --git a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp index e8932306ee9..e328ac936a3 100644 --- a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp +++ b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp @@ -29,7 +29,7 @@ SCENARIO("java_bytecode_convert_abstract_class", THEN("The symbol type should be abstract") { - const symbolt &class_symbol=new_symbol_table.lookup("java::I"); + const symbolt &class_symbol=*new_symbol_table.lookup("java::I"); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); @@ -44,7 +44,7 @@ SCENARIO("java_bytecode_convert_abstract_class", load_java_class("A", "./java_bytecode/java_bytecode_convert_class"); THEN("The symbol type should be abstract") { - const symbolt &class_symbol=new_symbol_table.lookup("java::A"); + const symbolt &class_symbol=*new_symbol_table.lookup("java::A"); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); @@ -59,7 +59,7 @@ SCENARIO("java_bytecode_convert_abstract_class", load_java_class("C", "./java_bytecode/java_bytecode_convert_class"); THEN("The symbol type should not be abstract") { - const symbolt &class_symbol=new_symbol_table.lookup("java::C"); + const symbolt &class_symbol=*new_symbol_table.lookup("java::C"); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); @@ -77,7 +77,7 @@ SCENARIO("java_bytecode_convert_abstract_class", THEN("The symbol type should not be abstract") { const symbolt &class_symbol= - new_symbol_table.lookup("java::Implementor"); + *new_symbol_table.lookup("java::Implementor"); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); @@ -95,7 +95,7 @@ SCENARIO("java_bytecode_convert_abstract_class", THEN("The symbol type should not be abstract") { const symbolt &class_symbol= - new_symbol_table.lookup("java::Extender"); + *new_symbol_table.lookup("java::Extender"); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); diff --git a/unit/src/java_bytecode/load_java_class.cpp b/unit/src/java_bytecode/load_java_class.cpp index bfcb662ffa2..5956012b853 100644 --- a/unit/src/java_bytecode/load_java_class.cpp +++ b/unit/src/java_bytecode/load_java_class.cpp @@ -54,7 +54,7 @@ symbol_tablet load_java_class( // Verify that the class was loaded const std::string class_symbol_name="java::"+java_class_name; REQUIRE(new_symbol_table.has_symbol(class_symbol_name)); - const symbolt &class_symbol=new_symbol_table.lookup(class_symbol_name); + const symbolt &class_symbol=*new_symbol_table.lookup(class_symbol_name); REQUIRE(class_symbol.is_type); const typet &class_type=class_symbol.type; REQUIRE(class_type.id()==ID_struct);