java: function in location is now pretty name

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -856,7 +856,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     code_declt declare_cloned(local_symexpr);
 
     source_locationt location;
-    location.set_function(local_name);
+    location.set_function(local_symbol.pretty_name);
     side_effect_exprt java_new_array(
       ID_java_new_array, java_reference_type(symbol_type), location);
     dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -356,8 +356,6 @@ void java_bytecode_convert_method_lazy(
   method_symbol.name=method_identifier;
   method_symbol.base_name=m.base_name;
   method_symbol.mode=ID_java;
-  method_symbol.location=m.source_location;
-  method_symbol.location.set_function(method_identifier);
 
   if(m.is_public)
     member_type.set_access(ID_public);
@@ -408,6 +406,9 @@ void java_bytecode_convert_method_lazy(
                                 id2string(m.base_name) + signature_string;
   }
 
+  method_symbol.location=m.source_location;
+  method_symbol.location.set_function(method_symbol.pretty_name);
+
   // Load annotations
   if(!m.annotations.empty())
   {
@@ -589,7 +590,6 @@ void java_bytecode_convert_methodt::convert(
   // Update the symbol for the method
   method_symbol.mode=ID_java;
   method_symbol.location=m.source_location;
-  method_symbol.location.set_function(method_identifier);
 
   for(const auto &exception_name : m.throws_exception_table)
     method_type.add_throws_exceptions(exception_name);
@@ -617,6 +617,7 @@ void java_bytecode_convert_methodt::convert(
                                 id2string(m.base_name) + signature_string;
   }
 
+  method_symbol.location.set_function(method_symbol.pretty_name);
   method_symbol.type = method_type;
   current_method = method_symbol.name;
   method_has_this = method_type.has_this();

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -149,7 +149,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
 
   // synthetic source location that contains the opaque function name only
   source_locationt synthesized_source_location;
-  synthesized_source_location.set_function(symbol.name);
+  synthesized_source_location.set_function(symbol.pretty_name);
 
   // Initialize the return value or `this` parameter under construction.
   // Note symbol.type is required_type, but with write access