Skip to content

Commit 0ee10a4

Browse files
committed
Use constructors to construct objects
This is some drive-by cleanup resulting from reviewing diffblue#3067. Instead of incrementally constructing objects do RAII.
1 parent aca054f commit 0ee10a4

23 files changed

+94
-133
lines changed

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

Lines changed: 16 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -122,11 +122,8 @@ static codet get_monitor_call(
122122
return code_skipt();
123123

124124
// Otherwise we create a function call
125-
code_function_callt call;
126-
call.function() = symbol_exprt(symbol, it->second.type);
127-
call.lhs().make_nil();
128-
call.arguments().push_back(object);
129-
return call;
125+
return code_function_callt(
126+
nil_exprt(), symbol_exprt(symbol, it->second.type), {object});
130127
}
131128

132129
/// Introduces a monitorexit before every return recursively.
@@ -288,11 +285,15 @@ static void instrument_start_thread(
288285

289286
// Create global variable __CPROVER__next_thread_id. Used as a counter
290287
// in-order to to assign ids to new threads.
291-
const symbolt &next_symbol =
292-
add_or_get_symbol(
293-
symbol_table, next_thread_id, next_thread_id,
294-
java_int_type(),
295-
from_integer(0, java_int_type()), false, true);
288+
const symbol_exprt next_symbol_expr = add_or_get_symbol(
289+
symbol_table,
290+
next_thread_id,
291+
next_thread_id,
292+
java_int_type(),
293+
from_integer(0, java_int_type()),
294+
false,
295+
true)
296+
.symbol_expr();
296297

297298
// Create thread-local variable __CPROVER__thread_id. Holds the id of
298299
// the thread.
@@ -320,14 +321,11 @@ static void instrument_start_thread(
320321
codet tmp_a(ID_start_thread);
321322
tmp_a.set(ID_destination, lbl1);
322323
code_gotot tmp_b(lbl2);
323-
code_labelt tmp_c(lbl1);
324-
tmp_c.op0() = codet(ID_skip);
324+
const code_labelt tmp_c(lbl1, code_skipt());
325325

326-
exprt plus(ID_plus, java_int_type());
327-
plus.copy_to_operands(next_symbol.symbol_expr());
328-
plus.copy_to_operands(from_integer(1, java_int_type()));
329-
code_assignt tmp_d(next_symbol.symbol_expr(), plus);
330-
code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol.symbol_expr());
326+
const plus_exprt plus(next_symbol_expr, from_integer(1, java_int_type()));
327+
const code_assignt tmp_d(next_symbol_expr, plus);
328+
const code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol_expr);
331329

332330
code_blockt block;
333331
block.add(tmp_a);
@@ -368,8 +366,7 @@ static void instrument_end_thread(
368366
// A: codet(id=ID_end_thread)
369367
// B: codet(id=ID_label,label= __CPROVER_THREAD_EXIT_<ID>)
370368
codet tmp_a(ID_end_thread);
371-
code_labelt tmp_b(lbl2);
372-
tmp_b.op0() = codet(ID_skip);
369+
const code_labelt tmp_b(lbl2, code_skipt());
373370

374371
code_blockt block;
375372
block.add(tmp_a);

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 8 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -973,8 +973,7 @@ codet java_bytecode_convert_methodt::get_clinit_call(
973973
return code_skipt();
974974
else
975975
{
976-
code_function_callt ret;
977-
ret.function() = findit->second.symbol_expr();
976+
const code_function_callt ret(findit->second.symbol_expr());
978977
if(needed_lazy_methods)
979978
needed_lazy_methods->add_needed_method(findit->second.name);
980979
return ret;
@@ -2004,10 +2003,8 @@ codet java_bytecode_convert_methodt::convert_monitorenterexit(
20042003
java_method_typet type(
20052004
{java_method_typet::parametert(java_reference_type(void_typet()))},
20062005
void_typet());
2007-
code_function_callt call;
2008-
call.function() = symbol_exprt(descriptor, type);
2009-
call.lhs().make_nil();
2010-
call.arguments().push_back(op[0]);
2006+
code_function_callt call(
2007+
nil_exprt(), symbol_exprt(descriptor, type), {op[0]});
20112008
call.add_source_location() = source_location;
20122009
if(needed_lazy_methods && symbol_table.has_symbol(descriptor))
20132010
needed_lazy_methods->add_needed_method(descriptor);
@@ -2737,13 +2734,11 @@ codet java_bytecode_convert_methodt::convert_iinc(
27372734
bytecode_write_typet::VARIABLE,
27382735
to_symbol_expr(locvar).get_identifier());
27392736

2740-
code_assignt code_assign;
2741-
code_assign.lhs() = variable(arg0, 'i', address, NO_CAST);
2742-
exprt arg1_int_type = arg1;
2743-
if(arg1.type() != java_int_type())
2744-
arg1_int_type.make_typecast(java_int_type());
2745-
code_assign.rhs() =
2746-
plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type);
2737+
const exprt arg1_int_type =
2738+
typecast_exprt::conditional_cast(arg1, java_int_type());
2739+
const code_assignt code_assign(
2740+
variable(arg0, 'i', address, NO_CAST),
2741+
plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type));
27472742
block.copy_to_operands(code_assign);
27482743
return block;
27492744
}

jbmc/src/java_bytecode/java_entry_point.cpp

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -169,8 +169,8 @@ static void java_static_lifetime_init(
169169
// Argument order is: name, isAnnotation, isArray, isInterface,
170170
// isSynthetic, isLocalClass, isMemberClass, isEnum
171171

172-
code_function_callt initializer_call;
173-
initializer_call.function() = class_literal_init_method->symbol_expr();
172+
code_function_callt initializer_call(
173+
class_literal_init_method->symbol_expr());
174174

175175
code_function_callt::argumentst &args = initializer_call.arguments();
176176

@@ -676,10 +676,8 @@ bool generate_java_start_function(
676676
return true; // give up with error
677677
}
678678

679-
code_function_callt call_init;
680-
call_init.lhs().make_nil();
679+
code_function_callt call_init(init_it->second.symbol_expr());
681680
call_init.add_source_location()=symbol.location;
682-
call_init.function()=init_it->second.symbol_expr();
683681

684682
init_code.move_to_operands(call_init);
685683
}
@@ -689,15 +687,13 @@ bool generate_java_start_function(
689687
// where return is a new variable
690688
// and arg1 ... argn are constructed below as well
691689

692-
code_function_callt call_main;
693-
694690
source_locationt loc=symbol.location;
695691
loc.set_function(symbol.name);
696692
source_locationt &dloc=loc;
697693

698694
// function to call
695+
code_function_callt call_main(symbol.symbol_expr());
699696
call_main.add_source_location()=dloc;
700-
call_main.function()=symbol.symbol_expr();
701697
call_main.function().add_source_location()=dloc;
702698

703699
// if the method return type is not void, store return value in a new variable

jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -213,7 +213,7 @@ exprt allocate_dynamic_object(
213213
ID_java,
214214
symbol_table);
215215
symbols_created.push_back(&malloc_sym);
216-
code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr);
216+
code_assignt assign(malloc_sym.symbol_expr(), malloc_expr);
217217
assign.add_source_location()=loc;
218218
output_code.copy_to_operands(assign);
219219
exprt malloc_symbol_expr=malloc_sym.symbol_expr();
@@ -1391,7 +1391,7 @@ void java_object_factoryt::gen_nondet_array_init(
13911391
symbol_table);
13921392
symbols_created.push_back(&array_init_symbol);
13931393
const auto &array_init_symexpr=array_init_symbol.symbol_expr();
1394-
codet data_assign=code_assignt(array_init_symexpr, init_array_expr);
1394+
code_assignt data_assign(array_init_symexpr, init_array_expr);
13951395
data_assign.add_source_location()=loc;
13961396
assignments.copy_to_operands(data_assign);
13971397

@@ -1738,8 +1738,7 @@ void java_object_factoryt::gen_method_call_if_present(
17381738
if(const auto func = symbol_table.lookup(method_name))
17391739
{
17401740
const java_method_typet &type = to_java_method_type(func->type);
1741-
code_function_callt fun_call;
1742-
fun_call.function() = func->symbol_expr();
1741+
code_function_callt fun_call(func->symbol_expr());
17431742
if(type.has_this())
17441743
fun_call.arguments().push_back(address_of_exprt(instance_expr));
17451744
assignments.add(fun_call);

jbmc/src/java_bytecode/java_static_initializers.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -208,18 +208,16 @@ static void clinit_wrapper_do_recursive_calls(
208208
auto findit = symbol_table.symbols.find(base_init_routine);
209209
if(findit == symbol_table.symbols.end())
210210
continue;
211-
code_function_callt call_base;
212-
call_base.function() = findit->second.symbol_expr();
213-
init_body.move_to_operands(call_base);
211+
const code_function_callt call_base(findit->second.symbol_expr());
212+
init_body.add(call_base);
214213
}
215214

216215
const irep_idt &real_clinit_name = clinit_function_name(class_name);
217216
auto find_sym_it = symbol_table.symbols.find(real_clinit_name);
218217
if(find_sym_it != symbol_table.symbols.end())
219218
{
220-
code_function_callt call_real_init;
221-
call_real_init.function() = find_sym_it->second.symbol_expr();
222-
init_body.move_to_operands(call_real_init);
219+
const code_function_callt call_real_init(find_sym_it->second.symbol_expr());
220+
init_body.add(call_real_init);
223221
}
224222

225223
// If nondet-static option is given, add a standard nondet initialization for

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1618,11 +1618,11 @@ codet java_string_library_preprocesst::make_object_get_class_code(
16181618
loc);
16191619

16201620
// > class1 = Class.forName(string1)
1621-
code_function_callt fun_call;
1622-
fun_call.function()=symbol_exprt(
1623-
"java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
1624-
fun_call.lhs()=class1;
1625-
fun_call.arguments().push_back(string1);
1621+
code_function_callt fun_call(
1622+
class1,
1623+
symbol_exprt(
1624+
"java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"),
1625+
{string1});
16261626
const java_method_typet fun_type(
16271627
{java_method_typet::parametert(string_ptr_type)}, class_type);
16281628
fun_call.function().type()=fun_type;

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -129,13 +129,13 @@ SCENARIO(
129129
callee.set(ID_C_class, "java::VirtualFunctionsTestParent");
130130
callee.set(ID_component_name, "f:()V");
131131

132-
code_function_callt call;
133-
call.function() = callee;
134-
// Specific argument doesn't matter, so just pass an appropriately typed
135-
// null pointer:
136-
call.arguments().push_back(
137-
null_pointer_exprt(
138-
to_pointer_type(to_code_type(callee.type()).parameters()[0].type())));
132+
const code_function_callt call(
133+
nil_exprt(),
134+
callee,
135+
// Specific argument doesn't matter, so just pass an appropriately typed
136+
// null pointer:
137+
{null_pointer_exprt(
138+
to_pointer_type(to_code_type(callee.type()).parameters()[0].type()))});
139139
virtual_call_inst->code = call;
140140

141141
test_program.add_instruction(END_FUNCTION);

jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ void check_function_call(
3232
for(const auto &target : targets)
3333
{
3434
REQUIRE(target->type == goto_program_instruction_typet::FUNCTION_CALL);
35-
const code_function_callt call = to_code_function_call(target->code);
35+
const code_function_callt &call = to_code_function_call(target->code);
3636
REQUIRE(call.function().id() == ID_symbol);
3737
REQUIRE(to_symbol_expr(call.function()).get_identifier() == function_name);
3838
}

src/cpp/cpp_typecheck_code.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -334,7 +334,7 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
334334
else
335335
{
336336
auto source_location = code.source_location();
337-
code = codet(ID_skip);
337+
code = code_skipt();
338338
code.add_source_location() = source_location;
339339
}
340340
}

src/cpp/parse.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8103,7 +8103,7 @@ bool Parser::rExprStatement(codet &statement)
81038103
#endif
81048104

81058105
lex.get_token(tk);
8106-
statement=codet(ID_skip);
8106+
statement = code_skipt();
81078107
set_location(statement, tk);
81088108
return true;
81098109
}

src/goto-analyzer/taint_analysis.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -281,8 +281,7 @@ bool taint_analysist::operator()(
281281
f_it->first!=goto_functionst::entry_point())
282282
{
283283
goto_programt::targett t=calls.add_instruction();
284-
code_function_callt call;
285-
call.function()=ns.lookup(f_it->first).symbol_expr();
284+
const code_function_callt call(ns.lookup(f_it->first).symbol_expr());
286285
t->make_function_call(call);
287286
calls.add_instruction()->make_goto(end.instructions.begin());
288287
goto_programt::targett g=gotos.add_instruction();

src/goto-cc/linker_script_merge.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -590,15 +590,15 @@ int linker_script_merget::ls_data2instructions(
590590
goto_programt::instructionst initialize_instructions=gp.instructions;
591591
for(const auto &d : data["regions"].array)
592592
{
593-
code_function_callt f;
594-
const code_typet void_t({}, empty_typet());
595-
f.function()=symbol_exprt(CPROVER_PREFIX "allocated_memory", void_t);
596593
unsigned start=safe_string2unsigned(d["start"].value);
597594
unsigned size=safe_string2unsigned(d["size"].value);
598595
constant_exprt first=from_integer(start, size_type());
599596
constant_exprt second=from_integer(size, size_type());
600-
code_function_callt::argumentst args={first, second};
601-
f.arguments()=args;
597+
const code_typet void_t({}, empty_typet());
598+
code_function_callt f(
599+
nil_exprt(),
600+
symbol_exprt(CPROVER_PREFIX "allocated_memory", void_t),
601+
{first, second});
602602
603603
source_locationt loc;
604604
loc.set_file(linker_script);

src/goto-instrument/call_sequences.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -277,7 +277,7 @@ static void list_calls_and_arguments(
277277
if(!i_it->is_function_call())
278278
continue;
279279

280-
const code_function_callt call=to_code_function_call(i_it->code);
280+
const code_function_callt &call = to_code_function_call(i_it->code);
281281

282282
const exprt &f=call.function();
283283

src/goto-instrument/goto_program2code.cpp

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1361,16 +1361,11 @@ goto_programt::const_targett goto_program2codet::convert_start_thread(
13611361

13621362
system_headers.insert("pthread.h");
13631363

1364-
code_function_callt f;
1365-
// we don't bother setting the type
1366-
f.lhs()=cf.lhs();
1367-
f.function() =
1368-
symbol_exprt("pthread_create", code_typet({}, empty_typet()));
13691364
const null_pointer_exprt n(pointer_type(empty_typet()));
1370-
f.arguments().push_back(n);
1371-
f.arguments().push_back(n);
1372-
f.arguments().push_back(cf.function());
1373-
f.arguments().push_back(cf.arguments().front());
1365+
code_function_callt f(
1366+
cf.lhs(),
1367+
symbol_exprt("pthread_create", code_typet({}, empty_typet())),
1368+
{n, n, cf.function(), cf.arguments().front()});
13741369

13751370
dest.move_to_operands(f);
13761371
return thread_end;

src/goto-instrument/interrupt.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -94,9 +94,8 @@ void interrupt(
9494
const source_locationt &source_location=
9595
original_instruction.source_location;
9696

97-
code_function_callt isr_call;
97+
code_function_callt isr_call(interrupt_handler);
9898
isr_call.add_source_location()=source_location;
99-
isr_call.function()=interrupt_handler;
10099

101100
goto_programt::targett t_goto=i_it;
102101
goto_programt::targett t_call=goto_program.insert_after(t_goto);
@@ -127,9 +126,8 @@ void interrupt(
127126

128127
const source_locationt &source_location=i_it->source_location;
129128

130-
code_function_callt isr_call;
129+
code_function_callt isr_call(interrupt_handler);
131130
isr_call.add_source_location()=source_location;
132-
isr_call.function()=interrupt_handler;
133131

134132
t_goto->make_goto(t_orig);
135133
t_goto->source_location=source_location;

src/goto-instrument/splice_call.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -73,9 +73,9 @@ bool splice_call(
7373
caller_fun->second.body.instructions.begin();
7474
goto_programt::targett g=
7575
caller_fun->second.body.insert_before(start);
76-
code_function_callt splice_call;
77-
splice_call.function()=ns.lookup(callee_fun->first).symbol_expr();
78-
g->make_function_call(to_code_function_call(splice_call));
76+
const code_function_callt splice_call(
77+
ns.lookup(callee_fun->first).symbol_expr());
78+
g->make_function_call(splice_call);
7979

8080
// update counters etc.
8181
goto_functions.update();

src/goto-instrument/thread_instrumentation.cpp

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -104,12 +104,11 @@ void mutex_init_instrumentation(
104104
{
105105
goto_programt::targett t=goto_program.insert_after(it);
106106

107-
code_function_callt call;
108-
109-
call.function()=f_it->second.symbol_expr();
110-
call.arguments().resize(2);
111-
call.arguments()[0]=address_of_exprt(code_assign.lhs());
112-
call.arguments()[1]=address_of_exprt(string_constantt("mutex-init"));
107+
const code_function_callt call(
108+
nil_exprt(),
109+
f_it->second.symbol_expr(),
110+
{address_of_exprt(code_assign.lhs()),
111+
address_of_exprt(string_constantt("mutex-init"))});
113112

114113
t->make_function_call(call);
115114
t->source_location=it->source_location;

src/goto-programs/goto_convert.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -845,7 +845,6 @@ void goto_convertt::convert_cpp_delete(
845845

846846
code_function_callt delete_call(
847847
nil_exprt(), delete_symbol, {typecast_exprt(tmp_op, arg_type)});
848-
delete_call.lhs().make_nil();
849848
delete_call.add_source_location()=code.source_location();
850849

851850
convert(delete_call, dest, ID_cpp);

0 commit comments

Comments
 (0)