@@ -382,11 +382,11 @@ void java_bytecode_convert_methodt::convert(
382
382
id2string (class_symbol.name )+" ." +id2string (m.name )+" :" +m.descriptor ;
383
383
method_id=method_identifier;
384
384
385
- const symbolt &old_sym =*symbol_table.lookup (method_identifier);
385
+ symbolt &method_symbol =*symbol_table.get_writeable (method_identifier);
386
386
387
387
// Obtain a std::vector of code_typet::parametert objects from the
388
388
// (function) type of the symbol
389
- typet member_type=old_sym .type ;
389
+ typet member_type=method_symbol .type ;
390
390
code_typet &code_type=to_code_type (member_type);
391
391
method_return_type=code_type.return_type ();
392
392
code_typet::parameterst ¶meters=code_type.parameters ();
@@ -527,10 +527,17 @@ void java_bytecode_convert_methodt::convert(
527
527
if (is_constructor (method))
528
528
method.set (ID_constructor, true );
529
529
530
- // we add the symbol for the method
531
- symbolt method_symbol;
532
- method_symbol.name =method.get_name ();
533
- method_symbol.base_name =method.get_base_name ();
530
+ // Check the fields that can't change are valid
531
+ INVARIANT (
532
+ method_symbol.name ==method.get_name (),
533
+ " Name of method symbol shouldn't change" );
534
+ INVARIANT (
535
+ method_symbol.base_name ==method.get_base_name (),
536
+ " Base name of method symbol shouldn't change" );
537
+ INVARIANT (
538
+ method_symbol.module .empty (),
539
+ " Method symbol shouldn't have module" );
540
+ // Update the symbol for the method
534
541
method_symbol.mode =ID_java;
535
542
method_symbol.location =m.source_location ;
536
543
method_symbol.location .set_function (method_identifier);
@@ -554,16 +561,6 @@ void java_bytecode_convert_methodt::convert(
554
561
method_has_this=code_type.has_this ();
555
562
if ((!m.is_abstract ) && (!m.is_native ))
556
563
method_symbol.value =convert_instructions (m, code_type, method_symbol.name );
557
-
558
- // Replace the existing stub symbol with the real deal:
559
- const auto s_it=symbol_table.symbols .find (method.get_name ());
560
- INVARIANT (
561
- s_it!=symbol_table.symbols .end (),
562
- " the symbol was there earlier on this function; it must be there now" );
563
- symbol_table.erase (s_it);
564
-
565
- // Insert the method symbol in the symbol table
566
- symbol_table.add (method_symbol);
567
564
}
568
565
569
566
const bytecode_infot &java_bytecode_convert_methodt::get_bytecode_info (
0 commit comments