Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about a simple example and jessie

Hello,

> I'm very surprised that you could prove your post-condition with HAVOC. For
> me you need a smart loop invariant for the inner loop to prove it

I have been wondering about this too ever since the original question.
Does HAVOC aim at being correct? Is it stated somewhere that
the program is correct when HAVOC remains silent?

Pascal