Skip to content

Commit 201a334

Browse files
committed
Pointer types must not be used with bit-level operators
Any such use requires a type cast.
1 parent b186e25 commit 201a334

File tree

1 file changed

+0
-15
lines changed

1 file changed

+0
-15
lines changed

src/solvers/flattening/bv_pointers.cpp

-15
Original file line numberDiff line numberDiff line change
@@ -421,21 +421,6 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
421421

422422
return bv;
423423
}
424-
else if(expr.id()==ID_lshr ||
425-
expr.id()==ID_shl)
426-
{
427-
return SUB::convert_shift(to_shift_expr(expr));
428-
}
429-
else if(expr.id()==ID_bitand ||
430-
expr.id()==ID_bitor ||
431-
expr.id()==ID_bitnot)
432-
{
433-
return convert_bitwise(expr);
434-
}
435-
else if(expr.id()==ID_concatenation)
436-
{
437-
return SUB::convert_concatenation(expr);
438-
}
439424
else if(expr.id()==ID_byte_extract_little_endian ||
440425
expr.id()==ID_byte_extract_big_endian)
441426
{

0 commit comments

Comments
 (0)