Skip to content

Commit 4adcfd8

Browse files
tautschnigtautschnig
authored
Merge pull request #3126 from diffblue/goto-instruction-function
remove goto_programt::instructiont::function member [blocks: #3113]
2 parents 8842667 + 8ddd9ba commit 4adcfd8

Some content is hidden

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

51 files changed

+22
-299
lines changed

‎jbmc/src/java_bytecode/remove_exceptions.cpp

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -237,7 +237,6 @@ void remove_exceptionst::instrument_exception_handler(
237237
t_null->code=code_assignt(
238238
thrown_global_symbol,
239239
null_voidptr);
240-
t_null->function=instr_it->function;
241240

242241
// add the assignment exc = @inflight_exception (before the null assignment)
243242
goto_programt::targett t_exc=goto_program.insert_after(instr_it);
@@ -246,7 +245,6 @@ void remove_exceptionst::instrument_exception_handler(
246245
t_exc->code=code_assignt(
247246
thrown_exception_local,
248247
typecast_exprt(thrown_global_symbol, thrown_exception_local.type()));
249-
t_exc->function=instr_it->function;
250248
}
251249
instr_it->make_skip();
252250
}
@@ -352,7 +350,6 @@ void remove_exceptionst::add_exception_dispatch_sequence(
352350
goto_programt::targett t_exc=goto_program.insert_after(instr_it);
353351
t_exc->make_goto(new_state_pc);
354352
t_exc->source_location=instr_it->source_location;
355-
t_exc->function=instr_it->function;
356353

357354
// use instanceof to check that this is the correct handler
358355
struct_tag_typet type(stack_catch[i][j].first);
@@ -377,7 +374,6 @@ void remove_exceptionst::add_exception_dispatch_sequence(
377374

378375
default_dispatch->make_goto(default_target);
379376
default_dispatch->source_location=instr_it->source_location;
380-
default_dispatch->function=instr_it->function;
381377

382378
// add dead instructions
383379
for(const auto &local : locals)
@@ -386,7 +382,6 @@ void remove_exceptionst::add_exception_dispatch_sequence(
386382
t_dead->make_dead();
387383
t_dead->code=code_deadt(local);
388384
t_dead->source_location=instr_it->source_location;
389-
t_dead->function=instr_it->function;
390385
}
391386
}
392387

@@ -466,7 +461,6 @@ bool remove_exceptionst::instrument_function_call(
466461
goto_programt::targett t_null=goto_program.insert_after(instr_it);
467462
t_null->make_goto(next_it);
468463
t_null->source_location=instr_it->source_location;
469-
t_null->function=instr_it->function;
470464
t_null->guard=no_exception_currently_in_flight;
471465
}
472466

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -840,9 +840,6 @@ void jbmc_parse_optionst::process_goto_function(
840840
function.compute_location_numbers();
841841
goto_function.body.compute_loop_numbers();
842842
}
843-
844-
// update the function member in each instruction
845-
function.update_instructions_function();
846843
}
847844
}
848845

‎jbmc/src/jdiff/java_syntactic_diff.cpp

Lines changed: 0 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -75,21 +75,6 @@ bool java_syntactic_difft::operator()()
7575
modified_functions.insert(it->first);
7676
continue;
7777
}
78-
79-
goto_programt::instructionst::const_iterator i_it1 =
80-
it->second.body.instructions.begin();
81-
for(goto_programt::instructionst::const_iterator
82-
i_it2 = f_it->second.body.instructions.begin();
83-
i_it1 != it->second.body.instructions.end() &&
84-
i_it2 != f_it->second.body.instructions.end();
85-
++i_it1, ++i_it2)
86-
{
87-
if(i_it1->function != i_it2->function)
88-
{
89-
modified_functions.insert(it->first);
90-
break;
91-
}
92-
}
9378
}
9479
forall_goto_functions(it, goto_model2.goto_functions)
9580
{

‎src/analyses/flow_insensitive_analysis.cpp

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -212,12 +212,9 @@ bool flow_insensitive_analysis_baset::do_function_call(
212212

213213
goto_programt::targett r = temp.add(goto_programt::make_return(code_returnt(
214214
side_effect_expr_nondett(code.lhs().type(), l_call->source_location))));
215-
216-
r->function=f_it->first;
217215
r->location_number=0;
218216

219217
goto_programt::targett t = temp.add(goto_programt::make_end_function());
220-
t->function=f_it->first;
221218
t->location_number=1;
222219

223220
locationt l_next=l_call; l_next++;
@@ -242,9 +239,6 @@ bool flow_insensitive_analysis_baset::do_function_call(
242239
// get the state at the beginning of the function
243240
locationt l_begin=goto_function.body.instructions.begin();
244241

245-
DATA_INVARIANT(
246-
l_begin->function == f_it->first, "function names have to match");
247-
248242
// do the edge from the call site to the beginning of the function
249243
new_data =
250244
state.transform(ns, calling_function, l_call, f_it->first, l_begin);

‎src/analyses/goto_check.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1900,9 +1900,6 @@ void goto_checkt::goto_check(
19001900
i_it->source_location.set_java_bytecode_index(
19011901
it->source_location.get_java_bytecode_index());
19021902
}
1903-
1904-
if(i_it->function.empty())
1905-
i_it->function=it->function;
19061903
}
19071904

19081905
// insert new instructions -- make sure targets are not moved

‎src/analyses/interval_analysis.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,6 @@ void instrument_intervals(
8282
t->make_assumption(conjunction(assertion));
8383
i_it++; // goes to original instruction
8484
t->source_location=i_it->source_location;
85-
t->function=i_it->function;
8685
}
8786
}
8887
}

‎src/assembler/remove_asm.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -493,9 +493,6 @@ void remove_asmt::process_function(
493493
it->make_skip();
494494
did_something = true;
495495

496-
for(auto &instruction : tmp_dest.instructions)
497-
instruction.function = it->function;
498-
499496
goto_programt::targett next = it;
500497
next++;
501498

‎src/goto-diff/syntactic_diff.cpp

Lines changed: 0 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -74,21 +74,6 @@ bool syntactic_difft::operator()()
7474
modified_functions.insert(it->first);
7575
continue;
7676
}
77-
78-
goto_programt::instructionst::const_iterator
79-
i_it1=it->second.body.instructions.begin();
80-
for(goto_programt::instructionst::const_iterator
81-
i_it2=f_it->second.body.instructions.begin();
82-
i_it1!=it->second.body.instructions.end() &&
83-
i_it2!=f_it->second.body.instructions.end();
84-
++i_it1, ++i_it2)
85-
{
86-
if(i_it1->function != i_it2->function)
87-
{
88-
modified_functions.insert(it->first);
89-
break;
90-
}
91-
}
9277
}
9378
forall_goto_functions(it, goto_model2.goto_functions)
9479
{

‎src/goto-diff/unified_diff.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -392,7 +392,7 @@ bool unified_difft::instructions_equal(
392392
const goto_programt::instructiont &ins1,
393393
const goto_programt::instructiont &ins2)
394394
{
395-
return ins1.equals(ins2) && ins1.function == ins2.function &&
395+
return ins1.equals(ins2) &&
396396
(ins1.targets.empty() ||
397397
instructions_equal(*ins1.get_target(), *ins2.get_target()));
398398
}

‎src/goto-instrument/branch.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,15 +54,13 @@ void branch(
5454
goto_programt::targett t1=body.insert_after(i_it);
5555
t1->make_function_call(
5656
function_to_call(goto_model.symbol_table, id, "taken"));
57-
t1->function=f_it->first;
5857

5958
goto_programt::targett t2=body.insert_after(t1);
6059
t2->make_goto(i_it->get_target());
6160

6261
goto_programt::targett t3=body.insert_after(t2);
6362
t3->make_function_call(
6463
function_to_call(goto_model.symbol_table, id, "not-taken"));
65-
t3->function=f_it->first;
6664
i_it->targets.clear();
6765
i_it->targets.push_back(t3);
6866
}

‎src/goto-instrument/code_contracts.cpp

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,6 @@ static void check_apply_invariants(
112112
{
113113
goto_programt::targett a=havoc_code.add_instruction(ASSERT);
114114
a->guard=invariant;
115-
a->function=loop_head->function;
116115
a->source_location=loop_head->source_location;
117116
a->source_location.set_comment("Loop invariant violated before entry");
118117
}
@@ -124,7 +123,6 @@ static void check_apply_invariants(
124123
{
125124
goto_programt::targett assume=havoc_code.add_instruction(ASSUME);
126125
assume->guard=invariant;
127-
assume->function=loop_head->function;
128126
assume->source_location=loop_head->source_location;
129127
}
130128

@@ -135,7 +133,6 @@ static void check_apply_invariants(
135133
jump->guard =
136134
side_effect_expr_nondett(bool_typet(), loop_head->source_location);
137135
jump->targets.push_back(loop_end);
138-
jump->function=loop_head->function;
139136
}
140137

141138
// Now havoc at the loop head. Use insert_swap to
@@ -146,7 +143,6 @@ static void check_apply_invariants(
146143
{
147144
goto_programt::instructiont a(ASSERT);
148145
a.guard=invariant;
149-
a.function=loop_end->function;
150146
a.source_location=loop_end->source_location;
151147
a.source_location.set_comment("Loop invariant not preserved");
152148
goto_function.body.insert_before_swap(loop_end, a);
@@ -216,7 +212,6 @@ void code_contractst::apply_contract(
216212
{
217213
goto_programt::instructiont a(ASSERT);
218214
a.guard=requires;
219-
a.function=target->function;
220215
a.source_location=target->source_location;
221216

222217
goto_program.insert_before_swap(target, a);
@@ -295,7 +290,6 @@ void code_contractst::add_contract_check(
295290
// build skip so that if(nondet) can refer to it
296291
goto_programt tmp_skip;
297292
goto_programt::targett skip=tmp_skip.add_instruction(SKIP);
298-
skip->function=dest.instructions.front().function;
299293
skip->source_location=ensures.source_location();
300294

301295
goto_programt check;
@@ -304,7 +298,6 @@ void code_contractst::add_contract_check(
304298
goto_programt::targett g=check.add_instruction();
305299
g->make_goto(
306300
skip, side_effect_expr_nondett(bool_typet(), skip->source_location));
307-
g->function=skip->function;
308301
g->source_location=skip->source_location;
309302

310303
// prepare function call including all declarations
@@ -315,7 +308,6 @@ void code_contractst::add_contract_check(
315308
if(gf.type.return_type()!=empty_typet())
316309
{
317310
goto_programt::targett d=check.add_instruction(DECL);
318-
d->function=skip->function;
319311
d->source_location=skip->source_location;
320312

321313
symbol_exprt r=
@@ -336,7 +328,6 @@ void code_contractst::add_contract_check(
336328
++p_it)
337329
{
338330
goto_programt::targett d=check.add_instruction(DECL);
339-
d->function=skip->function;
340331
d->source_location=skip->source_location;
341332

342333
symbol_exprt p=
@@ -358,7 +349,6 @@ void code_contractst::add_contract_check(
358349
{
359350
goto_programt::targett a=check.add_instruction();
360351
a->make_assumption(requires);
361-
a->function=skip->function;
362352
a->source_location=requires.source_location();
363353

364354
// rewrite any use of parameters
@@ -368,13 +358,11 @@ void code_contractst::add_contract_check(
368358
// ret=function(parameter1, ...)
369359
goto_programt::targett f=check.add_instruction();
370360
f->make_function_call(call);
371-
f->function=skip->function;
372361
f->source_location=skip->source_location;
373362

374363
// assert(ensures)
375364
goto_programt::targett a=check.add_instruction();
376365
a->make_assertion(ensures);
377-
a->function=skip->function;
378366
a->source_location=ensures.source_location();
379367

380368
// rewrite any use of __CPROVER_return_value
@@ -383,7 +371,6 @@ void code_contractst::add_contract_check(
383371
// assume(false)
384372
goto_programt::targett af=check.add_instruction();
385373
af->make_assumption(false_exprt());
386-
af->function=skip->function;
387374
af->source_location=ensures.source_location();
388375

389376
// prepend the new code to dest

‎src/goto-instrument/cover_instrument.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,6 @@ class cover_instrumenter_baset
7474
t->source_location.set(ID_coverage_criterion, coverage_criterion);
7575
t->source_location.set_property_class(property_class);
7676
t->source_location.set_function(function_id);
77-
t->function = function_id;
7877
}
7978

8079
bool is_non_cover_assertion(goto_programt::const_targett t) const

‎src/goto-instrument/cover_instrument_mcdc.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -667,7 +667,6 @@ void cover_mcdc_instrumentert::instrument(
667667
i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
668668
i_it->source_location.set_property_class(property_class);
669669
i_it->source_location.set_function(function_id);
670-
i_it->function = function_id;
671670

672671
std::string comment_f = description + " `" + p_string + "' false";
673672
goto_program.insert_before_swap(i_it);
@@ -677,7 +676,6 @@ void cover_mcdc_instrumentert::instrument(
677676
i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
678677
i_it->source_location.set_property_class(property_class);
679678
i_it->source_location.set_function(function_id);
680-
i_it->function = function_id;
681679
}
682680

683681
std::set<exprt> controlling;
@@ -704,7 +702,6 @@ void cover_mcdc_instrumentert::instrument(
704702
i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
705703
i_it->source_location.set_property_class(property_class);
706704
i_it->source_location.set_function(function_id);
707-
i_it->function = function_id;
708705
}
709706

710707
for(std::size_t i = 0; i < both.size() * 2 + controlling.size(); i++)

‎src/goto-instrument/cover_instrument_other.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -86,5 +86,4 @@ void cover_instrument_end_of_function(
8686
if_it->source_location.set_comment(comment);
8787
if_it->source_location.set_property_class("reachability_constraint");
8888
if_it->source_location.set_function(function_id);
89-
if_it->function = function_id;
9089
}

‎src/goto-instrument/function.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,6 @@ void function_enter(
9191
body.insert_before(body.instructions.begin());
9292
t->make_function_call(
9393
function_to_call(goto_model.symbol_table, id, f_it->first));
94-
t->function=f_it->first;
9594
}
9695
}
9796

@@ -123,7 +122,6 @@ void function_exit(
123122
if(i_it->is_return())
124123
{
125124
goto_programt::instructiont call;
126-
call.function=f_it->first;
127125
call.make_function_call(
128126
function_to_call(goto_model.symbol_table, id, f_it->first));
129127
body.insert_before_swap(i_it, call);
@@ -154,7 +152,6 @@ void function_exit(
154152
goto_programt::instructiont call;
155153
call.make_function_call(
156154
function_to_call(goto_model.symbol_table, id, f_it->first));
157-
call.function=f_it->first;
158155
body.insert_before_swap(last, call);
159156
}
160157
}

‎src/goto-instrument/generate_function_bodies.cpp

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,6 @@ class assume_false_generate_function_bodiest : public generate_function_bodiest
7676
// NOLINTNEXTLINE
7777
auto add_instruction = [&]() {
7878
auto instruction = function.body.add_instruction();
79-
instruction->function = function_name;
8079
instruction->source_location = function_symbol.location;
8180
return instruction;
8281
};
@@ -99,7 +98,6 @@ class assert_false_generate_function_bodiest : public generate_function_bodiest
9998
// NOLINTNEXTLINE
10099
auto add_instruction = [&]() {
101100
auto instruction = function.body.add_instruction();
102-
instruction->function = function_name;
103101
instruction->source_location = function_symbol.location;
104102
instruction->source_location.set_function(function_name);
105103
return instruction;
@@ -130,7 +128,6 @@ class assert_false_then_assume_false_generate_function_bodiest
130128
// NOLINTNEXTLINE
131129
auto add_instruction = [&]() {
132130
auto instruction = function.body.add_instruction();
133-
instruction->function = function_name;
134131
instruction->source_location = function_symbol.location;
135132
instruction->source_location.set_function(function_name);
136133
return instruction;
@@ -212,7 +209,6 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
212209
// NOLINTNEXTLINE
213210
auto add_instruction = [&]() {
214211
auto instruction = function.body.add_instruction();
215-
instruction->function = function_name;
216212
instruction->source_location = function_symbol.location;
217213
return instruction;
218214
};

‎src/goto-instrument/interrupt.cpp

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -110,11 +110,9 @@ static void interrupt(
110110
t_goto->make_goto(t_orig);
111111
t_goto->source_location=source_location;
112112
t_goto->guard = side_effect_expr_nondett(bool_typet(), source_location);
113-
t_goto->function=original_instruction.function;
114113

115114
t_call->make_function_call(isr_call);
116115
t_call->source_location=source_location;
117-
t_call->function=original_instruction.function;
118116

119117
t_orig->swap(original_instruction);
120118

@@ -138,11 +136,9 @@ static void interrupt(
138136
t_goto->make_goto(t_orig);
139137
t_goto->source_location=source_location;
140138
t_goto->guard = side_effect_expr_nondett(bool_typet(), source_location);
141-
t_goto->function=i_it->function;
142139

143140
t_call->make_function_call(isr_call);
144141
t_call->source_location=source_location;
145-
t_call->function=i_it->function;
146142

147143
i_it=t_call; // the for loop already counts us up
148144
}

0 commit comments

Comments
 (0)