@@ -2290,16 +2290,14 @@ std::string expr2ct::convert_initializer_list(const exprt &src)
22902290 return dest;
22912291}
22922292
2293- std::string expr2ct::convert_rox (const exprt &src, unsigned precedence)
2293+ std::string expr2ct::convert_rox (const shift_exprt &src, unsigned precedence)
22942294{
22952295 // AAAA rox n == (AAAA lhs_op n % width(AAAA))
22962296 // | (AAAA rhs_op (width(AAAA) - n % width(AAAA)))
22972297 // 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);
23002298 // Get AAAA and if it's signed wrap it in a cast to remove
23012299 // the sign since this messes with C shifts
2302- exprt & op0 = rotate_expr .op ();
2300+ exprt op0 = src .op ();
23032301 size_t type_width;
23042302 if (can_cast_type<signedbv_typet>(op0.type ()))
23052303 {
@@ -2316,17 +2314,15 @@ std::string expr2ct::convert_rox(const exprt &src, unsigned precedence)
23162314 }
23172315 else
23182316 {
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;
23222318 }
23232319 // Construct the "width(AAAA)" constant
23242320 const exprt width_expr =
2325- from_integer (type_width, rotate_expr .distance ().type ());
2321+ from_integer (type_width, src .distance ().type ());
23262322 // Apply modulo to n since shifting will overflow
23272323 // That is: 0001 << 4 == 0, but 0001 rol 4 == 0001
23282324 const exprt distance_modulo_width =
2329- mod_exprt (rotate_expr .distance (), width_expr);
2325+ mod_exprt (src .distance (), width_expr);
23302326 // Now put the pieces together
23312327 // width(AAAA) - (n % width(AAAA))
23322328 const auto complement_width_expr =
@@ -3861,7 +3857,7 @@ std::string expr2ct::convert_with_precedence(
38613857 return convert (src.type ());
38623858
38633859 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);
38653861
38663862 auto function_string_opt = convert_function (src);
38673863 if (function_string_opt.has_value ())
0 commit comments