Skip to content

Commit 1e9d135

Browse files
committed
Use code_blockt::add(code, source_location)
This simplifies the code and helps getting rid of some more temporaries.
1 parent cc7eff6 commit 1e9d135

File tree

1 file changed

+7
-11
lines changed

1 file changed

+7
-11
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+7-11
Original file line numberDiff line numberDiff line change
@@ -1949,10 +1949,9 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
19491949
if(a_it == args.begin())
19501950
{
19511951
code_switch_caset code_case(nil_exprt(), std::move(code));
1952-
code_case.add_source_location() = location;
19531952
code_case.set_default();
19541953

1955-
code_block.add(std::move(code_case));
1954+
code_block.add(std::move(code_case), location);
19561955
}
19571956
else
19581957
{
@@ -1961,9 +1960,7 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
19611960
case_op.add_source_location() = location;
19621961

19631962
code_switch_caset code_case(std::move(case_op), std::move(code));
1964-
code_case.add_source_location() = location;
1965-
1966-
code_block.add(std::move(code_case));
1963+
code_block.add(std::move(code_case), location);
19671964
}
19681965
}
19691966
}
@@ -2853,15 +2850,15 @@ code_blockt java_bytecode_convert_methodt::convert_store(
28532850
toassign = typecast_exprt::conditional_cast(toassign, var.type());
28542851

28552852
code_blockt block;
2853+
block.add_source_location() = location;
28562854

28572855
save_stack_entries(
28582856
"stack_store",
28592857
block,
28602858
bytecode_write_typet::VARIABLE,
28612859
var_name);
2862-
code_assignt assign(var, toassign);
2863-
assign.add_source_location() = location;
2864-
block.add(assign);
2860+
2861+
block.add(code_assignt{var, toassign}, location);
28652862
return block;
28662863
}
28672864

@@ -2886,9 +2883,8 @@ code_blockt java_bytecode_convert_methodt::convert_astore(
28862883
save_stack_entries(
28872884
"stack_astore", block, bytecode_write_typet::ARRAY_REF, "");
28882885

2889-
code_assignt array_put(element, op[2]);
2890-
array_put.add_source_location() = location;
2891-
block.add(array_put);
2886+
code_assignt array_put{dereference_exprt{data_plus_offset}, op[2]};
2887+
block.add(std::move(array_put), location);
28922888
return block;
28932889
}
28942890

0 commit comments

Comments
 (0)