Skip to content

Commit 6c901b6

Browse files
committed
Avoid codet construction without a statement set
The default constructor for codet is deprecated.
1 parent 3120f0f commit 6c901b6

10 files changed

+42
-53
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1206,7 +1206,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
12061206
}
12071207
}
12081208

1209-
codet catch_instruction;
1209+
optionalt<codet> catch_instruction;
12101210

12111211
if(catch_type!=typet())
12121212
{
@@ -1223,8 +1223,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
12231223
"caught_exception",
12241224
java_reference_type(catch_type));
12251225
stack.push_back(catch_var);
1226-
code_landingpadt catch_statement(catch_var);
1227-
catch_instruction=catch_statement;
1226+
catch_instruction = code_landingpadt(catch_var);
12281227
}
12291228

12301229
exprt::operandst op = pop(stmt_bytecode_info.pop);
@@ -1677,10 +1676,10 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
16771676
// Finally if this is the beginning of a catch block (already determined
16781677
// before the big bytecode switch), insert the exception 'landing pad'
16791678
// instruction before the actual instruction:
1680-
if(catch_instruction!=codet())
1679+
if(catch_instruction.has_value())
16811680
{
16821681
c.make_block();
1683-
c.operands().insert(c.operands().begin(), catch_instruction);
1682+
c.operands().insert(c.operands().begin(), *catch_instruction);
16841683
}
16851684

16861685
if(!i_it->source_location.get_line().empty())

src/ansi-c/c_typecheck_base.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -648,7 +648,7 @@ void c_typecheck_baset::typecheck_declaration(
648648
// mark as 'already typechecked'
649649
make_already_typechecked(declaration.type());
650650

651-
codet contract;
651+
irept contract;
652652

653653
{
654654
exprt spec_requires=
@@ -738,15 +738,15 @@ void c_typecheck_baset::typecheck_declaration(
738738
// available
739739
symbolt &new_symbol=*symbol_table.get_writeable(identifier);
740740

741-
typecheck_spec_expr(contract, ID_C_spec_requires);
741+
typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_requires);
742742

743743
typet ret_type=empty_typet();
744744
if(new_symbol.type.id()==ID_code)
745745
ret_type=to_code_type(new_symbol.type).return_type();
746746
assert(parameter_map.empty());
747747
if(ret_type.id()!=ID_empty)
748748
parameter_map[CPROVER_PREFIX "return_value"] = ret_type;
749-
typecheck_spec_expr(contract, ID_C_spec_ensures);
749+
typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_ensures);
750750
parameter_map.clear();
751751

752752
if(contract.find(ID_C_spec_requires).is_not_nil())

src/cpp/cpp_destructor.cpp

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -20,9 +20,6 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
2020
const source_locationt &source_location,
2121
const exprt &object)
2222
{
23-
codet new_code;
24-
new_code.add_source_location()=source_location;
25-
2623
elaborate_class_template(object.type());
2724

2825
typet tmp_type(follow(object.type()));
@@ -53,9 +50,8 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
5350
throw 0;
5451
}
5552

56-
new_code.type().id(ID_code);
53+
code_blockt new_code;
5754
new_code.add_source_location()=source_location;
58-
new_code.set_statement(ID_block);
5955

6056
// for each element of the array, call the destructor
6157
for(mp_integer i=0; i < s; ++i)
@@ -70,6 +66,8 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
7066
if(i_code.has_value())
7167
new_code.add_to_operands(std::move(i_code.value()));
7268
}
69+
70+
return std::move(new_code);
7371
}
7472
else
7573
{
@@ -115,9 +113,9 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
115113
typecheck_side_effect_function_call(function_call);
116114
already_typechecked(function_call);
117115

118-
new_code = code_expressiont(function_call);
116+
code_expressiont new_code(function_call);
119117
new_code.add_source_location() = source_location;
120-
}
121118

122-
return new_code;
119+
return std::move(new_code);
120+
}
123121
}

src/cpp/cpp_typecheck.h

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -124,9 +124,7 @@ class cpp_typecheckt:public c_typecheck_baset
124124

125125
void convert_pmop(exprt &expr);
126126

127-
void convert_anonymous_union(
128-
cpp_declarationt &declaration,
129-
codet &new_code);
127+
codet convert_anonymous_union(cpp_declarationt &declaration);
130128

131129
void convert_anon_struct_union_member(
132130
const cpp_declarationt &declaration,

src/cpp/cpp_typecheck_code.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -384,7 +384,7 @@ void cpp_typecheckt::typecheck_decl(codet &code)
384384
throw 0;
385385
}
386386

387-
convert_anonymous_union(declaration, code);
387+
code = convert_anonymous_union(declaration);
388388
return;
389389
}
390390

src/cpp/cpp_typecheck_declaration.cpp

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -31,9 +31,7 @@ void cpp_typecheckt::convert(cpp_declarationt &declaration)
3131
convert_non_template_declaration(declaration);
3232
}
3333

34-
void cpp_typecheckt::convert_anonymous_union(
35-
cpp_declarationt &declaration,
36-
codet &code)
34+
codet cpp_typecheckt::convert_anonymous_union(cpp_declarationt &declaration)
3735
{
3836
codet new_code(ID_decl_block);
3937
new_code.reserve_operands(declaration.declarators().size());
@@ -93,7 +91,7 @@ void cpp_typecheckt::convert_anonymous_union(
9391
symbol_table.get_writeable_ref(union_symbol.name)
9492
.type.set(ID_C_unnamed_object, symbol.base_name);
9593

96-
code.swap(new_code);
94+
return new_code;
9795
}
9896

9997
void cpp_typecheckt::convert_non_template_declaration(
@@ -135,8 +133,7 @@ void cpp_typecheckt::convert_non_template_declaration(
135133
throw 0;
136134
}
137135

138-
codet dummy;
139-
convert_anonymous_union(declaration, dummy);
136+
convert_anonymous_union(declaration);
140137
}
141138

142139
// do the declarators (optional)

src/goto-instrument/goto_program2code.cpp

Lines changed: 8 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -620,14 +620,13 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
620620
if(w.body().has_operands() &&
621621
to_code(w.body().operands().back()).get_statement()==ID_assign)
622622
{
623-
code_fort f(nil_exprt(), w.cond(), w.body().operands().back(), codet());
624-
623+
exprt increment = w.body().operands().back();
625624
w.body().operands().pop_back();
626-
f.iter().id(ID_side_effect);
625+
increment.id(ID_side_effect);
627626

628-
copy_source_location(target, f);
627+
code_fort f(nil_exprt(), w.cond(), increment, w.body());
629628

630-
f.body().swap(w.body());
629+
copy_source_location(target, f);
631630

632631
f.swap(w);
633632
}
@@ -1523,8 +1522,7 @@ void goto_program2codet::cleanup_code(
15231522

15241523
if(labels_in_use.find(label)==labels_in_use.end())
15251524
{
1526-
codet tmp;
1527-
tmp.swap(cl.code());
1525+
codet tmp = cl.code();
15281526
code.swap(tmp);
15291527
}
15301528
}
@@ -1624,8 +1622,7 @@ void goto_program2codet::cleanup_code_block(
16241622
parent_stmt!=ID_nil &&
16251623
to_code(code.op0()).get_statement()!=ID_decl)
16261624
{
1627-
codet tmp;
1628-
tmp.swap(code.op0());
1625+
codet tmp = to_code(code.op0());
16291626
code.swap(tmp);
16301627
}
16311628
}
@@ -1717,8 +1714,7 @@ void goto_program2codet::cleanup_code_ifthenelse(
17171714
cond.is_true() &&
17181715
(i_t_e.else_case().is_nil() || !has_labels(i_t_e.else_case())))
17191716
{
1720-
codet tmp;
1721-
tmp.swap(i_t_e.then_case());
1717+
codet tmp = i_t_e.then_case();
17221718
code.swap(tmp);
17231719
}
17241720
else if(cond.is_false() && !has_labels(i_t_e.then_case()))
@@ -1727,8 +1723,7 @@ void goto_program2codet::cleanup_code_ifthenelse(
17271723
code=code_skipt();
17281724
else
17291725
{
1730-
codet tmp;
1731-
tmp.swap(i_t_e.else_case());
1726+
codet tmp = i_t_e.else_case();
17321727
code.swap(tmp);
17331728
}
17341729
}

src/goto-programs/goto_convert.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -563,7 +563,10 @@ void goto_convertt::convert_block(
563563
unwind_destructor_stack(end_location, old_stack_size, dest, mode);
564564

565565
// remove those destructors
566-
targets.destructor_stack.resize(old_stack_size);
566+
PRECONDITION(old_stack_size <= targets.destructor_stack.size());
567+
targets.destructor_stack.erase(
568+
targets.destructor_stack.begin() + old_stack_size,
569+
targets.destructor_stack.end());
567570
}
568571

569572
void goto_convertt::convert_expression(

src/goto-programs/goto_convert_side_effect.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -453,8 +453,6 @@ void goto_convertt::remove_malloc(
453453
const irep_idt &mode,
454454
bool result_is_used)
455455
{
456-
codet call;
457-
458456
if(result_is_used)
459457
{
460458
const symbolt &new_symbol = get_fresh_aux_symbol(
@@ -469,17 +467,17 @@ void goto_convertt::remove_malloc(
469467
decl.add_source_location()=new_symbol.location;
470468
convert_decl(decl, dest, mode);
471469

472-
call=code_assignt(new_symbol.symbol_expr(), expr);
470+
code_assignt call(new_symbol.symbol_expr(), expr);
473471
call.add_source_location()=expr.source_location();
474472

475473
static_cast<exprt &>(expr)=new_symbol.symbol_expr();
474+
475+
convert(call, dest, mode);
476476
}
477477
else
478478
{
479-
call = code_expressiont(std::move(expr));
479+
convert(code_expressiont(std::move(expr)), dest, mode);
480480
}
481-
482-
convert(call, dest, mode);
483481
}
484482

485483
void goto_convertt::remove_temporary_object(

src/goto-programs/goto_program.h

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -422,13 +422,14 @@ class goto_programt
422422
{
423423
}
424424

425-
explicit instructiont(goto_program_instruction_typet _type):
426-
source_location(static_cast<const source_locationt &>(get_nil_irep())),
427-
type(_type),
428-
guard(true_exprt()),
429-
location_number(0),
430-
loop_number(0),
431-
target_number(nil_target)
425+
explicit instructiont(goto_program_instruction_typet _type)
426+
: code(static_cast<const codet &>(get_nil_irep())),
427+
source_location(static_cast<const source_locationt &>(get_nil_irep())),
428+
type(_type),
429+
guard(true_exprt()),
430+
location_number(0),
431+
loop_number(0),
432+
target_number(nil_target)
432433
{
433434
}
434435

0 commit comments

Comments
 (0)