Skip to content

Commit 87d1a07

Browse files
tautschnigPetr Bauch
authored and
Petr Bauch
committed
Use typecast_exprt::conditional_cast
This avoids repeated use of if(t1 != t2) x = typecast_exprt(x, t2) and thus shortens the code.
1 parent 225522f commit 87d1a07

File tree

3 files changed

+11
-26
lines changed

3 files changed

+11
-26
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 9 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -236,8 +236,8 @@ const exprt java_bytecode_convert_methodt::variable(
236236
else
237237
{
238238
exprt result=var.symbol_expr;
239-
if(do_cast==CAST_AS_NEEDED && t!=result.type())
240-
result=typecast_exprt(result, t);
239+
if(do_cast == CAST_AS_NEEDED)
240+
result = typecast_exprt::conditional_cast(result, t);
241241
return result;
242242
}
243243
}
@@ -1289,9 +1289,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
12891289
// Return types are promoted in java, so this might need
12901290
// conversion.
12911291
PRECONDITION(op.size() == 1 && results.empty());
1292-
exprt r=op[0];
1293-
if(r.type()!=method_return_type)
1294-
r=typecast_exprt(r, method_return_type);
1292+
const exprt r =
1293+
typecast_exprt::conditional_cast(op[0], method_return_type);
12951294
c=code_returnt(r);
12961295
}
12971296
else if(statement==patternt("?astore"))
@@ -2793,17 +2792,11 @@ code_ifthenelset java_bytecode_convert_methodt::convert_if_cmp(
27932792
{
27942793
code_ifthenelset code_branch;
27952794
const irep_idt cmp_op = get_if_cmp_operator(statement);
2796-
2797-
binary_relation_exprt condition(op[0], cmp_op, op[1]);
2798-
2799-
exprt &lhs(condition.lhs());
2800-
exprt &rhs(condition.rhs());
2801-
const typet &lhs_type(lhs.type());
2802-
if(lhs_type != rhs.type())
2803-
rhs = typecast_exprt(rhs, lhs_type);
2795+
binary_relation_exprt condition(
2796+
op[0], cmp_op, typecast_exprt::conditional_cast(op[1], op[0].type()));
2797+
condition.add_source_location() = location;
28042798

28052799
code_branch.cond() = condition;
2806-
code_branch.cond().add_source_location() = location;
28072800
const method_offsett label_number = numeric_cast_v<method_offsett>(number);
28082801
code_branch.then_case() = code_gotot(label(std::to_string(label_number)));
28092802
code_branch.then_case().add_source_location() =
@@ -2876,8 +2869,8 @@ code_blockt java_bytecode_convert_methodt::convert_store(
28762869
const irep_idt &var_name = to_symbol_expr(var).get_identifier();
28772870

28782871
exprt toassign = op[0];
2879-
if('a' == statement[0] && toassign.type() != var.type())
2880-
toassign = typecast_exprt(toassign, var.type());
2872+
if('a' == statement[0])
2873+
toassign = typecast_exprt::conditional_cast(toassign, var.type());
28812874

28822875
code_blockt block;
28832876

src/pointer-analysis/pointer_offset_sum.cpp

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -24,10 +24,6 @@ exprt pointer_offset_sum(const exprt &a, const exprt &b)
2424
else if(b.is_zero())
2525
return a;
2626

27-
plus_exprt new_offset(a, b);
28-
29-
if(b.type() != a.type())
30-
new_offset.op1().make_typecast(a.type());
31-
27+
plus_exprt new_offset(a, typecast_exprt::conditional_cast(b, a.type()));
3228
return std::move(new_offset);
3329
}

src/solvers/flattening/functions.cpp

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -42,11 +42,7 @@ exprt functionst::arguments_equal(const exprt::operandst &o1,
4242
for(std::size_t i=0; i<o1.size(); i++)
4343
{
4444
exprt lhs=o1[i];
45-
exprt rhs=o2[i];
46-
47-
if(lhs.type()!=rhs.type())
48-
rhs.make_typecast(lhs.type());
49-
45+
exprt rhs = typecast_exprt::conditional_cast(o2[i], o1[i].type());
5046
conjuncts[i]=equal_exprt(lhs, rhs);
5147
}
5248

0 commit comments

Comments
 (0)