Skip to content

Commit 65cfed1

Browse files
tautschnigtautschnig
authored
Merge pull request #3856 from diffblue/make_typecast
deprecate exprt::make_typecast(type)
2 parents e2a5430 + 49b0670 commit 65cfed1

22 files changed

+79
-118
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 9 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1386,9 +1386,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
13861386
DATA_INVARIANT(
13871387
arg0.id()==ID_constant,
13881388
"ipush argument expected to be constant");
1389-
results[0]=arg0;
1390-
if(arg0.type()!=java_int_type())
1391-
results[0].make_typecast(java_int_type());
1389+
results[0] = typecast_exprt::conditional_cast(arg0, java_int_type());
13921390
}
13931391
else if(statement==patternt("if_?cmp??"))
13941392
{
@@ -1598,9 +1596,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
15981596
{
15991597
PRECONDITION(op.size() == 1 && results.size() == 1);
16001598
typet type=java_type_from_char(statement[2]);
1601-
results[0]=op[0];
1602-
if(results[0].type()!=type)
1603-
results[0].make_typecast(type);
1599+
results[0] = typecast_exprt::conditional_cast(op[0], type);
16041600
}
16051601
else if(statement=="new")
16061602
{
@@ -2277,9 +2273,9 @@ codet &java_bytecode_convert_methodt::replace_call_to_cprover_assume(
22772273
codet &c)
22782274
{
22792275
exprt operand = pop(1)[0];
2276+
22802277
// we may need to adjust the type of the argument
2281-
if(operand.type() != bool_typet())
2282-
operand.make_typecast(bool_typet());
2278+
operand = typecast_exprt::conditional_cast(operand, bool_typet());
22832279

22842280
c = code_assumet(operand);
22852281
location.set_function(method_id);
@@ -2701,16 +2697,12 @@ exprt::operandst &java_bytecode_convert_methodt::convert_ushr(
27012697
const std::size_t width = get_bytecode_type_width(type);
27022698
typet target = unsignedbv_typet(width);
27032699

2704-
exprt lhs = op[0];
2705-
if(lhs.type() != target)
2706-
lhs.make_typecast(target);
2707-
exprt rhs = op[1];
2708-
if(rhs.type() != target)
2709-
rhs.make_typecast(target);
2700+
exprt lhs = typecast_exprt::conditional_cast(op[0], target);
2701+
exprt rhs = typecast_exprt::conditional_cast(op[1], target);
2702+
2703+
results[0] =
2704+
typecast_exprt::conditional_cast(lshr_exprt(lhs, rhs), op[0].type());
27102705

2711-
results[0] = lshr_exprt(lhs, rhs);
2712-
if(results[0].type() != op[0].type())
2713-
results[0].make_typecast(op[0].type());
27142706
return results;
27152707
}
27162708

‎jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,8 @@ void java_bytecode_typecheckt::typecheck_code(codet &code)
2121
typecheck_expr(code_assign.lhs());
2222
typecheck_expr(code_assign.rhs());
2323

24-
if(code_assign.lhs().type()!=code_assign.rhs().type())
25-
code_assign.rhs().make_typecast(code_assign.lhs().type());
24+
code_assign.rhs() = typecast_exprt::conditional_cast(
25+
code_assign.rhs(), code_assign.lhs().type());
2626
}
2727
else if(statement==ID_block)
2828
{

‎src/analyses/escape_analysis.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -421,8 +421,9 @@ void escape_analysist::insert_cleanup(
421421
exprt arg=lhs;
422422
if(is_object)
423423
arg=address_of_exprt(arg);
424-
if(arg.type()!=param_type)
425-
arg.make_typecast(param_type);
424+
425+
arg = typecast_exprt::conditional_cast(arg, param_type);
426+
426427
code.arguments().push_back(arg);
427428
}
428429

‎src/analyses/goto_check.cpp

Lines changed: 10 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1293,18 +1293,19 @@ void goto_checkt::bounds_check(
12931293
const exprt &pointer=
12941294
to_dereference_expr(ode.root_object()).pointer();
12951295

1296-
if_exprt size(
1296+
const if_exprt size(
12971297
dynamic_object(pointer),
12981298
typecast_exprt(dynamic_size(ns), object_size(pointer).type()),
12991299
object_size(pointer));
13001300

1301-
plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
1301+
const plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
13021302

13031303
assert(effective_offset.op0().type()==effective_offset.op1().type());
1304-
if(effective_offset.type()!=size.type())
1305-
size.make_typecast(effective_offset.type());
13061304

1307-
binary_relation_exprt inequality(effective_offset, ID_lt, size);
1305+
const auto size_casted =
1306+
typecast_exprt::conditional_cast(size, effective_offset.type());
1307+
1308+
binary_relation_exprt inequality(effective_offset, ID_lt, size_casted);
13081309

13091310
or_exprt precond(
13101311
and_exprt(
@@ -1371,12 +1372,8 @@ void goto_checkt::bounds_check(
13711372
binary_relation_exprt inequality(index, ID_lt, size);
13721373

13731374
// typecast size
1374-
if(inequality.op1().type()!=inequality.op0().type())
1375-
inequality.op1().make_typecast(inequality.op0().type());
1376-
1377-
// typecast size
1378-
if(inequality.op1().type()!=inequality.op0().type())
1379-
inequality.op1().make_typecast(inequality.op0().type());
1375+
inequality.op1() = typecast_exprt::conditional_cast(
1376+
inequality.op1(), inequality.op0().type());
13801377

13811378
add_guarded_claim(
13821379
implies_exprt(type_matches_size, inequality),
@@ -1839,8 +1836,8 @@ void goto_checkt::goto_check(
18391836
goto_programt::targett t=new_code.add_instruction(ASSIGN);
18401837
exprt address_of_expr=address_of_exprt(variable);
18411838
exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
1842-
if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
1843-
address_of_expr.make_typecast(lhs.type());
1839+
address_of_expr =
1840+
typecast_exprt::conditional_cast(address_of_expr, lhs.type());
18441841
const if_exprt rhs(
18451842
side_effect_expr_nondett(bool_typet(), i.source_location),
18461843
address_of_expr,

‎src/ansi-c/c_typecast.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -735,16 +735,15 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
735735

736736
if(dest_type.get(ID_C_c_type)==ID_bool)
737737
{
738-
expr=is_not_zero(expr, ns);
739-
expr.make_typecast(dest_type);
738+
expr = typecast_exprt(is_not_zero(expr, ns), dest_type);
740739
}
741740
else if(dest_type.id()==ID_bool)
742741
{
743742
expr=is_not_zero(expr, ns);
744743
}
745744
else
746745
{
747-
expr.make_typecast(dest_type);
746+
expr = typecast_exprt(expr, dest_type);
748747
}
749748
}
750749
}

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -667,7 +667,7 @@ void c_typecheck_baset::typecheck_return(codet &code)
667667
warning() << to_string(code.op0().type());
668668
warning() << eom;
669669

670-
code.op0().make_typecast(return_type);
670+
code.op0() = typecast_exprt(code.op0(), return_type);
671671
}
672672
}
673673
else

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 15 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -420,7 +420,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
420420
// that we are using "bool" for boolean operators instead
421421
// of "int". We convert for this reason.
422422
if(expr.op0().type().id() == ID_bool)
423-
expr.op0().make_typecast(signed_int_type());
423+
expr.op0() = typecast_exprt(expr.op0(), signed_int_type());
424424

425425
irept::subt &generic_associations=
426426
expr.add(ID_generic_associations).get_sub();
@@ -619,8 +619,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
619619
throw 0;
620620
}
621621

622-
if(o.type()!=size_type())
623-
o.make_typecast(size_type());
622+
o = typecast_exprt::conditional_cast(o, size_type());
624623

625624
result=plus_exprt(result, o);
626625
}
@@ -653,8 +652,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
653652
throw 0;
654653
}
655654

656-
if(o.type()!=size_type())
657-
o.make_typecast(size_type());
655+
o = typecast_exprt::conditional_cast(o, size_type());
658656

659657
result=plus_exprt(result, o);
660658
}
@@ -696,8 +694,9 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
696694
typecheck_expr(index);
697695

698696
exprt sub_size=size_of_expr(type.subtype(), *this);
699-
if(index.type()!=size_type())
700-
index.make_typecast(size_type());
697+
698+
index = typecast_exprt::conditional_cast(index, size_type());
699+
701700
result=plus_exprt(result, mult_exprt(sub_size, index));
702701

703702
typet tmp=type.subtype();
@@ -1104,7 +1103,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
11041103
// that we are using "bool" for boolean operators instead
11051104
// of "int". We convert for this reason.
11061105
if(op.type().id() == ID_bool)
1107-
op.make_typecast(signed_int_type());
1106+
op = typecast_exprt(op, signed_int_type());
11081107

11091108
// we need to find a member with the right type
11101109
for(const auto &c : to_union_type(expr_type).components())
@@ -1409,19 +1408,19 @@ void c_typecheck_baset::typecheck_expr_rel(
14091408
// pointer and integer
14101409
if(type0.id()==ID_pointer && is_number(type1))
14111410
{
1412-
op1.make_typecast(type0);
1411+
op1 = typecast_exprt(op1, type0);
14131412
return;
14141413
}
14151414

14161415
if(type1.id()==ID_pointer && is_number(type0))
14171416
{
1418-
op0.make_typecast(type1);
1417+
op0 = typecast_exprt(op0, type1);
14191418
return;
14201419
}
14211420

14221421
if(type0.id()==ID_pointer && type1.id()==ID_pointer)
14231422
{
1424-
op1.make_typecast(type0);
1423+
op1 = typecast_exprt(op1, type0);
14251424
return;
14261425
}
14271426
}
@@ -1890,7 +1889,7 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
18901889
{
18911890
// promote to underlying type
18921891
typet underlying_type = to_c_bit_field_type(type0).subtype();
1893-
expr.op0().make_typecast(underlying_type);
1892+
expr.op0() = typecast_exprt(expr.op0(), underlying_type);
18941893
expr.type()=underlying_type;
18951894
}
18961895
else if(is_numeric_type(type0))
@@ -2973,8 +2972,7 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
29732972
is_number(o_type0.subtype()))
29742973
{
29752974
// Vector arithmetic has fairly strict typing rules, no promotion
2976-
if(o_type0!=o_type1)
2977-
op1.make_typecast(op0.type());
2975+
op1 = typecast_exprt::conditional_cast(op1, op0.type());
29782976
expr.type()=op0.type();
29792977
return;
29802978
}
@@ -3326,7 +3324,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
33263324
// Add a cast to the underlying type for bit fields.
33273325
// In particular, sizeof(s.f=1) works for bit fields.
33283326
if(op0.type().id()==ID_c_bit_field)
3329-
op0.make_typecast(op0.type().subtype());
3327+
op0 = typecast_exprt(op0, op0.type().subtype());
33303328

33313329
const typet o_type0=op0.type();
33323330
const typet o_type1=op1.type();
@@ -3406,8 +3404,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
34063404
if(gcc_vector_types_compatible(
34073405
to_vector_type(o_type0), to_vector_type(o_type1)))
34083406
{
3409-
if(o_type0!=o_type1)
3410-
op1.make_typecast(o_type0);
3407+
op1 = typecast_exprt::conditional_cast(op1, o_type0);
34113408
return;
34123409
}
34133410
}
@@ -3427,8 +3424,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
34273424
if(gcc_vector_types_compatible(
34283425
to_vector_type(o_type0), to_vector_type(o_type1)))
34293426
{
3430-
if(o_type0!=o_type1)
3431-
op1.make_typecast(o_type0);
3427+
op1 = typecast_exprt::conditional_cast(op1, o_type0);
34323428
return;
34333429
}
34343430
}

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1020,7 +1020,7 @@ void c_typecheck_baset::typecheck_compound_body(
10201020
exprt &assertion=it->op0();
10211021
typecheck_expr(assertion);
10221022
typecheck_expr(it->op1());
1023-
assertion.make_typecast(bool_typet());
1023+
assertion = typecast_exprt(assertion, bool_typet());
10241024
make_constant(assertion);
10251025

10261026
if(assertion.is_false())

‎src/cpp/cpp_typecheck_compound_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1703,5 +1703,5 @@ void cpp_typecheckt::make_ptr_typecast(
17031703
subtype_typecast(src_struct, dest_struct) ||
17041704
subtype_typecast(dest_struct, src_struct));
17051705

1706-
expr.make_typecast(dest_type);
1706+
expr = typecast_exprt(expr, dest_type);
17071707
}

‎src/cpp/cpp_typecheck_resolve.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1725,9 +1725,7 @@ void cpp_typecheck_resolvet::guess_template_args(
17251725
if(e.id()==ID_unassigned)
17261726
{
17271727
typet old_type=e.type();
1728-
e=desired_expr;
1729-
if(e.type()!=old_type)
1730-
e.make_typecast(old_type);
1728+
e = typecast_exprt::conditional_cast(desired_expr, old_type);
17311729
}
17321730
}
17331731
}

‎src/linking/linking.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1072,7 +1072,7 @@ void linkingt::duplicate_object_symbol(
10721072
{
10731073
// the type has been updated, now make sure that the initialising assignment
10741074
// will have matching types
1075-
old_symbol.value.make_typecast(old_symbol.type);
1075+
old_symbol.value = typecast_exprt(old_symbol.value, old_symbol.type);
10761076
}
10771077
}
10781078

‎src/pointer-analysis/goto_program_dereference.cpp

Lines changed: 2 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -180,17 +180,8 @@ void goto_program_dereferencet::dereference_rec(
180180
assert(expr.operands().size()==1);
181181

182182
if(expr.op0().id()==ID_dereference)
183-
{
184-
assert(expr.op0().operands().size()==1);
185-
186-
exprt tmp;
187-
tmp.swap(expr.op0().op0());
188-
189-
if(tmp.type()!=expr.type())
190-
tmp.make_typecast(expr.type());
191-
192-
expr.swap(tmp);
193-
}
183+
expr = typecast_exprt::conditional_cast(
184+
to_dereference_expr(expr.op0()).pointer(), expr.type());
194185
}
195186

196187
Forall_operands(it, expr)

‎src/solvers/flattening/arrays.cpp

Lines changed: 3 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -323,14 +323,8 @@ void arrayst::add_array_Ackermann_constraints()
323323
continue;
324324

325325
// index equality
326-
equal_exprt indices_equal(*i1, *i2);
327-
328-
if(indices_equal.op0().type()!=
329-
indices_equal.op1().type())
330-
{
331-
indices_equal.op1().
332-
make_typecast(indices_equal.op0().type());
333-
}
326+
const equal_exprt indices_equal(
327+
*i1, typecast_exprt::conditional_cast(*i2, i1->type()));
334328

335329
literalt indices_equal_lit=convert(indices_equal);
336330

@@ -537,8 +531,7 @@ void arrayst::add_array_constraints_with(
537531
{
538532
// we first build the guard
539533

540-
if(other_index.type()!=index.type())
541-
other_index.make_typecast(index.type());
534+
other_index = typecast_exprt::conditional_cast(other_index, index.type());
542535

543536
literalt guard_lit=convert(equal_exprt(index, other_index));
544537

‎src/solvers/flattening/boolbv_byte_extract.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -91,8 +91,10 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
9191
object_descriptor_exprt o;
9292
o.build(expr.op(), ns);
9393
CHECK_RETURN(o.offset().id() != ID_unknown);
94-
if(o.offset().type() != expr.offset().type())
95-
o.offset().make_typecast(expr.offset().type());
94+
95+
o.offset() =
96+
typecast_exprt::conditional_cast(o.offset(), expr.offset().type());
97+
9698
byte_extract_exprt be(
9799
expr.id(),
98100
o.root_object(),

‎src/solvers/lowering/byte_operators.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -396,9 +396,7 @@ static exprt lower_byte_update(
396396

397397
if(i==0 && element_size==1) // bytes?
398398
{
399-
new_value = src.value();
400-
if(new_value.type()!=subtype)
401-
new_value.make_typecast(subtype);
399+
new_value = typecast_exprt::conditional_cast(src.value(), subtype);
402400
}
403401
else
404402
{

0 commit comments

Comments
 (0)