Merge pull request #848 from cristina-david/bugfix/set-bytecode-index

Set the bytecode index for the instrumentation in goto_check.cpp

Author: peterschrammel

regression/cbmc-java/NullPointer1/test.desc

@@ -3,7 +3,7 @@ NullPointer1.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer1.java line 16 function java::NullPointer1.main:\(\[Ljava/lang/String;\)V$
+^  file NullPointer1.java line 16 function java::NullPointer1.main:\(\[Ljava/lang/String;\)V bytecode_index 9$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/NullPointer4/test.desc

@@ -3,7 +3,7 @@ NullPointer4.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V$
+^  file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V bytecode_index 4$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

src/analyses/goto_check.cpp

@@ -1820,6 +1820,10 @@ void goto_checkt::goto_check(
 
         if(it->source_location.get_column()!=irep_idt())
           i_it->source_location.set_column(it->source_location.get_column());
+
+        if(it->source_location.get_java_bytecode_index()!=irep_idt())
+          i_it->source_location.set_java_bytecode_index(
+            it->source_location.get_java_bytecode_index());
       }
 
       if(i_it->function==irep_idt())