@@ -2290,16 +2290,14 @@ std::string expr2ct::convert_initializer_list(const exprt &src)
2290
2290
return dest;
2291
2291
}
2292
2292
2293
- std::string expr2ct::convert_rox (const exprt &src, unsigned precedence)
2293
+ std::string expr2ct::convert_rox (const shift_exprt &src, unsigned precedence)
2294
2294
{
2295
2295
// AAAA rox n == (AAAA lhs_op n % width(AAAA))
2296
2296
// | (AAAA rhs_op (width(AAAA) - n % width(AAAA)))
2297
2297
// Where lhs_op and rhs_op depend on whether it is rol or ror
2298
- // auto rotate_expr = to_binary_expr(src);
2299
- auto rotate_expr = expr_checked_cast<shift_exprt>(src);
2300
2298
// Get AAAA and if it's signed wrap it in a cast to remove
2301
2299
// the sign since this messes with C shifts
2302
- exprt & op0 = rotate_expr .op ();
2300
+ exprt op0 = src .op ();
2303
2301
size_t type_width;
2304
2302
if (can_cast_type<signedbv_typet>(op0.type ()))
2305
2303
{
@@ -2316,17 +2314,15 @@ std::string expr2ct::convert_rox(const exprt &src, unsigned precedence)
2316
2314
}
2317
2315
else
2318
2316
{
2319
- // Type that can't be represented as bitvector
2320
- // get some kind of width in a potentially unsafe way
2321
- type_width = op0.type ().get_size_t (" width" );
2317
+ UNREACHABLE;
2322
2318
}
2323
2319
// Construct the "width(AAAA)" constant
2324
2320
const exprt width_expr =
2325
- from_integer (type_width, rotate_expr .distance ().type ());
2321
+ from_integer (type_width, src .distance ().type ());
2326
2322
// Apply modulo to n since shifting will overflow
2327
2323
// That is: 0001 << 4 == 0, but 0001 rol 4 == 0001
2328
2324
const exprt distance_modulo_width =
2329
- mod_exprt (rotate_expr .distance (), width_expr);
2325
+ mod_exprt (src .distance (), width_expr);
2330
2326
// Now put the pieces together
2331
2327
// width(AAAA) - (n % width(AAAA))
2332
2328
const auto complement_width_expr =
@@ -3861,7 +3857,7 @@ std::string expr2ct::convert_with_precedence(
3861
3857
return convert (src.type ());
3862
3858
3863
3859
else if (src.id () == ID_rol || src.id () == ID_ror)
3864
- return convert_rox (src, precedence);
3860
+ return convert_rox (to_shift_expr ( src) , precedence);
3865
3861
3866
3862
auto function_string_opt = convert_function (src);
3867
3863
if (function_string_opt.has_value ())
0 commit comments