analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Quickcheck int domain overflows

Open sim642 opened this issue 4 months ago • 0 comments

As I noted in #1804:

domain tests don't check the overflow flags of abstract operator results. Moreover, when the concrete operator calculates the overflowed value, it's forced into bounds by the abstraction before leq check.

Also, the current concrete value generators are unlikely to generate ikind bounds, so #1803 wouldn't have been caught most likely.

sim642 avatar Aug 14 '25 16:08 sim642