Skip to content

Commit 268a0d0

Browse files
kroeningkroening
authored
Merge pull request #6400 from diffblue/goto_instruction_location_API
introduce API for goto_instructiont::source_location
2 parents 293748d + 8e14af7 commit 268a0d0

File tree

115 files changed

+720
-648
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

115 files changed

+720
-648
lines changed

‎jbmc/src/java_bytecode/convert_java_nondet.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
102102
if(!nondet_expr.get_nullable())
103103
object_factory_parameters.min_null_tree_depth = 1;
104104

105-
const source_locationt &source_loc = target->source_location;
105+
const source_locationt &source_loc = target->source_location();
106106

107107
// Currently the code looks like this
108108
// target: instruction containing op

‎jbmc/src/java_bytecode/remove_exceptions.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -246,7 +246,7 @@ void remove_exceptionst::instrument_exception_handler(
246246
instr_it,
247247
goto_programt::make_assignment(
248248
code_assignt(thrown_global_symbol, null_voidptr),
249-
instr_it->source_location));
249+
instr_it->source_location()));
250250

251251
// add the assignment exc = @inflight_exception (before the null assignment)
252252
goto_program.insert_after(
@@ -255,7 +255,7 @@ void remove_exceptionst::instrument_exception_handler(
255255
code_assignt(
256256
thrown_exception_local,
257257
typecast_exprt(thrown_global_symbol, thrown_exception_local.type())),
258-
instr_it->source_location));
258+
instr_it->source_location()));
259259
}
260260

261261
instr_it->turn_into_skip();
@@ -362,7 +362,7 @@ void remove_exceptionst::add_exception_dispatch_sequence(
362362
goto_programt::targett t_exc = goto_program.insert_after(
363363
instr_it,
364364
goto_programt::make_goto(
365-
new_state_pc, true_exprt(), instr_it->source_location));
365+
new_state_pc, true_exprt(), instr_it->source_location()));
366366

367367
// use instanceof to check that this is the correct handler
368368
struct_tag_typet type(stack_catch[i][j].first);
@@ -385,13 +385,13 @@ void remove_exceptionst::add_exception_dispatch_sequence(
385385
}
386386

387387
*default_dispatch = goto_programt::make_goto(
388-
default_target, true_exprt(), instr_it->source_location);
388+
default_target, true_exprt(), instr_it->source_location());
389389

390390
// add dead instructions
391391
for(const auto &local : locals)
392392
{
393393
goto_program.insert_after(
394-
instr_it, goto_programt::make_dead(local, instr_it->source_location));
394+
instr_it, goto_programt::make_dead(local, instr_it->source_location()));
395395
}
396396
}
397397

@@ -476,7 +476,7 @@ remove_exceptionst::instrument_function_call(
476476
goto_programt::make_goto(
477477
next_it,
478478
no_exception_currently_in_flight,
479-
instr_it->source_location));
479+
instr_it->source_location()));
480480

481481
return instrumentation_resultt::ADDED_CODE_WITH_MAY_THROW;
482482
}

‎jbmc/src/java_bytecode/replace_java_nondet.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -274,28 +274,28 @@ static goto_programt::targett check_and_replace_target(
274274
const auto &nondet_var = target_instruction->return_value();
275275

276276
side_effect_expr_nondett inserted_expr(
277-
nondet_var.type(), target_instruction->source_location);
277+
nondet_var.type(), target_instruction->source_location());
278278
inserted_expr.set_nullable(
279279
instr_info.get_nullable_type() ==
280280
nondet_instruction_infot::is_nullablet::TRUE);
281281
target_instruction->code_nonconst() = code_returnt(inserted_expr);
282282
target_instruction->code_nonconst().add_source_location() =
283-
target_instruction->source_location;
283+
target_instruction->source_location();
284284
}
285285
else if(target_instruction->is_assign())
286286
{
287287
// Assume that the LHS of *this* assignment is the actual nondet variable
288288
const auto &nondet_var = target_instruction->assign_lhs();
289289

290290
side_effect_expr_nondett inserted_expr(
291-
nondet_var.type(), target_instruction->source_location);
291+
nondet_var.type(), target_instruction->source_location());
292292
inserted_expr.set_nullable(
293293
instr_info.get_nullable_type() ==
294294
nondet_instruction_infot::is_nullablet::TRUE);
295295
target_instruction->code_nonconst() =
296296
code_assignt(nondet_var, inserted_expr);
297297
target_instruction->code_nonconst().add_source_location() =
298-
target_instruction->source_location;
298+
target_instruction->source_location();
299299
}
300300

301301
goto_program.update();

‎jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@ SCENARIO(
148148

149149
while(it->type != goto_program_instruction_typet::END_FUNCTION)
150150
{
151-
const source_locationt &loc = it->source_location;
151+
const source_locationt &loc = it->source_location();
152152
REQUIRE(loc != source_locationt::nil());
153153
REQUIRE_FALSE(loc.get_java_bytecode_index().empty());
154154
const auto new_index = loc.get_java_bytecode_index();

‎src/analyses/ai.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -45,8 +45,8 @@ void ai_baset::output(
4545
{
4646
forall_goto_program_instructions(i_it, goto_program)
4747
{
48-
out << "**** " << i_it->location_number << " "
49-
<< i_it->source_location << "\n";
48+
out << "**** " << i_it->location_number << " " << i_it->source_location()
49+
<< "\n";
5050

5151
abstract_state_before(i_it)->output(out, *this, ns);
5252
out << "\n";
@@ -94,7 +94,7 @@ jsont ai_baset::output_json(
9494

9595
json_objectt location{
9696
{"locationNumber", json_numbert(std::to_string(i_it->location_number))},
97-
{"sourceLocation", json_stringt(i_it->source_location.as_string())},
97+
{"sourceLocation", json_stringt(i_it->source_location().as_string())},
9898
{"abstractState", abstract_state_before(i_it)->output_json(*this, ns)},
9999
{"instruction", json_stringt(out.str())}};
100100

@@ -142,7 +142,7 @@ xmlt ai_baset::output_xml(
142142
xmlt location(
143143
"",
144144
{{"location_number", std::to_string(i_it->location_number)},
145-
{"source_location", i_it->source_location.as_string()}},
145+
{"source_location", i_it->source_location().as_string()}},
146146
{abstract_state_before(i_it)->output_xml(*this, ns)});
147147

148148
// Ideally we need output_instruction_xml

‎src/analyses/custom_bitvector_analysis.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -800,7 +800,7 @@ void custom_bitvector_analysist::check(
800800
const namespacet ns(goto_model.symbol_table);
801801
result = simplify_expr(std::move(tmp), ns);
802802

803-
description=i_it->source_location.get_comment();
803+
description = i_it->source_location().get_comment();
804804
}
805805
else
806806
continue;
@@ -815,15 +815,15 @@ void custom_bitvector_analysist::check(
815815
else
816816
out << "UNKNOWN";
817817
out << "\">\n";
818-
out << xml(i_it->source_location);
818+
out << xml(i_it->source_location());
819819
out << "<description>"
820820
<< description
821821
<< "</description>\n";
822822
out << "</result>\n\n";
823823
}
824824
else
825825
{
826-
out << i_it->source_location;
826+
out << i_it->source_location();
827827
if(!description.empty())
828828
out << ", " << description;
829829
out << ": ";

‎src/analyses/dependence_graph.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -311,7 +311,7 @@ jsont dep_graph_domaint::output_json(
311311
{
312312
json_objectt link{
313313
{"locationNumber", json_numbert(std::to_string(cd->location_number))},
314-
{"sourceLocation", json(cd->source_location)},
314+
{"sourceLocation", json(cd->source_location())},
315315
{"type", json_stringt("control")}};
316316
graph.push_back(std::move(link));
317317
}
@@ -320,7 +320,7 @@ jsont dep_graph_domaint::output_json(
320320
{
321321
json_objectt link{
322322
{"locationNumber", json_numbert(std::to_string(dd->location_number))},
323-
{"sourceLocation", json(dd->source_location)},
323+
{"sourceLocation", json(dd->source_location())},
324324
{"type", json_stringt("data")}};
325325
graph.push_back(std::move(link));
326326
}

‎src/analyses/does_remove_const.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ std::pair<bool, source_locationt> does_remove_constt::operator()() const
4646
// const that the lhs
4747
if(!does_type_preserve_const_correctness(&lhs_type, &rhs_type))
4848
{
49-
return {true, instruction.source_location};
49+
return {true, instruction.source_location()};
5050
}
5151

5252
if(does_expr_lose_const(instruction.assign_rhs()))

‎src/analyses/escape_analysis.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -420,7 +420,7 @@ void escape_analysist::insert_cleanup(
420420
bool is_object,
421421
const namespacet &ns)
422422
{
423-
source_locationt source_location=location->source_location;
423+
source_locationt source_location = location->source_location();
424424

425425
for(const auto &cleanup : cleanup_functions)
426426
{

‎src/analyses/flow_insensitive_analysis.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -203,7 +203,7 @@ bool flow_insensitive_analysis_baset::do_function_call(
203203

204204
goto_programt::targett r =
205205
temp.add(goto_programt::make_return(code_returnt(side_effect_expr_nondett(
206-
l_call->call_lhs().type(), l_call->source_location))));
206+
l_call->call_lhs().type(), l_call->source_location()))));
207207
r->location_number=0;
208208

209209
goto_programt::targett t = temp.add(goto_programt::make_end_function());

‎src/analyses/goto_check.cpp

Lines changed: 40 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1573,8 +1573,9 @@ void goto_checkt::add_guarded_property(
15731573
std::string source_expr_string;
15741574
get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
15751575

1576-
t->source_location.set_comment(comment + " in " + source_expr_string);
1577-
t->source_location.set_property_class(property_class);
1576+
t->source_location_nonconst().set_comment(
1577+
comment + " in " + source_expr_string);
1578+
t->source_location_nonconst().set_property_class(property_class);
15781579
}
15791580
}
15801581

@@ -1894,7 +1895,7 @@ void goto_checkt::goto_check(
18941895
goto_programt::instructiont &i=*it;
18951896

18961897
flag_resett flag_resetter;
1897-
const auto &pragmas = i.source_location.get_pragmas();
1898+
const auto &pragmas = i.source_location().get_pragmas();
18981899
for(const auto &d : pragmas)
18991900
{
19001901
if(d.first == "disable:bounds-check")
@@ -1956,12 +1957,13 @@ void goto_checkt::goto_check(
19561957
{
19571958
auto t = new_code.add(
19581959
enable_assert_to_assume
1959-
? goto_programt::make_assumption(false_exprt{}, i.source_location)
1960-
: goto_programt::make_assertion(false_exprt{}, i.source_location));
1960+
? goto_programt::make_assumption(false_exprt{}, i.source_location())
1961+
: goto_programt::make_assertion(
1962+
false_exprt{}, i.source_location()));
19611963

1962-
t->source_location.set_property_class("error label");
1963-
t->source_location.set_comment("error label "+label);
1964-
t->source_location.set("user-provided", true);
1964+
t->source_location_nonconst().set_property_class("error label");
1965+
t->source_location_nonconst().set_comment("error label " + label);
1966+
t->source_location_nonconst().set("user-provided", true);
19651967
}
19661968
}
19671969

@@ -2034,7 +2036,7 @@ void goto_checkt::goto_check(
20342036
not_eq_null,
20352037
"this is null on method invocation",
20362038
"pointer dereference",
2037-
i.source_location,
2039+
i.source_location(),
20382040
pointer,
20392041
guardt(true_exprt(), guard_manager));
20402042
}
@@ -2084,7 +2086,7 @@ void goto_checkt::goto_check(
20842086
not_eq_null,
20852087
"throwing null",
20862088
"pointer dereference",
2087-
i.source_location,
2089+
i.source_location(),
20882090
pointer,
20892091
guardt(true_exprt(), guard_manager));
20902092
}
@@ -2094,11 +2096,12 @@ void goto_checkt::goto_check(
20942096
}
20952097
else if(i.is_assert())
20962098
{
2097-
bool is_user_provided=i.source_location.get_bool("user-provided");
2099+
bool is_user_provided = i.source_location().get_bool("user-provided");
20982100

2099-
if((is_user_provided && !enable_assertions &&
2100-
i.source_location.get_property_class()!="error label") ||
2101-
(!is_user_provided && !enable_built_in_assertions))
2101+
if(
2102+
(is_user_provided && !enable_assertions &&
2103+
i.source_location().get_property_class() != "error label") ||
2104+
(!is_user_provided && !enable_built_in_assertions))
21022105
{
21032106
i.turn_into_skip();
21042107
did_something = true;
@@ -2126,13 +2129,13 @@ void goto_checkt::goto_check(
21262129
exprt address_of_expr = typecast_exprt::conditional_cast(
21272130
address_of_exprt(variable), lhs.type());
21282131
if_exprt rhs(
2129-
side_effect_expr_nondett(bool_typet(), i.source_location),
2132+
side_effect_expr_nondett(bool_typet(), i.source_location()),
21302133
std::move(address_of_expr),
21312134
lhs);
21322135
goto_programt::targett t =
21332136
new_code.add(goto_programt::make_assignment(
2134-
std::move(lhs), std::move(rhs), i.source_location));
2135-
t->code_nonconst().add_source_location() = i.source_location;
2137+
std::move(lhs), std::move(rhs), i.source_location()));
2138+
t->code_nonconst().add_source_location() = i.source_location();
21362139
}
21372140

21382141
if(
@@ -2148,13 +2151,13 @@ void goto_checkt::goto_check(
21482151
exprt alloca_result =
21492152
typecast_exprt::conditional_cast(variable, lhs.type());
21502153
if_exprt rhs(
2151-
side_effect_expr_nondett(bool_typet(), i.source_location),
2154+
side_effect_expr_nondett(bool_typet(), i.source_location()),
21522155
std::move(alloca_result),
21532156
lhs);
21542157
goto_programt::targett t =
21552158
new_code.add(goto_programt::make_assignment(
2156-
std::move(lhs), std::move(rhs), i.source_location));
2157-
t->code_nonconst().add_source_location() = i.source_location;
2159+
std::move(lhs), std::move(rhs), i.source_location()));
2160+
t->code_nonconst().add_source_location() = i.source_location();
21582161
}
21592162
}
21602163
}
@@ -2188,30 +2191,32 @@ void goto_checkt::goto_check(
21882191

21892192
for(auto &instruction : new_code.instructions)
21902193
{
2191-
if(instruction.source_location.is_nil())
2194+
if(instruction.source_location().is_nil())
21922195
{
2193-
instruction.source_location.id(irep_idt());
2196+
instruction.source_location_nonconst().id(irep_idt());
21942197

2195-
if(!it->source_location.get_file().empty())
2196-
instruction.source_location.set_file(it->source_location.get_file());
2198+
if(!it->source_location().get_file().empty())
2199+
instruction.source_location_nonconst().set_file(
2200+
it->source_location().get_file());
21972201

2198-
if(!it->source_location.get_line().empty())
2199-
instruction.source_location.set_line(it->source_location.get_line());
2202+
if(!it->source_location().get_line().empty())
2203+
instruction.source_location_nonconst().set_line(
2204+
it->source_location().get_line());
22002205

2201-
if(!it->source_location.get_function().empty())
2202-
instruction.source_location.set_function(
2203-
it->source_location.get_function());
2206+
if(!it->source_location().get_function().empty())
2207+
instruction.source_location_nonconst().set_function(
2208+
it->source_location().get_function());
22042209

2205-
if(!it->source_location.get_column().empty())
2210+
if(!it->source_location().get_column().empty())
22062211
{
2207-
instruction.source_location.set_column(
2208-
it->source_location.get_column());
2212+
instruction.source_location_nonconst().set_column(
2213+
it->source_location().get_column());
22092214
}
22102215

2211-
if(!it->source_location.get_java_bytecode_index().empty())
2216+
if(!it->source_location().get_java_bytecode_index().empty())
22122217
{
2213-
instruction.source_location.set_java_bytecode_index(
2214-
it->source_location.get_java_bytecode_index());
2218+
instruction.source_location_nonconst().set_java_bytecode_index(
2219+
it->source_location().get_java_bytecode_index());
22152220
}
22162221
}
22172222
}

‎src/analyses/interval_analysis.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ void instrument_intervals(
7979
goto_function.body.insert_before_swap(i_it);
8080
*t = goto_programt::make_assumption(conjunction(assertion));
8181
i_it++; // goes to original instruction
82-
t->source_location=i_it->source_location;
82+
t->source_location_nonconst() = i_it->source_location();
8383
}
8484
}
8585
}

‎src/analyses/local_bitvector_analysis.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -352,7 +352,7 @@ void local_bitvector_analysist::output(
352352

353353
for(const auto &instruction : goto_function.body.instructions)
354354
{
355-
out << "**** " << instruction.source_location << "\n";
355+
out << "**** " << instruction.source_location() << "\n";
356356

357357
const auto &loc_info=loc_infos[l];
358358

‎src/analyses/local_may_alias.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -471,7 +471,7 @@ void local_may_aliast::output(
471471

472472
for(const auto &instruction : goto_function.body.instructions)
473473
{
474-
out << "**** " << instruction.source_location << "\n";
474+
out << "**** " << instruction.source_location() << "\n";
475475

476476
const loc_infot &loc_info=loc_infos[l];
477477

0 commit comments

Comments
 (0)