Skip to content

Commit 0bdf097

Browse files
author
Daniel Kroening
committed
use make_boolean_expr instead of exprt::make_bool
This ensures type safety.
1 parent c1c5fa7 commit 0bdf097

6 files changed

+40
-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: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include "arith_tools.h"
1212
#include "expr.h"
13+
#include "expr_util.h"
1314
#include "ieee_float.h"
1415
#include "invariant.h"
1516
#include "namespace.h"
@@ -27,7 +28,7 @@ bool simplify_exprt::simplify_isinf(exprt &expr)
2728
if(expr.op0().is_constant())
2829
{
2930
ieee_floatt value(to_constant_expr(expr.op0()));
30-
expr.make_bool(value.is_infinity());
31+
expr = make_boolean_expr(value.is_infinity());
3132
return false;
3233
}
3334

@@ -42,7 +43,7 @@ bool simplify_exprt::simplify_isnan(exprt &expr)
4243
if(expr.op0().is_constant())
4344
{
4445
ieee_floatt value(to_constant_expr(expr.op0()));
45-
expr.make_bool(value.is_NaN());
46+
expr = make_boolean_expr(value.is_NaN());
4647
return false;
4748
}
4849

@@ -57,7 +58,7 @@ bool simplify_exprt::simplify_isnormal(exprt &expr)
5758
if(expr.op0().is_constant())
5859
{
5960
ieee_floatt value(to_constant_expr(expr.op0()));
60-
expr.make_bool(value.is_normal());
61+
expr = make_boolean_expr(value.is_normal());
6162
return false;
6263
}
6364

@@ -119,7 +120,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
119120
if(type.id()==ID_floatbv)
120121
{
121122
ieee_floatt value(to_constant_expr(expr.op0()));
122-
expr.make_bool(value.get_sign());
123+
expr = make_boolean_expr(value.get_sign());
123124
return false;
124125
}
125126
else if(type.id()==ID_signedbv ||
@@ -128,7 +129,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
128129
mp_integer value;
129130
if(!to_integer(expr.op0(), value))
130131
{
131-
expr.make_bool(value>=0);
132+
expr = make_boolean_expr(value>=0);
132133
return false;
133134
}
134135
}
@@ -381,9 +382,9 @@ bool simplify_exprt::simplify_ieee_float_relation(exprt &expr)
381382
ieee_floatt f1(to_constant_expr(expr.op1()));
382383

383384
if(expr.id()==ID_ieee_float_notequal)
384-
expr.make_bool(f0.ieee_not_equal(f1));
385+
expr = make_boolean_expr(f0.ieee_not_equal(f1));
385386
else if(expr.id()==ID_ieee_float_equal)
386-
expr.make_bool(f0.ieee_equal(f1));
387+
expr = make_boolean_expr(f0.ieee_equal(f1));
387388
else
388389
UNREACHABLE;
389390

‎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
}
@@ -1425,7 +1425,7 @@ bool simplify_exprt::simplify_inequality_both_constant(exprt &expr)
14251425
}
14261426
equal = tmp0_const.is_zero() && tmp1_const.is_zero();
14271427
}
1428-
expr.make_bool(expr.id() == ID_equal ? equal : !equal);
1428+
expr = make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
14291429
return false;
14301430
}
14311431

@@ -1435,13 +1435,13 @@ bool simplify_exprt::simplify_inequality_both_constant(exprt &expr)
14351435
fixedbvt f1(tmp1_const);
14361436

14371437
if(expr.id() == ID_ge)
1438-
expr.make_bool(f0 >= f1);
1438+
expr = make_boolean_expr(f0 >= f1);
14391439
else if(expr.id() == ID_le)
1440-
expr.make_bool(f0 <= f1);
1440+
expr = make_boolean_expr(f0 <= f1);
14411441
else if(expr.id() == ID_gt)
1442-
expr.make_bool(f0 > f1);
1442+
expr = make_boolean_expr(f0 > f1);
14431443
else if(expr.id() == ID_lt)
1444-
expr.make_bool(f0 < f1);
1444+
expr = make_boolean_expr(f0 < f1);
14451445
else
14461446
UNREACHABLE;
14471447

@@ -1453,13 +1453,13 @@ bool simplify_exprt::simplify_inequality_both_constant(exprt &expr)
14531453
ieee_floatt f1(tmp1_const);
14541454

14551455
if(expr.id() == ID_ge)
1456-
expr.make_bool(f0 >= f1);
1456+
expr = make_boolean_expr(f0 >= f1);
14571457
else if(expr.id() == ID_le)
1458-
expr.make_bool(f0 <= f1);
1458+
expr = make_boolean_expr(f0 <= f1);
14591459
else if(expr.id() == ID_gt)
1460-
expr.make_bool(f0 > f1);
1460+
expr = make_boolean_expr(f0 > f1);
14611461
else if(expr.id() == ID_lt)
1462-
expr.make_bool(f0 < f1);
1462+
expr = make_boolean_expr(f0 < f1);
14631463
else
14641464
UNREACHABLE;
14651465

@@ -1476,13 +1476,13 @@ bool simplify_exprt::simplify_inequality_both_constant(exprt &expr)
14761476
return true;
14771477

14781478
if(expr.id() == ID_ge)
1479-
expr.make_bool(r0 >= r1);
1479+
expr = make_boolean_expr(r0 >= r1);
14801480
else if(expr.id() == ID_le)
1481-
expr.make_bool(r0 <= r1);
1481+
expr = make_boolean_expr(r0 <= r1);
14821482
else if(expr.id() == ID_gt)
1483-
expr.make_bool(r0 > r1);
1483+
expr = make_boolean_expr(r0 > r1);
14841484
else if(expr.id() == ID_lt)
1485-
expr.make_bool(r0 < r1);
1485+
expr = make_boolean_expr(r0 < r1);
14861486
else
14871487
UNREACHABLE;
14881488

@@ -1501,13 +1501,13 @@ bool simplify_exprt::simplify_inequality_both_constant(exprt &expr)
15011501
return true;
15021502

15031503
if(expr.id() == ID_ge)
1504-
expr.make_bool(*v0 >= *v1);
1504+
expr = make_boolean_expr(*v0 >= *v1);
15051505
else if(expr.id() == ID_le)
1506-
expr.make_bool(*v0 <= *v1);
1506+
expr = make_boolean_expr(*v0 <= *v1);
15071507
else if(expr.id() == ID_gt)
1508-
expr.make_bool(*v0 > *v1);
1508+
expr = make_boolean_expr(*v0 > *v1);
15091509
else if(expr.id() == ID_lt)
1510-
expr.make_bool(*v0 < *v1);
1510+
expr = make_boolean_expr(*v0 < *v1);
15111511
else
15121512
UNREACHABLE;
15131513

@@ -1669,7 +1669,7 @@ bool simplify_exprt::simplify_inequality_no_constant(exprt &expr)
16691669

16701670
if(ok)
16711671
{
1672-
expr.make_bool(result);
1672+
expr = make_boolean_expr(result);
16731673
return false;
16741674
}
16751675
}

‎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)