Skip to content

Commit e010ac4

Browse files
committed
Use more specific return type instead of generic codet/exprt
If functions can only ever return a single kind of codet/exprt, there is no need to use the generic codet/exprt and std::move.
1 parent 0b81f16 commit e010ac4

10 files changed

+58
-58
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 22 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -991,7 +991,7 @@ static std::size_t get_bytecode_type_width(const typet &ty)
991991
return ty.get_size_t(ID_width);
992992
}
993993

994-
codet java_bytecode_convert_methodt::convert_instructions(
994+
code_blockt java_bytecode_convert_methodt::convert_instructions(
995995
const methodt &method,
996996
const java_class_typet::java_lambda_method_handlest &lambda_method_handles)
997997
{
@@ -1913,7 +1913,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
19131913
for(auto &block : root_block.statements())
19141914
code.add(block);
19151915

1916-
return std::move(code);
1916+
return code;
19171917
}
19181918

19191919
codet java_bytecode_convert_methodt::convert_pop(
@@ -1932,7 +1932,7 @@ codet java_bytecode_convert_methodt::convert_pop(
19321932
return c;
19331933
}
19341934

1935-
codet java_bytecode_convert_methodt::convert_switch(
1935+
code_switcht java_bytecode_convert_methodt::convert_switch(
19361936
java_bytecode_convert_methodt::address_mapt &address_map,
19371937
const exprt::operandst &op,
19381938
const java_bytecode_parse_treet::instructiont::argst &args,
@@ -1983,7 +1983,7 @@ codet java_bytecode_convert_methodt::convert_switch(
19831983
}
19841984

19851985
code_switch.body() = code_block;
1986-
return std::move(code_switch);
1986+
return code_switch;
19871987
}
19881988

19891989
codet java_bytecode_convert_methodt::convert_monitorenterexit(
@@ -2537,7 +2537,7 @@ void java_bytecode_convert_methodt::convert_new(
25372537
results[0] = tmp;
25382538
}
25392539

2540-
codet java_bytecode_convert_methodt::convert_putstatic(
2540+
code_blockt java_bytecode_convert_methodt::convert_putstatic(
25412541
const source_locationt &location,
25422542
const exprt &arg0,
25432543
const exprt::operandst &op,
@@ -2566,10 +2566,10 @@ codet java_bytecode_convert_methodt::convert_putstatic(
25662566
bytecode_write_typet::STATIC_FIELD,
25672567
symbol_expr.get_identifier());
25682568
block.add(code_assignt(symbol_expr, op[0]));
2569-
return std::move(block);
2569+
return block;
25702570
}
25712571

2572-
codet java_bytecode_convert_methodt::convert_putfield(
2572+
code_blockt java_bytecode_convert_methodt::convert_putfield(
25732573
const exprt &arg0,
25742574
const exprt::operandst &op)
25752575
{
@@ -2581,7 +2581,7 @@ codet java_bytecode_convert_methodt::convert_putfield(
25812581
bytecode_write_typet::FIELD,
25822582
arg0.get(ID_component_name));
25832583
block.add(code_assignt(to_member(op[0], arg0), op[1]));
2584-
return std::move(block);
2584+
return block;
25852585
}
25862586

25872587
void java_bytecode_convert_methodt::convert_getstatic(
@@ -2698,7 +2698,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_ushr(
26982698
return results;
26992699
}
27002700

2701-
codet java_bytecode_convert_methodt::convert_iinc(
2701+
code_blockt java_bytecode_convert_methodt::convert_iinc(
27022702
const exprt &arg0,
27032703
const exprt &arg1,
27042704
const source_locationt &location,
@@ -2722,10 +2722,10 @@ codet java_bytecode_convert_methodt::convert_iinc(
27222722
plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type));
27232723
block.add(code_assign);
27242724

2725-
return std::move(block);
2725+
return block;
27262726
}
27272727

2728-
codet java_bytecode_convert_methodt::convert_ifnull(
2728+
code_ifthenelset java_bytecode_convert_methodt::convert_ifnull(
27292729
const java_bytecode_convert_methodt::address_mapt &address_map,
27302730
const exprt::operandst &op,
27312731
const mp_integer &number,
@@ -2740,10 +2740,10 @@ codet java_bytecode_convert_methodt::convert_ifnull(
27402740
code_branch.then_case().add_source_location() =
27412741
address_map.at(label_number).source->source_location;
27422742
code_branch.add_source_location() = location;
2743-
return std::move(code_branch);
2743+
return code_branch;
27442744
}
27452745

2746-
codet java_bytecode_convert_methodt::convert_ifnonull(
2746+
code_ifthenelset java_bytecode_convert_methodt::convert_ifnonull(
27472747
const java_bytecode_convert_methodt::address_mapt &address_map,
27482748
const exprt::operandst &op,
27492749
const mp_integer &number,
@@ -2758,10 +2758,10 @@ codet java_bytecode_convert_methodt::convert_ifnonull(
27582758
code_branch.then_case().add_source_location() =
27592759
address_map.at(label_number).source->source_location;
27602760
code_branch.add_source_location() = location;
2761-
return std::move(code_branch);
2761+
return code_branch;
27622762
}
27632763

2764-
codet java_bytecode_convert_methodt::convert_if(
2764+
code_ifthenelset java_bytecode_convert_methodt::convert_if(
27652765
const java_bytecode_convert_methodt::address_mapt &address_map,
27662766
const exprt::operandst &op,
27672767
const irep_idt &id,
@@ -2780,10 +2780,10 @@ codet java_bytecode_convert_methodt::convert_if(
27802780
code_branch.then_case().add_source_location().set_function(method_id);
27812781
code_branch.add_source_location() = location;
27822782
code_branch.add_source_location().set_function(method_id);
2783-
return std::move(code_branch);
2783+
return code_branch;
27842784
}
27852785

2786-
codet java_bytecode_convert_methodt::convert_if_cmp(
2786+
code_ifthenelset java_bytecode_convert_methodt::convert_if_cmp(
27872787
const java_bytecode_convert_methodt::address_mapt &address_map,
27882788
const irep_idt &statement,
27892789
const exprt::operandst &op,
@@ -2809,7 +2809,7 @@ codet java_bytecode_convert_methodt::convert_if_cmp(
28092809
address_map.at(label_number).source->source_location;
28102810
code_branch.add_source_location() = location;
28112811

2812-
return std::move(code_branch);
2812+
return code_branch;
28132813
}
28142814

28152815
code_blockt java_bytecode_convert_methodt::convert_ret(
@@ -2864,7 +2864,7 @@ exprt java_bytecode_convert_methodt::convert_aload(
28642864
return java_bytecode_promotion(element);
28652865
}
28662866

2867-
codet java_bytecode_convert_methodt::convert_store(
2867+
code_blockt java_bytecode_convert_methodt::convert_store(
28682868
const irep_idt &statement,
28692869
const exprt &arg0,
28702870
const exprt::operandst &op,
@@ -2889,10 +2889,10 @@ codet java_bytecode_convert_methodt::convert_store(
28892889
code_assignt assign(var, toassign);
28902890
assign.add_source_location() = location;
28912891
block.add(assign);
2892-
return std::move(block);
2892+
return block;
28932893
}
28942894

2895-
codet java_bytecode_convert_methodt::convert_astore(
2895+
code_blockt java_bytecode_convert_methodt::convert_astore(
28962896
const irep_idt &statement,
28972897
const exprt::operandst &op,
28982898
const source_locationt &location)
@@ -2921,7 +2921,7 @@ codet java_bytecode_convert_methodt::convert_astore(
29212921
code_assignt array_put(element, op[2]);
29222922
array_put.add_source_location() = location;
29232923
block.add(array_put);
2924-
return std::move(block);
2924+
return block;
29252925
}
29262926

29272927
optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -268,7 +268,7 @@ class java_bytecode_convert_methodt:public messaget
268268
// conversion
269269
void convert(const symbolt &class_symbol, const methodt &);
270270

271-
codet convert_instructions(
271+
code_blockt convert_instructions(
272272
const methodt &,
273273
const java_class_typet::java_lambda_method_handlest &);
274274

@@ -321,12 +321,12 @@ class java_bytecode_convert_methodt:public messaget
321321
const source_locationt &location,
322322
const exprt &arg0);
323323

324-
codet convert_astore(
324+
code_blockt convert_astore(
325325
const irep_idt &statement,
326326
const exprt::operandst &op,
327327
const source_locationt &location);
328328

329-
codet convert_store(
329+
code_blockt convert_store(
330330
const irep_idt &statement,
331331
const exprt &arg0,
332332
const exprt::operandst &op,
@@ -342,33 +342,33 @@ class java_bytecode_convert_methodt:public messaget
342342
const source_locationt &location,
343343
const method_offsett address);
344344

345-
codet convert_if_cmp(
345+
code_ifthenelset convert_if_cmp(
346346
const java_bytecode_convert_methodt::address_mapt &address_map,
347347
const irep_idt &statement,
348348
const exprt::operandst &op,
349349
const mp_integer &number,
350350
const source_locationt &location) const;
351351

352-
codet convert_if(
352+
code_ifthenelset convert_if(
353353
const java_bytecode_convert_methodt::address_mapt &address_map,
354354
const exprt::operandst &op,
355355
const irep_idt &id,
356356
const mp_integer &number,
357357
const source_locationt &location) const;
358358

359-
codet convert_ifnonull(
359+
code_ifthenelset convert_ifnonull(
360360
const java_bytecode_convert_methodt::address_mapt &address_map,
361361
const exprt::operandst &op,
362362
const mp_integer &number,
363363
const source_locationt &location) const;
364364

365-
codet convert_ifnull(
365+
code_ifthenelset convert_ifnull(
366366
const java_bytecode_convert_methodt::address_mapt &address_map,
367367
const exprt::operandst &op,
368368
const mp_integer &number,
369369
const source_locationt &location) const;
370370

371-
codet convert_iinc(
371+
code_blockt convert_iinc(
372372
const exprt &arg0,
373373
const exprt &arg1,
374374
const source_locationt &location,
@@ -394,9 +394,9 @@ class java_bytecode_convert_methodt:public messaget
394394
codet &c,
395395
exprt::operandst &results);
396396

397-
codet convert_putfield(const exprt &arg0, const exprt::operandst &op);
397+
code_blockt convert_putfield(const exprt &arg0, const exprt::operandst &op);
398398

399-
codet convert_putstatic(
399+
code_blockt convert_putstatic(
400400
const source_locationt &location,
401401
const exprt &arg0,
402402
const exprt::operandst &op,
@@ -466,7 +466,7 @@ class java_bytecode_convert_methodt:public messaget
466466

467467
void convert_dup2(exprt::operandst &op, exprt::operandst &results);
468468

469-
codet convert_switch(
469+
code_switcht convert_switch(
470470
java_bytecode_convert_methodt::address_mapt &address_map,
471471
const exprt::operandst &op,
472472
const java_bytecode_parse_treet::instructiont::argst &args,

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ class java_bytecode_instrumentt:public messaget
4343
const bool throw_runtime_exceptions;
4444
message_handlert &message_handler;
4545

46-
codet throw_exception(
46+
code_ifthenelset throw_exception(
4747
const exprt &cond,
4848
const source_locationt &original_loc,
4949
const irep_idt &exc_name);
@@ -61,7 +61,7 @@ class java_bytecode_instrumentt:public messaget
6161
const exprt &expr,
6262
const source_locationt &original_loc);
6363

64-
codet check_class_cast(
64+
code_ifthenelset check_class_cast(
6565
const exprt &class1,
6666
const exprt &class2,
6767
const source_locationt &original_loc);
@@ -92,7 +92,7 @@ const std::vector<std::string> exception_needed_classes = {
9292
/// \param exc_name: the name of the exception to be thrown
9393
/// \return Returns the code initialising the throwing the
9494
/// exception
95-
codet java_bytecode_instrumentt::throw_exception(
95+
code_ifthenelset java_bytecode_instrumentt::throw_exception(
9696
const exprt &cond,
9797
const source_locationt &original_loc,
9898
const irep_idt &exc_name)
@@ -133,7 +133,7 @@ codet java_bytecode_instrumentt::throw_exception(
133133
if_code.cond()=cond;
134134
if_code.then_case() = code_blockt({assign_new, code_expressiont(throw_expr)});
135135

136-
return std::move(if_code);
136+
return if_code;
137137
}
138138

139139

@@ -218,7 +218,7 @@ codet java_bytecode_instrumentt::check_array_access(
218218
/// \return Based on the value of the flag `throw_runtime_exceptions`,
219219
/// it returns code that either throws an ClassCastException or emits an
220220
/// assertion checking the subtype relation
221-
codet java_bytecode_instrumentt::check_class_cast(
221+
code_ifthenelset java_bytecode_instrumentt::check_class_cast(
222222
const exprt &class1,
223223
const exprt &class2,
224224
const source_locationt &original_loc)
@@ -255,7 +255,7 @@ codet java_bytecode_instrumentt::check_class_cast(
255255
notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr));
256256
conditional_check.cond()=std::move(op_not_null);
257257
conditional_check.then_case()=std::move(check_code);
258-
return std::move(conditional_check);
258+
return conditional_check;
259259
}
260260

261261
/// Checks whether `expr` is null and throws NullPointerException/

jbmc/src/java_bytecode/java_static_initializers.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -445,7 +445,7 @@ static void create_clinit_wrapper_symbols(
445445
/// \param pointer_type_selector: used to choose concrete types for abstract-
446446
/// typed globals and fields (only needed if nondet-static is true)
447447
/// \return the body of the static initializer wrapper
448-
codet get_thread_safe_clinit_wrapper_body(
448+
code_blockt get_thread_safe_clinit_wrapper_body(
449449
const irep_idt &function_id,
450450
symbol_table_baset &symbol_table,
451451
const bool nondet_static,
@@ -626,7 +626,7 @@ codet get_thread_safe_clinit_wrapper_body(
626626
function_body.add(code_returnt());
627627
}
628628

629-
return std::move(function_body);
629+
return function_body;
630630
}
631631

632632
/// Produces the static initializer wrapper body for the given function.
@@ -641,7 +641,7 @@ codet get_thread_safe_clinit_wrapper_body(
641641
/// \param pointer_type_selector: used to choose concrete types for abstract-
642642
/// typed globals and fields (only needed if nondet-static is true)
643643
/// \return the body of the static initializer wrapper
644-
codet get_clinit_wrapper_body(
644+
code_ifthenelset get_clinit_wrapper_body(
645645
const irep_idt &function_id,
646646
symbol_table_baset &symbol_table,
647647
const bool nondet_static,
@@ -701,7 +701,7 @@ codet get_clinit_wrapper_body(
701701

702702
wrapper_body.then_case() = init_body;
703703

704-
return std::move(wrapper_body);
704+
return wrapper_body;
705705
}
706706

707707

@@ -841,7 +841,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
841841
/// \param pointer_type_selector: used to choose concrete types for abstract-
842842
/// typed globals and fields.
843843
/// \return synthetic static initializer body.
844-
codet stub_global_initializer_factoryt::get_stub_initializer_body(
844+
code_blockt stub_global_initializer_factoryt::get_stub_initializer_body(
845845
const irep_idt &function_id,
846846
symbol_table_baset &symbol_table,
847847
const object_factory_parameterst &object_factory_parameters,
@@ -890,5 +890,5 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body(
890890
update_in_placet::NO_UPDATE_IN_PLACE);
891891
}
892892

893-
return std::move(static_init_body);
893+
return static_init_body;
894894
}

jbmc/src/java_bytecode/java_static_initializers.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,14 +27,14 @@ void create_static_initializer_wrappers(
2727
synthetic_methods_mapt &synthetic_methods,
2828
const bool thread_safe);
2929

30-
codet get_thread_safe_clinit_wrapper_body(
30+
code_blockt get_thread_safe_clinit_wrapper_body(
3131
const irep_idt &function_id,
3232
symbol_table_baset &symbol_table,
3333
const bool nondet_static,
3434
const object_factory_parameterst &object_factory_parameters,
3535
const select_pointer_typet &pointer_type_selector);
3636

37-
codet get_clinit_wrapper_body(
37+
code_ifthenelset get_clinit_wrapper_body(
3838
const irep_idt &function_id,
3939
symbol_table_baset &symbol_table,
4040
const bool nondet_static,
@@ -53,7 +53,7 @@ class stub_global_initializer_factoryt
5353
const std::unordered_set<irep_idt> &stub_globals_set,
5454
synthetic_methods_mapt &synthetic_methods);
5555

56-
codet get_stub_initializer_body(
56+
code_blockt get_stub_initializer_body(
5757
const irep_idt &function_id,
5858
symbol_table_baset &symbol_table,
5959
const object_factory_parameterst &object_factory_parameters,

0 commit comments

Comments
 (0)