Addressed reviewers comments

Author: cristina-david

regression/cbmc-java/exceptions19/exception_handler.class

@@ -17,7 +17,7 @@
         invokespecial java/lang/Exception.<init>()V
         athrow
       start:
-        nop
+        dup
       end:
         astore_1
         return

regression/cbmc-java/exceptions19/exception_handler.j

@@ -473,7 +473,8 @@ void java_bytecode_convert_methodt::convert(
 
   tmp_vars.clear();
   if((!m.is_abstract) && (!m.is_native))
-    method_symbol.value=convert_instructions(m, code_type);
+    method_symbol.value=convert_instructions(
+      m, code_type, method_symbol.name);
 
   // Replace the existing stub symbol with the real deal:
   const auto s_it=symbol_table.symbols.find(method.get_name());
@@ -1120,7 +1121,8 @@ Function: java_bytecode_convert_methodt::convert_instructions
 
 codet java_bytecode_convert_methodt::convert_instructions(
   const methodt &method,
-  const code_typet &method_type)
+  const code_typet &method_type,
+  const irep_idt &method_name)
 {
   const instructionst &instructions=method.instructions;
 
@@ -1316,17 +1318,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
         stack.clear();
         auxiliary_symbolt new_symbol;
         new_symbol.is_static_lifetime=true;
-        int file_name_length=
-          id2string(method.source_location.get_file()).size();
-        // remove the file extension
-        const std::string &file_name=
-          id2string(method.source_location.get_file()).
-             substr(0, file_name_length-5);
         // generate the name of the exceptional return variable
         const std::string &exceptional_var_name=
-          "java::"+file_name+"."+
-          id2string(method.name)+":"+
-          id2string(method.signature)+
+          id2string(method_name)+
           EXC_SUFFIX;
         new_symbol.base_name=exceptional_var_name;
         new_symbol.name=exceptional_var_name;
@@ -2397,10 +2391,6 @@ codet java_bytecode_convert_methodt::convert_instructions(
       results[1]=op[0];
       results[0]=op[1];
     }
-    else if(statement=="nop")
-    {
-      c=code_skipt();
-    }
     else
     {
       c=codet(statement);

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -214,7 +214,8 @@ class java_bytecode_convert_methodt:public messaget
 
   codet convert_instructions(
     const methodt &,
-    const code_typet &);
+    const code_typet &,
+    const irep_idt &);
 
   const bytecode_infot &get_bytecode_info(const irep_idt &statement);
 

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -594,7 +594,7 @@ bool java_entry_point(
     // add the exceptional return value
     auxiliary_symbolt exc_symbol;
     exc_symbol.mode=ID_C;
-    exc_symbol.is_static_lifetime=false;
+    exc_symbol.is_static_lifetime=true;
     exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX;
     exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX;
     exc_symbol.type=typet(ID_pointer, empty_typet());