Merge pull request #6400 from diffblue/goto_instruction_location_API

introduce API for goto_instructiont::source_location

Author: kroening

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -102,7 +102,7 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
     if(!nondet_expr.get_nullable())
       object_factory_parameters.min_null_tree_depth = 1;
 
-    const source_locationt &source_loc = target->source_location;
+    const source_locationt &source_loc = target->source_location();
 
     // Currently the code looks like this
     //   target: instruction containing op

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -246,7 +246,7 @@ void remove_exceptionst::instrument_exception_handler(
       instr_it,
       goto_programt::make_assignment(
         code_assignt(thrown_global_symbol, null_voidptr),
-        instr_it->source_location));
+        instr_it->source_location()));
 
     // add the assignment exc = @inflight_exception (before the null assignment)
     goto_program.insert_after(
@@ -255,7 +255,7 @@ void remove_exceptionst::instrument_exception_handler(
         code_assignt(
           thrown_exception_local,
           typecast_exprt(thrown_global_symbol, thrown_exception_local.type())),
-        instr_it->source_location));
+        instr_it->source_location()));
   }
 
   instr_it->turn_into_skip();
@@ -362,7 +362,7 @@ void remove_exceptionst::add_exception_dispatch_sequence(
         goto_programt::targett t_exc = goto_program.insert_after(
           instr_it,
           goto_programt::make_goto(
-            new_state_pc, true_exprt(), instr_it->source_location));
+            new_state_pc, true_exprt(), instr_it->source_location()));
 
         // use instanceof to check that this is the correct handler
         struct_tag_typet type(stack_catch[i][j].first);
@@ -385,13 +385,13 @@ void remove_exceptionst::add_exception_dispatch_sequence(
   }
 
   *default_dispatch = goto_programt::make_goto(
-    default_target, true_exprt(), instr_it->source_location);
+    default_target, true_exprt(), instr_it->source_location());
 
   // add dead instructions
   for(const auto &local : locals)
   {
     goto_program.insert_after(
-      instr_it, goto_programt::make_dead(local, instr_it->source_location));
+      instr_it, goto_programt::make_dead(local, instr_it->source_location()));
   }
 }
 
@@ -476,7 +476,7 @@ remove_exceptionst::instrument_function_call(
         goto_programt::make_goto(
           next_it,
           no_exception_currently_in_flight,
-          instr_it->source_location));
+          instr_it->source_location()));
 
       return instrumentation_resultt::ADDED_CODE_WITH_MAY_THROW;
     }

jbmc/src/java_bytecode/replace_java_nondet.cpp

@@ -274,28 +274,28 @@ static goto_programt::targett check_and_replace_target(
     const auto &nondet_var = target_instruction->return_value();
 
     side_effect_expr_nondett inserted_expr(
-      nondet_var.type(), target_instruction->source_location);
+      nondet_var.type(), target_instruction->source_location());
     inserted_expr.set_nullable(
       instr_info.get_nullable_type() ==
       nondet_instruction_infot::is_nullablet::TRUE);
     target_instruction->code_nonconst() = code_returnt(inserted_expr);
     target_instruction->code_nonconst().add_source_location() =
-      target_instruction->source_location;
+      target_instruction->source_location();
   }
   else if(target_instruction->is_assign())
   {
     // Assume that the LHS of *this* assignment is the actual nondet variable
     const auto &nondet_var = target_instruction->assign_lhs();
 
     side_effect_expr_nondett inserted_expr(
-      nondet_var.type(), target_instruction->source_location);
+      nondet_var.type(), target_instruction->source_location());
     inserted_expr.set_nullable(
       instr_info.get_nullable_type() ==
       nondet_instruction_infot::is_nullablet::TRUE);
     target_instruction->code_nonconst() =
       code_assignt(nondet_var, inserted_expr);
     target_instruction->code_nonconst().add_source_location() =
-      target_instruction->source_location;
+      target_instruction->source_location();
   }
 
   goto_program.update();

jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

@@ -148,7 +148,7 @@ SCENARIO(
 
           while(it->type != goto_program_instruction_typet::END_FUNCTION)
           {
-            const source_locationt &loc = it->source_location;
+            const source_locationt &loc = it->source_location();
             REQUIRE(loc != source_locationt::nil());
             REQUIRE_FALSE(loc.get_java_bytecode_index().empty());
             const auto new_index = loc.get_java_bytecode_index();

src/analyses/ai.cpp

@@ -45,8 +45,8 @@ void ai_baset::output(
 {
   forall_goto_program_instructions(i_it, goto_program)
   {
-    out << "**** " << i_it->location_number << " "
-        << i_it->source_location << "\n";
+    out << "**** " << i_it->location_number << " " << i_it->source_location()
+        << "\n";
 
     abstract_state_before(i_it)->output(out, *this, ns);
     out << "\n";
@@ -94,7 +94,7 @@ jsont ai_baset::output_json(
 
     json_objectt location{
       {"locationNumber", json_numbert(std::to_string(i_it->location_number))},
-      {"sourceLocation", json_stringt(i_it->source_location.as_string())},
+      {"sourceLocation", json_stringt(i_it->source_location().as_string())},
       {"abstractState", abstract_state_before(i_it)->output_json(*this, ns)},
       {"instruction", json_stringt(out.str())}};
 
@@ -142,7 +142,7 @@ xmlt ai_baset::output_xml(
     xmlt location(
       "",
       {{"location_number", std::to_string(i_it->location_number)},
-       {"source_location", i_it->source_location.as_string()}},
+       {"source_location", i_it->source_location().as_string()}},
       {abstract_state_before(i_it)->output_xml(*this, ns)});
 
     // Ideally we need output_instruction_xml

src/analyses/custom_bitvector_analysis.cpp

@@ -800,7 +800,7 @@ void custom_bitvector_analysist::check(
         const namespacet ns(goto_model.symbol_table);
         result = simplify_expr(std::move(tmp), ns);
 
-        description=i_it->source_location.get_comment();
+        description = i_it->source_location().get_comment();
       }
       else
         continue;
@@ -815,15 +815,15 @@ void custom_bitvector_analysist::check(
         else
           out << "UNKNOWN";
         out << "\">\n";
-        out << xml(i_it->source_location);
+        out << xml(i_it->source_location());
         out << "<description>"
             << description
             << "</description>\n";
         out << "</result>\n\n";
       }
       else
       {
-        out << i_it->source_location;
+        out << i_it->source_location();
         if(!description.empty())
           out << ", " << description;
         out << ": ";

src/analyses/dependence_graph.cpp

@@ -311,7 +311,7 @@ jsont dep_graph_domaint::output_json(
   {
     json_objectt link{
       {"locationNumber", json_numbert(std::to_string(cd->location_number))},
-      {"sourceLocation", json(cd->source_location)},
+      {"sourceLocation", json(cd->source_location())},
       {"type", json_stringt("control")}};
     graph.push_back(std::move(link));
   }
@@ -320,7 +320,7 @@ jsont dep_graph_domaint::output_json(
   {
     json_objectt link{
       {"locationNumber", json_numbert(std::to_string(dd->location_number))},
-      {"sourceLocation", json(dd->source_location)},
+      {"sourceLocation", json(dd->source_location())},
       {"type", json_stringt("data")}};
     graph.push_back(std::move(link));
   }

src/analyses/does_remove_const.cpp

@@ -46,7 +46,7 @@ std::pair<bool, source_locationt> does_remove_constt::operator()() const
     // const that the lhs
     if(!does_type_preserve_const_correctness(&lhs_type, &rhs_type))
     {
-      return {true, instruction.source_location};
+      return {true, instruction.source_location()};
     }
 
     if(does_expr_lose_const(instruction.assign_rhs()))

src/analyses/escape_analysis.cpp

@@ -420,7 +420,7 @@ void escape_analysist::insert_cleanup(
   bool is_object,
   const namespacet &ns)
 {
-  source_locationt source_location=location->source_location;
+  source_locationt source_location = location->source_location();
 
   for(const auto &cleanup : cleanup_functions)
   {

src/analyses/flow_insensitive_analysis.cpp

@@ -203,7 +203,7 @@ bool flow_insensitive_analysis_baset::do_function_call(
 
     goto_programt::targett r =
       temp.add(goto_programt::make_return(code_returnt(side_effect_expr_nondett(
-        l_call->call_lhs().type(), l_call->source_location))));
+        l_call->call_lhs().type(), l_call->source_location()))));
     r->location_number=0;
 
     goto_programt::targett t = temp.add(goto_programt::make_end_function());