Prevent anonymous and named variables from clashing

Anonymous variables' names could previously clash with user-defined ones. This puts anonymous variables in a different namespace and gives them names guaranteed to be unique from each other based on their declaration program point.

Author: smowton

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();