Someone added a bunch of random overflow & underflow checks to my code while changing something else. I think it's just a habit and all of these extra range checks are completely unnecessary - they're already checked elsewhere...
To make a point in the argument, I put the code into CBMC, removed those checks, and started a formal verification run.
The verification failed... 🤡
with a counterexample... 🤡
Follow
@niconiconi what do you use for verification? the most I ever used was this package where you had to annotate all your function signatures, but it still threw up a bunch of false positives anyway. is yours usable by someone without much training?
