@@ -985,11 +985,12 @@ void goto_check_ct::integer_overflow_check(
985
985
// a shift of zero isn't overflow;
986
986
// else check the top bits
987
987
add_guarded_property (
988
- disjunction ({neg_value_shift,
989
- neg_dist_shift,
990
- dist_too_large,
991
- op_zero,
992
- top_bits_zero}),
988
+ disjunction (
989
+ {neg_value_shift,
990
+ neg_dist_shift,
991
+ dist_too_large,
992
+ op_zero,
993
+ top_bits_zero}),
993
994
" arithmetic overflow on signed shl" ,
994
995
" overflow" ,
995
996
expr.find_source_location (),
@@ -1553,9 +1554,10 @@ void goto_check_ct::bounds_check_index(
1553
1554
exprt p_offset =
1554
1555
pointer_offset (to_dereference_expr (ode.root_object ()).pointer ());
1555
1556
1556
- effective_offset = plus_exprt{p_offset,
1557
- typecast_exprt::conditional_cast (
1558
- effective_offset, p_offset.type ())};
1557
+ effective_offset = plus_exprt{
1558
+ p_offset,
1559
+ typecast_exprt::conditional_cast (
1560
+ effective_offset, p_offset.type ())};
1559
1561
}
1560
1562
1561
1563
exprt zero = from_integer (0 , ode.offset ().type ());
@@ -1824,9 +1826,10 @@ bool goto_check_ct::check_rec_member(
1824
1826
deref.pointer (), pointer_type (char_type ()));
1825
1827
1826
1828
const exprt new_address_casted = typecast_exprt::conditional_cast (
1827
- plus_exprt{char_pointer,
1828
- typecast_exprt::conditional_cast (
1829
- member_offset_opt.value (), pointer_diff_type ())},
1829
+ plus_exprt{
1830
+ char_pointer,
1831
+ typecast_exprt::conditional_cast (
1832
+ member_offset_opt.value (), pointer_diff_type ())},
1830
1833
new_pointer_type);
1831
1834
1832
1835
dereference_exprt new_deref{new_address_casted};
@@ -2367,8 +2370,9 @@ goto_check_ct::get_pointer_is_null_condition(
2367
2370
if (flags.is_unknown () || flags.is_uninitialized () || flags.is_null ())
2368
2371
{
2369
2372
return {conditiont{
2370
- or_exprt{is_in_bounds_of_some_explicit_allocation (address, size),
2371
- not_exprt (null_pointer (address))},
2373
+ or_exprt{
2374
+ is_in_bounds_of_some_explicit_allocation (address, size),
2375
+ not_exprt (null_pointer (address))},
2372
2376
" pointer NULL" }};
2373
2377
}
2374
2378
0 commit comments