boolbvt error handling for byte_extract #2501
Conversation
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 8301743).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77795181
|
I'll take a look and provide comments on this: it should be co-ordinated with existing open issues on cleaning up exceptions and also the refactoring of |
|
In light of #3290 merged, this needs to be reconsidered and at bare minimum rebased. |
There was a problem hiding this comment.
OK but I agree with @tautschnig 's comments about whether this is the thing to do.
kroening
force-pushed
the
boolbvt_error_handling
branch
from
8301743 to
56194ef
Compare
There was a problem hiding this comment.
Diffblue compatibility check is currently unavailable.
Please create manual bump.
(cbmc commit: 56194ef).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90716260
There was a problem hiding this comment.
Now that we've merged the various byte extract/byte update fixes: this seems like the right thing to do, except it's actually needed in more places: tautschnig@deaa887 might provide guidance.
|
I'm of course biased, but I'd by now actually prefer #4651 (plus a follow-up PR that replaces the two remaining two throws by invariants). |
|
I've not put up #4691, which ought to make this one unnecessary. |
|
Closing as this is no longer applicable with #4691 merged. |
boolbvt does not throw exceptions in case unsupported expressions are given; instead, it calls conversion_failed, which calls ignoring().