Overflow checking confusion

[Vladimir Klebanov]

Hello,

the attached code produces upon

cbmc guineapig.c --function reduce --unsigned-overflow-check
--signed-overflow-check

a bunch of overflow check failures even though I am told the
operations are not supposed to overflow.

Is it a problem with CBMC or me not understanding C or the meaning of
the above command-line options?

Thanks!

Vladimir

[Michael Tautschnig]

Hi Vladimir,

[...]

Not at all, it was just another copy&paste-type error:

https://github.com/diffblue/cbmc/pull/414

Thank you very much for raising this, and I hope you're ok with the example
being included as regression test (with attribution in the commit message).

Best,
Michael

[Vladimir Klebanov]

Hi Michael,

On Tue, Jan 10, 2017 at 12:54 AM, Michael Tautschnig
<michael.t...@gmail.com> wrote:
> Not at all, it was just another copy&paste-type error:
> https://github.com/diffblue/cbmc/pull/414

Ah, that explains it. Many thanks for investigating and fixing!

> Thank you very much for raising this, and I hope you're ok with the example
> being included as regression test (with attribution in the commit message).

Sure. If possible, please attribute also to Emilia Käsper and Bart Jacobs.

Thanks,

Vladimir