search

AllanBlanchard / tutoriel_wp

Frama-C and WP tutorial
Other
52 stars 16 forks source link

Exercise 7.3.6.1: additionnal assert needed to prove post-condition #29

Closed qsantos closed 4 years ago

qsantos commented 4 years ago

Using the code from the correction of 7.3.6.1 in Frama-C 21 Scandium, WP fails to prove the post-condition of sum_n with either Alt-Ergo or CVC4. Somehow, adding //@ assert 0 <= n * (n + 1); allows either to prove it.

AllanBlanchard commented 4 years ago

I think that there is a small regression in WP, I'll had the assertion for now, but I will also have a look to WP.

Thank you!

AllanBlanchard commented 4 years ago

Issue is fixed on master.

qsantos commented 4 years ago

Thanks for the promptness of your reply!

AllanBlanchard commented 4 years ago

Note, just for fun : using -warn-unsigned-overflow provide the assertion so that the bug is hidden ^^

qsantos commented 4 years ago

Oh, right. I turned it off for some of the exercises of chapter 7 and must have forgotten to turn it back on. By the way, thanks a lot for your manual. It's a gem!