Rename java bytecode index in output

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 bytecode_index 9$
+^  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 bytecode_index 4$
+^  file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V bytecode-index 4$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/enum1/test.desc

@@ -4,6 +4,6 @@ enum1.class
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
-^Unwinding loop java::enum1.<clinit>:\(\)V.0 iteration 5 \(6 max\) file enum1.java line 6 function java::enum1.<clinit>:\(\)V bytecode_index 78 thread 0$
+^Unwinding loop java::enum1.<clinit>:\(\)V.0 iteration 5 \(6 max\) file enum1.java line 6 function java::enum1.<clinit>:\(\)V bytecode-index 78 thread 0$
 --
 ^warning: ignoring

regression/cbmc-java/putstatic_source_location/test.desc

@@ -3,4 +3,4 @@ test.class
 --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-test\.java line 5 function java::test.main:\(\)V bytecode_index 1
+test\.java line 5 function java::test.main:\(\)V bytecode-index 1

regression/strings-smoke-tests/java_parseint_with_radix_knownbug/output

@@ -45,18 +45,18 @@ Runtime decision procedure: 0.386s
 [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.1] reference is null in *args: SUCCESS
 [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.2] reference is null in *new_tmp0: SUCCESS
 [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.3] reference is null in *new_tmp2: SUCCESS
-[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.1] assertion at file test_parseint_with_radix.java line 9 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 20: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.1] assertion at file test_parseint_with_radix.java line 9 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode-index 20: SUCCESS
 [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.1] Throw null: SUCCESS
 [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.4] reference is null in *new_tmp3: SUCCESS
-[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.2] assertion at file test_parseint_with_radix.java line 10 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 29: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.2] assertion at file test_parseint_with_radix.java line 10 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode-index 29: SUCCESS
 [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.2] Throw null: SUCCESS
 [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.5] reference is null in *args: SUCCESS
 [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.6] reference is null in *new_tmp4: SUCCESS
 [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.7] reference is null in *new_tmp6: SUCCESS
-[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.3] assertion at file test_parseint_with_radix.java line 16 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 52: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.3] assertion at file test_parseint_with_radix.java line 16 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode-index 52: SUCCESS
 [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.3] Throw null: SUCCESS
 [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.8] reference is null in *new_tmp7: SUCCESS
-[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.4] assertion at file test_parseint_with_radix.java line 17 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 61: SUCCESS
+[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.4] assertion at file test_parseint_with_radix.java line 17 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode-index 61: SUCCESS
 [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.4] Throw null: SUCCESS
 [pointer_dereference.7] reference is null in *this: SUCCESS
 [array-create-negative-size.1] Array size should be >= 0: SUCCESS

src/analyses/goto_check.cpp

@@ -1703,7 +1703,7 @@ void goto_checkt::goto_check(
         if(!it->source_location.get_column().empty())
           i_it->source_location.set_column(it->source_location.get_column());
 
-        if(it->source_location.get_java_bytecode_index()!=irep_idt())
+        if(!it->source_location.get_java_bytecode_index().empty())
           i_it->source_location.set_java_bytecode_index(
             it->source_location.get_java_bytecode_index());
       }

src/goto-instrument/cover.cpp

@@ -145,27 +145,27 @@ bool coverage_goalst::get_coverage_goals(
         // ensure minimal requirements for a goal entry
         PRECONDITION(
           (!each_goal["goal"].is_null()) ||
-          (!each_goal["sourceLocation"]["bytecode_index"].is_null()) ||
+          (!each_goal["sourceLocation"]["bytecodeIndex"].is_null()) ||
           (!each_goal["sourceLocation"]["file"].is_null() &&
            !each_goal["sourceLocation"]["function"].is_null() &&
            !each_goal["sourceLocation"]["line"].is_null()));
 
-        // check whether bytecode_index is provided for Java programs
+        // check whether bytecodeIndex is provided for Java programs
         if(mode==ID_java &&
-          each_goal["sourceLocation"]["bytecode_index"].is_null())
+          each_goal["sourceLocation"]["bytecodeIndex"].is_null())
         {
           messaget message(message_handler);
           message.error() << coverage_file
-                          << " file does not contain bytecode_index"
+                          << " file does not contain bytecodeIndex"
                           << messaget::eom;
           return true;
         }
 
-        if(!each_goal["sourceLocation"]["bytecode_index"].is_null())
+        if(!each_goal["sourceLocation"]["bytecodeIndex"].is_null())
         {
-          // get and set the bytecode_index
+          // get and set the bytecodeIndex
           irep_idt bytecode_index=
-            each_goal["sourceLocation"]["bytecode_index"].value;
+            each_goal["sourceLocation"]["bytecodeIndex"].value;
           source_location.set_java_bytecode_index(bytecode_index);
         }
 
@@ -1509,7 +1509,7 @@ bool instrument_cover_goals(
   if(cmdline.isset("existing-coverage"))
   {
     // get the mode to ensure invariants
-    // (e.g., bytecode_index for Java programs)
+    // (e.g., bytecodeIndex for Java programs)
     namespacet ns(symbol_table);
     const irep_idt &mode=ns.lookup(goto_functions.entry_point()).mode;
 

src/util/json_expr.cpp

@@ -95,7 +95,7 @@ json_objectt json(const source_locationt &location)
     result["function"]=json_stringt(id2string(location.get_function()));
 
   if(!location.get_java_bytecode_index().empty())
-    result["bytecode_index"]=
+    result["bytecodeIndex"]=
       json_stringt(id2string(location.get_java_bytecode_index()));
 
   return result;

src/util/source_location.cpp

@@ -56,7 +56,7 @@ std::string source_locationt::as_string(bool print_cwd) const
   {
     if(dest!="")
       dest+=' ';
-    dest+="bytecode_index "+id2string(bytecode);
+    dest+="bytecode-index "+id2string(bytecode);
   }
 
   return dest;