introduce API for goto_instructiont::source_location

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

src/analyses/goto_check.cpp

@@ -1573,8 +1573,9 @@ void goto_checkt::add_guarded_property(
     std::string source_expr_string;
     get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
 
-    t->source_location.set_comment(comment + " in " + source_expr_string);
-    t->source_location.set_property_class(property_class);
+    t->source_location_nonconst().set_comment(
+      comment + " in " + source_expr_string);
+    t->source_location_nonconst().set_property_class(property_class);
   }
 }
 
@@ -1894,7 +1895,7 @@ void goto_checkt::goto_check(
     goto_programt::instructiont &i=*it;
 
     flag_resett flag_resetter;
-    const auto &pragmas = i.source_location.get_pragmas();
+    const auto &pragmas = i.source_location().get_pragmas();
     for(const auto &d : pragmas)
     {
       if(d.first == "disable:bounds-check")
@@ -1956,12 +1957,13 @@ void goto_checkt::goto_check(
       {
         auto t = new_code.add(
           enable_assert_to_assume
-            ? goto_programt::make_assumption(false_exprt{}, i.source_location)
-            : goto_programt::make_assertion(false_exprt{}, i.source_location));
+            ? goto_programt::make_assumption(false_exprt{}, i.source_location())
+            : goto_programt::make_assertion(
+                false_exprt{}, i.source_location()));
 
-        t->source_location.set_property_class("error label");
-        t->source_location.set_comment("error label "+label);
-        t->source_location.set("user-provided", true);
+        t->source_location_nonconst().set_property_class("error label");
+        t->source_location_nonconst().set_comment("error label " + label);
+        t->source_location_nonconst().set("user-provided", true);
       }
     }
 
@@ -2034,7 +2036,7 @@ void goto_checkt::goto_check(
             not_eq_null,
             "this is null on method invocation",
             "pointer dereference",
-            i.source_location,
+            i.source_location(),
             pointer,
             guardt(true_exprt(), guard_manager));
         }
@@ -2084,7 +2086,7 @@ void goto_checkt::goto_check(
           not_eq_null,
           "throwing null",
           "pointer dereference",
-          i.source_location,
+          i.source_location(),
           pointer,
           guardt(true_exprt(), guard_manager));
       }
@@ -2094,11 +2096,12 @@ void goto_checkt::goto_check(
     }
     else if(i.is_assert())
     {
-      bool is_user_provided=i.source_location.get_bool("user-provided");
+      bool is_user_provided = i.source_location().get_bool("user-provided");
 
-      if((is_user_provided && !enable_assertions &&
-          i.source_location.get_property_class()!="error label") ||
-         (!is_user_provided && !enable_built_in_assertions))
+      if(
+        (is_user_provided && !enable_assertions &&
+         i.source_location().get_property_class() != "error label") ||
+        (!is_user_provided && !enable_built_in_assertions))
       {
         i.turn_into_skip();
         did_something = true;
@@ -2126,13 +2129,13 @@ void goto_checkt::goto_check(
           exprt address_of_expr = typecast_exprt::conditional_cast(
             address_of_exprt(variable), lhs.type());
           if_exprt rhs(
-            side_effect_expr_nondett(bool_typet(), i.source_location),
+            side_effect_expr_nondett(bool_typet(), i.source_location()),
             std::move(address_of_expr),
             lhs);
           goto_programt::targett t =
             new_code.add(goto_programt::make_assignment(
-              std::move(lhs), std::move(rhs), i.source_location));
-          t->code_nonconst().add_source_location() = i.source_location;
+              std::move(lhs), std::move(rhs), i.source_location()));
+          t->code_nonconst().add_source_location() = i.source_location();
         }
 
         if(
@@ -2148,13 +2151,13 @@ void goto_checkt::goto_check(
           exprt alloca_result =
             typecast_exprt::conditional_cast(variable, lhs.type());
           if_exprt rhs(
-            side_effect_expr_nondett(bool_typet(), i.source_location),
+            side_effect_expr_nondett(bool_typet(), i.source_location()),
             std::move(alloca_result),
             lhs);
           goto_programt::targett t =
             new_code.add(goto_programt::make_assignment(
-              std::move(lhs), std::move(rhs), i.source_location));
-          t->code_nonconst().add_source_location() = i.source_location;
+              std::move(lhs), std::move(rhs), i.source_location()));
+          t->code_nonconst().add_source_location() = i.source_location();
         }
       }
     }
@@ -2188,30 +2191,32 @@ void goto_checkt::goto_check(
 
     for(auto &instruction : new_code.instructions)
     {
-      if(instruction.source_location.is_nil())
+      if(instruction.source_location().is_nil())
       {
-        instruction.source_location.id(irep_idt());
+        instruction.source_location_nonconst().id(irep_idt());
 
-        if(!it->source_location.get_file().empty())
-          instruction.source_location.set_file(it->source_location.get_file());
+        if(!it->source_location().get_file().empty())
+          instruction.source_location_nonconst().set_file(
+            it->source_location().get_file());
 
-        if(!it->source_location.get_line().empty())
-          instruction.source_location.set_line(it->source_location.get_line());
+        if(!it->source_location().get_line().empty())
+          instruction.source_location_nonconst().set_line(
+            it->source_location().get_line());
 
-        if(!it->source_location.get_function().empty())
-          instruction.source_location.set_function(
-            it->source_location.get_function());
+        if(!it->source_location().get_function().empty())
+          instruction.source_location_nonconst().set_function(
+            it->source_location().get_function());
 
-        if(!it->source_location.get_column().empty())
+        if(!it->source_location().get_column().empty())
         {
-          instruction.source_location.set_column(
-            it->source_location.get_column());
+          instruction.source_location_nonconst().set_column(
+            it->source_location().get_column());
         }
 
-        if(!it->source_location.get_java_bytecode_index().empty())
+        if(!it->source_location().get_java_bytecode_index().empty())
         {
-          instruction.source_location.set_java_bytecode_index(
-            it->source_location.get_java_bytecode_index());
+          instruction.source_location_nonconst().set_java_bytecode_index(
+            it->source_location().get_java_bytecode_index());
         }
       }
     }

src/analyses/interval_analysis.cpp

@@ -79,7 +79,7 @@ void instrument_intervals(
       goto_function.body.insert_before_swap(i_it);
       *t = goto_programt::make_assumption(conjunction(assertion));
       i_it++; // goes to original instruction
-      t->source_location=i_it->source_location;
+      t->source_location_nonconst() = i_it->source_location();
     }
   }
 }

src/analyses/local_bitvector_analysis.cpp

@@ -352,7 +352,7 @@ void local_bitvector_analysist::output(
 
   for(const auto &instruction : goto_function.body.instructions)
   {
-    out << "**** " << instruction.source_location << "\n";
+    out << "**** " << instruction.source_location() << "\n";
 
     const auto &loc_info=loc_infos[l];
 

src/analyses/local_may_alias.cpp

@@ -471,7 +471,7 @@ void local_may_aliast::output(
 
   for(const auto &instruction : goto_function.body.instructions)
   {
-    out << "**** " << instruction.source_location << "\n";
+    out << "**** " << instruction.source_location() << "\n";
 
     const loc_infot &loc_info=loc_infos[l];