diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index c4a91cff14f..a289ee14f58 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -134,7 +134,7 @@ class java_bytecode_convert_methodt:public messaget if(var.symbol_expr.get_identifier().empty()) { // an un-named local variable - irep_idt base_name="local"+id2string(number)+type_char; + irep_idt base_name="anonlocal::"+id2string(number)+type_char; irep_idt identifier=id2string(current_method)+"::"+id2string(base_name); symbol_exprt result(identifier, t); @@ -304,7 +304,9 @@ void java_bytecode_convert_methodt::convert( for(const auto & v : m.local_variable_table) { typet t=java_type_from_string(v.signature); - irep_idt identifier=id2string(method_identifier)+"::"+id2string(v.name); + std::ostringstream id_oss; + id_oss << method_identifier << "::" << v.start_pc << "::" << v.name; + irep_idt identifier(id_oss.str()); symbol_exprt result(identifier, t); result.set(ID_C_base_name, v.name); size_t number_index_entries = variables[v.index].size();