Skip to content

Commit 7a0493a

Browse files
kroeningkroening
committed
use make_boolean_expr instead of exprt::make_bool
This ensures type safety.
1 parent 568dc07 commit 7a0493a

File tree

6 files changed

+39
-38
lines changed

6 files changed

+39
-38
lines changed

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -245,7 +245,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
245245
subtypes[1].remove(ID_C_volatile);
246246
subtypes[1].remove(ID_C_restricted);
247247

248-
expr.make_bool(gcc_types_compatible_p(subtypes[0], subtypes[1]));
248+
expr = make_boolean_expr(gcc_types_compatible_p(subtypes[0], subtypes[1]));
249249
expr.add_source_location()=source_location;
250250
}
251251
else if(expr.id()==ID_clang_builtin_convertvector)

‎src/util/simplify_expr.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
115115
if(type.id()==ID_floatbv)
116116
{
117117
ieee_floatt value(to_constant_expr(expr.op0()));
118-
expr.make_bool(value.get_sign());
118+
expr = make_boolean_expr(value.get_sign());
119119
return false;
120120
}
121121
else if(type.id()==ID_signedbv ||
@@ -124,7 +124,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
124124
const auto value = numeric_cast<mp_integer>(expr.op0());
125125
if(value.has_value())
126126
{
127-
expr.make_bool(*value >= 0);
127+
expr = make_boolean_expr(*value >= 0);
128128
return false;
129129
}
130130
}
@@ -561,7 +561,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
561561

562562
if(expr_type_id==ID_bool)
563563
{
564-
expr.make_bool(int_value!=0);
564+
expr = make_boolean_expr(int_value != 0);
565565
return false;
566566
}
567567

@@ -646,7 +646,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
646646

647647
if(expr_type_id==ID_bool)
648648
{
649-
expr.make_bool(int_value!=0);
649+
expr = make_boolean_expr(int_value != 0);
650650
return false;
651651
}
652652

‎src/util/simplify_expr_boolean.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
7575

7676
if(operands.empty())
7777
{
78-
expr.make_bool(negate);
78+
expr = make_boolean_expr(negate);
7979
return false;
8080
}
8181
else if(operands.size()==1)
@@ -135,13 +135,13 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
135135
op.type().id()==ID_bool &&
136136
expr_set.find(op.op0())!=expr_set.end())
137137
{
138-
expr.make_bool(expr.id()==ID_or);
138+
expr = make_boolean_expr(expr.id() == ID_or);
139139
return false;
140140
}
141141

142142
if(operands.empty())
143143
{
144-
expr.make_bool(expr.id()==ID_and);
144+
expr = make_boolean_expr(expr.id() == ID_and);
145145
return false;
146146
}
147147
else if(operands.size()==1)

‎src/util/simplify_expr_floatbv.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ bool simplify_exprt::simplify_isinf(exprt &expr)
2727
if(expr.op0().is_constant())
2828
{
2929
ieee_floatt value(to_constant_expr(expr.op0()));
30-
expr.make_bool(value.is_infinity());
30+
expr = make_boolean_expr(value.is_infinity());
3131
return false;
3232
}
3333

@@ -42,7 +42,7 @@ bool simplify_exprt::simplify_isnan(exprt &expr)
4242
if(expr.op0().is_constant())
4343
{
4444
ieee_floatt value(to_constant_expr(expr.op0()));
45-
expr.make_bool(value.is_NaN());
45+
expr = make_boolean_expr(value.is_NaN());
4646
return false;
4747
}
4848

@@ -57,7 +57,7 @@ bool simplify_exprt::simplify_isnormal(exprt &expr)
5757
if(expr.op0().is_constant())
5858
{
5959
ieee_floatt value(to_constant_expr(expr.op0()));
60-
expr.make_bool(value.is_normal());
60+
expr = make_boolean_expr(value.is_normal());
6161
return false;
6262
}
6363

@@ -119,7 +119,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
119119
if(type.id()==ID_floatbv)
120120
{
121121
ieee_floatt value(to_constant_expr(expr.op0()));
122-
expr.make_bool(value.get_sign());
122+
expr = make_boolean_expr(value.get_sign());
123123
return false;
124124
}
125125
else if(type.id()==ID_signedbv ||
@@ -128,7 +128,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
128128
mp_integer value;
129129
if(!to_integer(expr.op0(), value))
130130
{
131-
expr.make_bool(value>=0);
131+
expr = make_boolean_expr(value>=0);
132132
return false;
133133
}
134134
}
@@ -381,9 +381,9 @@ bool simplify_exprt::simplify_ieee_float_relation(exprt &expr)
381381
ieee_floatt f1(to_constant_expr(expr.op1()));
382382

383383
if(expr.id()==ID_ieee_float_notequal)
384-
expr.make_bool(f0.ieee_not_equal(f1));
384+
expr = make_boolean_expr(f0.ieee_not_equal(f1));
385385
else if(expr.id()==ID_ieee_float_equal)
386-
expr.make_bool(f0.ieee_equal(f1));
386+
expr = make_boolean_expr(f0.ieee_equal(f1));
387387
else
388388
UNREACHABLE;
389389

‎src/util/simplify_expr_int.cpp

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -846,7 +846,7 @@ bool simplify_exprt::simplify_extractbit(exprt &expr)
846846
src_bit_width,
847847
numeric_cast_v<std::size_t>(*index_converted_to_int));
848848

849-
expr.make_bool(bit);
849+
expr = make_boolean_expr(bit);
850850

851851
return false;
852852
}
@@ -1374,7 +1374,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
13741374
}
13751375
equal = tmp0_const->is_zero() && tmp1_const->is_zero();
13761376
}
1377-
expr.make_bool(expr.id() == ID_equal ? equal : !equal);
1377+
expr = make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
13781378
return false;
13791379
}
13801380

@@ -1384,13 +1384,13 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
13841384
fixedbvt f1(to_constant_expr(tmp1));
13851385

13861386
if(expr.id() == ID_ge)
1387-
expr.make_bool(f0>=f1);
1387+
expr = make_boolean_expr(f0 >= f1);
13881388
else if(expr.id()==ID_le)
1389-
expr.make_bool(f0<=f1);
1389+
expr = make_boolean_expr(f0 <= f1);
13901390
else if(expr.id()==ID_gt)
1391-
expr.make_bool(f0>f1);
1391+
expr = make_boolean_expr(f0 > f1);
13921392
else if(expr.id()==ID_lt)
1393-
expr.make_bool(f0<f1);
1393+
expr = make_boolean_expr(f0 < f1);
13941394
else
13951395
UNREACHABLE;
13961396

@@ -1402,13 +1402,13 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
14021402
ieee_floatt f1(to_constant_expr(tmp1));
14031403

14041404
if(expr.id() == ID_ge)
1405-
expr.make_bool(f0>=f1);
1405+
expr = make_boolean_expr(f0 >= f1);
14061406
else if(expr.id()==ID_le)
1407-
expr.make_bool(f0<=f1);
1407+
expr = make_boolean_expr(f0 <= f1);
14081408
else if(expr.id()==ID_gt)
1409-
expr.make_bool(f0>f1);
1409+
expr = make_boolean_expr(f0 > f1);
14101410
else if(expr.id()==ID_lt)
1411-
expr.make_bool(f0<f1);
1411+
expr = make_boolean_expr(f0 < f1);
14121412
else
14131413
UNREACHABLE;
14141414

@@ -1425,13 +1425,13 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
14251425
return true;
14261426

14271427
if(expr.id() == ID_ge)
1428-
expr.make_bool(r0>=r1);
1428+
expr = make_boolean_expr(r0 >= r1);
14291429
else if(expr.id()==ID_le)
1430-
expr.make_bool(r0<=r1);
1430+
expr = make_boolean_expr(r0 <= r1);
14311431
else if(expr.id()==ID_gt)
1432-
expr.make_bool(r0>r1);
1432+
expr = make_boolean_expr(r0 > r1);
14331433
else if(expr.id()==ID_lt)
1434-
expr.make_bool(r0<r1);
1434+
expr = make_boolean_expr(r0 < r1);
14351435
else
14361436
UNREACHABLE;
14371437

@@ -1450,13 +1450,13 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
14501450
return true;
14511451

14521452
if(expr.id() == ID_ge)
1453-
expr.make_bool(*v0 >= *v1);
1453+
expr = make_boolean_expr(*v0 >= *v1);
14541454
else if(expr.id()==ID_le)
1455-
expr.make_bool(*v0 <= *v1);
1455+
expr = make_boolean_expr(*v0 <= *v1);
14561456
else if(expr.id()==ID_gt)
1457-
expr.make_bool(*v0 > *v1);
1457+
expr = make_boolean_expr(*v0 > *v1);
14581458
else if(expr.id()==ID_lt)
1459-
expr.make_bool(*v0 < *v1);
1459+
expr = make_boolean_expr(*v0 < *v1);
14601460
else
14611461
UNREACHABLE;
14621462

@@ -1648,7 +1648,7 @@ bool simplify_exprt::simplify_inequality_no_constant(exprt &expr)
16481648

16491649
if(ok)
16501650
{
1651-
expr.make_bool(result);
1651+
expr = make_boolean_expr(result);
16521652
return false;
16531653
}
16541654
}

‎src/util/simplify_expr_pointer.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -443,7 +443,7 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
443443
bool equal = to_symbol_expr(tmp0.op0()).get_identifier() ==
444444
to_symbol_expr(tmp1.op0()).get_identifier();
445445

446-
expr.make_bool(expr.id()==ID_equal?equal:!equal);
446+
expr = make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
447447

448448
return false;
449449
}
@@ -454,15 +454,15 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
454454
bool equal = to_dynamic_object_expr(tmp0.op0()).get_instance() ==
455455
to_dynamic_object_expr(tmp1.op0()).get_instance();
456456

457-
expr.make_bool(expr.id() == ID_equal ? equal : !equal);
457+
expr = make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
458458

459459
return false;
460460
}
461461
else if(
462462
(tmp0.op0().id() == ID_symbol && tmp1.op0().id() == ID_dynamic_object) ||
463463
(tmp0.op0().id() == ID_dynamic_object && tmp1.op0().id() == ID_symbol))
464464
{
465-
expr.make_bool(expr.id() != ID_equal);
465+
expr = make_boolean_expr(expr.id() != ID_equal);
466466

467467
return false;
468468
}
@@ -580,7 +580,8 @@ bool simplify_exprt::simplify_is_dynamic_object(exprt &expr)
580580
const irep_idt identifier=to_symbol_expr(op.op0()).get_identifier();
581581

582582
// this is for the benefit of symex
583-
expr.make_bool(has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX));
583+
expr = make_boolean_expr(
584+
has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX));
584585
return false;
585586
}
586587
else if(op.op0().id()==ID_string_constant)

0 commit comments

Comments
 (0)