--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on May 2010 ---
[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