@@ -804,7 +804,7 @@ void goto_checkt::integer_overflow_check(
804
804
805
805
add_guarded_property (
806
806
not_exprt (overflow),
807
- " arithmetic overflow on " + kind+ " " + expr.id_string (),
807
+ " arithmetic overflow on " + kind + " " + expr.id_string (),
808
808
" overflow" ,
809
809
expr.find_source_location (),
810
810
expr,
@@ -818,7 +818,7 @@ void goto_checkt::integer_overflow_check(
818
818
819
819
add_guarded_property (
820
820
not_exprt (overflow),
821
- " arithmetic overflow on " + kind+ " " + expr.id_string (),
821
+ " arithmetic overflow on " + kind + " " + expr.id_string (),
822
822
" overflow" ,
823
823
expr.find_source_location (),
824
824
expr,
@@ -928,7 +928,7 @@ void goto_checkt::float_overflow_check(
928
928
929
929
add_guarded_property (
930
930
overflow_check,
931
- " arithmetic overflow on floating-point " + kind,
931
+ " arithmetic overflow on floating-point " + kind,
932
932
" overflow" ,
933
933
expr.find_source_location (),
934
934
expr,
@@ -1129,7 +1129,7 @@ void goto_checkt::pointer_validity_check(
1129
1129
{
1130
1130
add_guarded_property (
1131
1131
c.assertion ,
1132
- " dereference failure: " + c.description ,
1132
+ " dereference failure: " + c.description ,
1133
1133
" pointer dereference" ,
1134
1134
expr.find_source_location (),
1135
1135
expr,
@@ -1328,7 +1328,7 @@ void goto_checkt::bounds_check(
1328
1328
1329
1329
add_guarded_property (
1330
1330
inequality,
1331
- name+ " lower bound" ,
1331
+ name + " lower bound" ,
1332
1332
" array bounds" ,
1333
1333
expr.find_source_location (),
1334
1334
expr,
@@ -1385,7 +1385,7 @@ void goto_checkt::bounds_check(
1385
1385
1386
1386
add_guarded_property (
1387
1387
precond,
1388
- name+ " dynamic object upper bound" ,
1388
+ name + " dynamic object upper bound" ,
1389
1389
" array bounds" ,
1390
1390
expr.find_source_location (),
1391
1391
expr,
@@ -1462,7 +1462,7 @@ void goto_checkt::bounds_check(
1462
1462
1463
1463
add_guarded_property (
1464
1464
implies_exprt (type_matches_size, inequality),
1465
- name+ " upper bound" ,
1465
+ name + " upper bound" ,
1466
1466
" array bounds" ,
1467
1467
expr.find_source_location (),
1468
1468
expr,
@@ -1503,7 +1503,7 @@ void goto_checkt::add_guarded_property(
1503
1503
std::string source_expr_string;
1504
1504
get_language_from_mode (mode)->from_expr (src_expr, source_expr_string, ns);
1505
1505
1506
- t->source_location .set_comment (comment+ " in " + source_expr_string);
1506
+ t->source_location .set_comment (comment + " in " + source_expr_string);
1507
1507
t->source_location .set_property_class (property_class);
1508
1508
}
1509
1509
}
@@ -1652,12 +1652,12 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
1652
1652
if (expr.id () == ID_exists || expr.id () == ID_forall)
1653
1653
return ;
1654
1654
1655
- if (expr.id ()== ID_address_of)
1655
+ if (expr.id () == ID_address_of)
1656
1656
{
1657
1657
check_rec_address (to_address_of_expr (expr).object (), guard);
1658
1658
return ;
1659
1659
}
1660
- else if (expr.id ()== ID_and || expr.id ()== ID_or)
1660
+ else if (expr.id () == ID_and || expr.id () == ID_or)
1661
1661
{
1662
1662
check_rec_logical_op (expr, guard);
1663
1663
return ;
0 commit comments