seahorn/crab

Implement a sound domain for machine integer arithmetic

caballa opened this issue · 1 comments

caballa commented

The wrapped interval domain is a good candidate:
https://jorgenavas.github.io/papers/wrapped-intervals-aplas12.pdf

caballa commented

I implemented the above wrapped interval domain and committed here 81cc35f.
Although there are still many things to implement as described in the log message of this commit, I consider for now this issue closed.