Refactor boolbvt::convert_overflow
#6752
Conversation
Because the code used for one operand vs two operands is slightly different and because this facilitates a more type-specific implementation.
thomasspriggs
requested review from
martin-cs,
kroening,
tautschnig and
peterschrammel
as code owners
| literalt boolbvt::convert_unary_overflow(const unary_overflow_exprt &expr) | ||
| { | ||
| if( |
There was a problem hiding this comment.
There really is just this single unary_minus_overflow_exprt that exists for this case, so I would suggest to make this convert_unary_minus_overflow(const unary_minus_overflow_exprt &expr).
There was a problem hiding this comment.
unary_minus_overflow_exprt and unary_overflow_exprt are currently equivalent. This fact could be used to simplify the way they are currently used, or even to remove unary_overflow_exprt and just keep unary_minus_overflow_exprt. However I think it would make it more difficult to add other kinds of unary overflow expressions. Adding more checks isn't something I am planning to work on but does seem worth considering. The following example unary operations might be considered for overflow checks -
- The existing
abs_exprt. - Increment operators
++/--. - The trigonometric
tan/ "tangent" operation. - Could a narrowing cast be considered to overflow?
This PR is based on the refactoring suggestion from @tautschnig in this code review comment - #6744 (comment)
This PR should be purely refactoring only. As in both implementations should produce the same results given the same inputs. Many of the remaining differences between the different operators are down to differences in error / unexpected case handling. The implementation could be further simplified based on unifying whether these checks result in skipped conversions or invariant violations for the different operators. However I would prefer not to make more functional changes as part of this PR.