Skip to content

Commit 6351d3a

Browse files
kroeningkroening
authored
Merge pull request #6412 from diffblue/instructiont_type
introduce goto_programt::instructiont::type() and _nonconst()
2 parents fd10a22 + 13c2919 commit 6351d3a

Some content is hidden

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

47 files changed

+166
-151
lines changed

‎jbmc/src/java_bytecode/remove_exceptions.cpp

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -228,7 +228,7 @@ void remove_exceptionst::instrument_exception_handler(
228228
const goto_programt::targett &instr_it,
229229
bool may_catch)
230230
{
231-
PRECONDITION(instr_it->type==CATCH);
231+
PRECONDITION(instr_it->type() == CATCH);
232232

233233
if(may_catch)
234234
{
@@ -404,7 +404,7 @@ bool remove_exceptionst::instrument_throw(
404404
const remove_exceptionst::stack_catcht &stack_catch,
405405
const std::vector<symbol_exprt> &locals)
406406
{
407-
PRECONDITION(instr_it->type==THROW);
407+
PRECONDITION(instr_it->type() == THROW);
408408

409409
const exprt &exc_expr =
410410
uncaught_exceptions_domaint::get_exception_symbol(instr_it->get_code());
@@ -416,13 +416,11 @@ bool remove_exceptionst::instrument_throw(
416416
symbol_exprt exc_thrown =
417417
get_inflight_exception_global();
418418

419-
// add the assignment with the appropriate cast
420-
code_assignt assignment(
419+
// now turn the `throw' into an assignment with the appropriate cast
420+
*instr_it = goto_programt::make_assignment(
421421
exc_thrown,
422-
typecast_exprt(exc_expr, exc_thrown.type()));
423-
// now turn the `throw' into `assignment'
424-
instr_it->type=ASSIGN;
425-
instr_it->code_nonconst() = assignment;
422+
typecast_exprt(exc_expr, exc_thrown.type()),
423+
instr_it->source_location());
426424

427425
return true;
428426
}
@@ -437,7 +435,7 @@ remove_exceptionst::instrument_function_call(
437435
const stack_catcht &stack_catch,
438436
const std::vector<symbol_exprt> &locals)
439437
{
440-
PRECONDITION(instr_it->type==FUNCTION_CALL);
438+
PRECONDITION(instr_it->type() == FUNCTION_CALL);
441439

442440
// save the address of the next instruction
443441
goto_programt::targett next_it=instr_it;
@@ -512,7 +510,7 @@ void remove_exceptionst::instrument_exceptions(
512510
locals.push_back(instr_it->decl_symbol());
513511
}
514512
// Is it a handler push/pop or catch landing-pad?
515-
else if(instr_it->type==CATCH)
513+
else if(instr_it->type() == CATCH)
516514
{
517515
const irep_idt &statement = instr_it->get_code().get_statement();
518516
// Is it an exception landing pad (start of a catch block)?
@@ -584,12 +582,12 @@ void remove_exceptionst::instrument_exceptions(
584582
instr_it->turn_into_skip();
585583
did_something = true;
586584
}
587-
else if(instr_it->type==THROW)
585+
else if(instr_it->type() == THROW)
588586
{
589587
did_something = instrument_throw(
590588
function_identifier, goto_program, instr_it, stack_catch, locals);
591589
}
592-
else if(instr_it->type==FUNCTION_CALL)
590+
else if(instr_it->type() == FUNCTION_CALL)
593591
{
594592
instrumentation_resultt result =
595593
instrument_function_call(

‎jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ static goto_programt::const_targett interpret_classid_comparison(
8888

8989
while(pc != program.instructions.end())
9090
{
91-
if(pc->type == GOTO)
91+
if(pc->type() == GOTO)
9292
{
9393
exprt guard = pc->guard;
9494
guard = resolve_classid_test(guard, actual_class_id, ns);
@@ -105,7 +105,7 @@ static goto_programt::const_targett interpret_classid_comparison(
105105
return pc;
106106
}
107107
}
108-
else if(pc->type == SKIP)
108+
else if(pc->type() == SKIP)
109109
{
110110
++pc;
111111
}

‎jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ Author: Diffblue Limited.
1919
static bool is_expected_virtualmethod_call(
2020
const goto_programt::instructiont &instruction)
2121
{
22-
if(instruction.type != FUNCTION_CALL)
22+
if(instruction.type() != FUNCTION_CALL)
2323
return false;
2424
const auto &called_function = instruction.call_function();
2525
if(!can_cast_expr<class_method_descriptor_exprt>(called_function))

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ void check_function_call(
3030

3131
for(const auto &target : targets)
3232
{
33-
REQUIRE(target->type == goto_program_instruction_typet::FUNCTION_CALL);
33+
REQUIRE(target->type() == goto_program_instruction_typet::FUNCTION_CALL);
3434
REQUIRE(target->call_function().id() == ID_symbol);
3535
REQUIRE(
3636
to_symbol_expr(target->call_function()).get_identifier() ==
@@ -69,7 +69,7 @@ SCENARIO(
6969
{
7070
// There should be two guarded GOTOs with non-constant guards. One
7171
// branching for class C and one for class D or O.
72-
if(instruction.type == goto_program_instruction_typet::GOTO)
72+
if(instruction.type() == goto_program_instruction_typet::GOTO)
7373
{
7474
if(instruction.guard.id() == ID_equal)
7575
{
@@ -146,7 +146,7 @@ SCENARIO(
146146
{
147147
irep_idt current_index;
148148

149-
while(it->type != goto_program_instruction_typet::END_FUNCTION)
149+
while(it->type() != goto_program_instruction_typet::END_FUNCTION)
150150
{
151151
const source_locationt &loc = it->source_location();
152152
REQUIRE(loc != source_locationt::nil());
@@ -157,7 +157,7 @@ SCENARIO(
157157
{
158158
current_index = new_index;
159159
// instruction with a new bytecode index begins with ASSERT
160-
REQUIRE(it->type == goto_program_instruction_typet::ASSERT);
160+
REQUIRE(it->type() == goto_program_instruction_typet::ASSERT);
161161
// the assertion corresponds to a line coverage goal
162162
REQUIRE_FALSE(loc.get_basic_block_covered_lines().empty());
163163
}

‎src/analyses/custom_bitvector_analysis.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -283,7 +283,7 @@ void custom_bitvector_domaint::transform(
283283

284284
const goto_programt::instructiont &instruction=*from;
285285

286-
switch(instruction.type)
286+
switch(instruction.type())
287287
{
288288
case ASSIGN:
289289
assign_struct_rec(

‎src/analyses/escape_analysis.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -184,7 +184,7 @@ void escape_domaint::transform(
184184

185185
const goto_programt::instructiont &instruction=*from;
186186

187-
switch(instruction.type)
187+
switch(instruction.type())
188188
{
189189
case ASSIGN:
190190
{
@@ -460,7 +460,7 @@ void escape_analysist::instrument(
460460

461461
const goto_programt::instructiont &instruction=*i_it;
462462

463-
if(instruction.type == ASSIGN)
463+
if(instruction.type() == ASSIGN)
464464
{
465465
const exprt &assign_lhs = instruction.assign_lhs();
466466

@@ -469,7 +469,7 @@ void escape_analysist::instrument(
469469
insert_cleanup(
470470
gf_entry.second, i_it, assign_lhs, cleanup_functions, false, ns);
471471
}
472-
else if(instruction.type == DEAD)
472+
else if(instruction.type() == DEAD)
473473
{
474474
const auto &dead_symbol = instruction.dead_symbol();
475475

‎src/analyses/global_may_alias.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,7 @@ void global_may_alias_domaint::transform(
107107

108108
const goto_programt::instructiont &instruction=*from;
109109

110-
switch(instruction.type)
110+
switch(instruction.type())
111111
{
112112
case ASSIGN:
113113
{

‎src/analyses/goto_rw.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -756,7 +756,7 @@ void goto_rw(
756756
goto_programt::const_targett target,
757757
rw_range_sett &rw_set)
758758
{
759-
switch(target->type)
759+
switch(target->type())
760760
{
761761
case NO_INSTRUCTION_TYPE:
762762
case INCOMPLETE_GOTO:

‎src/analyses/interval_domain.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ void interval_domaint::transform(
6868
locationt to{trace_to->current_location()};
6969

7070
const goto_programt::instructiont &instruction=*from;
71-
switch(instruction.type)
71+
switch(instruction.type())
7272
{
7373
case DECL:
7474
havoc_rec(instruction.decl_symbol());

‎src/analyses/invariant_set_domain.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ void invariant_set_domaint::transform(
2525
locationt from_l(trace_from->current_location());
2626
locationt to_l(trace_to->current_location());
2727

28-
switch(from_l->type)
28+
switch(from_l->type())
2929
{
3030
case GOTO:
3131
{

‎src/analyses/local_bitvector_analysis.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -266,7 +266,7 @@ void local_bitvector_analysist::build()
266266
auto &loc_info_src=loc_infos[loc_nr];
267267
auto loc_info_dest=loc_infos[loc_nr];
268268

269-
switch(instruction.type)
269+
switch(instruction.type())
270270
{
271271
case ASSIGN:
272272
assign_lhs(

‎src/analyses/local_cfg.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ void local_cfgt::build(const goto_programt &goto_program)
3232
nodet &node=nodes[loc_nr];
3333
const goto_programt::instructiont &instruction=*node.t;
3434

35-
switch(instruction.type)
35+
switch(instruction.type())
3636
{
3737
case GOTO:
3838
if(!instruction.get_condition().is_true())

‎src/analyses/local_may_alias.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -371,7 +371,7 @@ void local_may_aliast::build(const goto_functiont &goto_function)
371371
const loc_infot &loc_info_src=loc_infos[loc_nr];
372372
loc_infot loc_info_dest=loc_infos[loc_nr];
373373

374-
switch(instruction.type)
374+
switch(instruction.type())
375375
{
376376
case ASSIGN:
377377
{

‎src/analyses/local_safe_pointers.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -108,7 +108,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
108108
instruction.location_number, checked_expressions);
109109
}
110110

111-
switch(instruction.type)
111+
switch(instruction.type())
112112
{
113113
// Instruction types that definitely don't write anything, and therefore
114114
// can't store a null pointer:

‎src/analyses/uncaught_exceptions_analysis.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ void uncaught_exceptions_domaint::transform(
6767
{
6868
const goto_programt::instructiont &instruction=*from;
6969

70-
switch(instruction.type)
70+
switch(instruction.type())
7171
{
7272
case THROW:
7373
{

‎src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ void variable_sensitivity_domaint::transform(
3636
#endif
3737

3838
const goto_programt::instructiont &instruction = *from;
39-
switch(instruction.type)
39+
switch(instruction.type())
4040
{
4141
case DECL:
4242
{
@@ -290,7 +290,7 @@ void variable_sensitivity_domaint::transform_function_call(
290290
ai_baset &ai,
291291
const namespacet &ns)
292292
{
293-
PRECONDITION(from->type == FUNCTION_CALL);
293+
PRECONDITION(from->type() == FUNCTION_CALL);
294294

295295
const exprt &function = from->call_function();
296296

‎src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -845,9 +845,7 @@ void disjunctive_polynomial_accelerationt::build_fixed()
845845
for(auto &instruction : fixed.instructions)
846846
{
847847
if(instruction.is_assert())
848-
{
849-
instruction.type = ASSUME;
850-
}
848+
instruction.turn_into_assume();
851849
}
852850

853851
// We're only interested in paths that loop back to the loop header.

‎src/goto-instrument/accelerate/sat_path_enumerator.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -196,7 +196,7 @@ void sat_path_enumeratort::build_fixed()
196196
for(auto &instruction : fixed.instructions)
197197
{
198198
if(instruction.is_assert())
199-
instruction.type = ASSUME;
199+
instruction.turn_into_assume();
200200
}
201201

202202
// We're only interested in paths that loop back to the loop header.

‎src/goto-instrument/contracts/contracts.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -261,8 +261,8 @@ void code_contractst::check_apply_loop_contracts(
261261
insert_before_swap_and_advance(goto_function.body, loop_end, havoc_code);
262262

263263
// change the back edge into assume(false) or assume(guard)
264-
loop_end->targets.clear();
265-
loop_end->type = ASSUME;
264+
loop_end->turn_into_assume();
265+
266266
if(loop_head->is_goto())
267267
loop_end->set_condition(false_exprt());
268268
else

‎src/goto-instrument/cover.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -311,7 +311,8 @@ static void instrument_cover_goals(
311311
{
312312
successor->turn_into_skip();
313313
}
314-
i_it->type = goto_program_instruction_typet::ASSUME;
314+
315+
i_it->turn_into_assume();
315316
}
316317
else
317318
{

‎src/goto-instrument/goto_program2code.cpp

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,9 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
138138
{
139139
assert(target!=goto_program.instructions.end());
140140

141-
if(target->type != ASSERT && !target->source_location().get_comment().empty())
141+
if(
142+
target->type() != ASSERT &&
143+
!target->source_location().get_comment().empty())
142144
{
143145
dest.add(code_skipt());
144146
dest.statements().back().add_source_location().set_comment(
@@ -158,7 +160,7 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
158160

159161
convert_labels(target, dest);
160162

161-
switch(target->type)
163+
switch(target->type())
162164
{
163165
case SKIP:
164166
case LOCATION:
@@ -764,10 +766,9 @@ bool goto_program2codet::set_block_end_points(
764766
continue;
765767

766768
// compute the block that belongs to this case
767-
for(goto_programt::const_targett case_end=it->case_start;
768-
case_end!=goto_program.instructions.end() &&
769-
case_end->type!=END_FUNCTION &&
770-
case_end!=upper_bound;
769+
for(goto_programt::const_targett case_end = it->case_start;
770+
case_end != goto_program.instructions.end() &&
771+
case_end->type() != END_FUNCTION && case_end != upper_bound;
771772
++case_end)
772773
{
773774
const auto &case_end_node = dominators.get_node(case_end);

‎src/goto-instrument/k_induction.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,7 @@ void k_inductiont::process_loop(
131131
{
132132
assert(t!=goto_function.body.instructions.end());
133133
if(t->is_assert())
134-
t->type=ASSUME;
134+
t->turn_into_assume();
135135
}
136136

137137
// assume the loop condition has become false

‎src/goto-instrument/points_to.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ bool points_tot::transform(const cfgt::nodet &e)
5656
bool result=false;
5757
const goto_programt::instructiont &instruction=*(e.PC);
5858

59-
switch(instruction.type)
59+
switch(instruction.type())
6060
{
6161
case SET_RETURN_VALUE:
6262
// TODO

0 commit comments

Comments
 (0)