analyzer
analyzer copied to clipboard
Quickcheck int domain overflows
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
leqcheck.
Also, the current concrete value generators are unlikely to generate ikind bounds, so #1803 wouldn't have been caught most likely.