--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on April 2012 ---
Hi Pascal, the quote is a nice touch, but a workable explanation would be even nicer. > To answer your question, you cannot prove the kind of functional > property you desire with the value analysis. Okay... but why? In this case the value analysis plugin does _not_ output "I am intrinsically not able to prove what you want because of my inner working". It _just_ outputs ... unknown. It outputs "unknown" _as well_ as a mean to say "I can not prove nor disprove this property because it may be false in some cases and true in other". Which is an indication that either the analysis was not precise enough, or that the property genuinely does not hold and a bug was found. Three cases, at least. How one can learn to distinguish between them, if one does not ask and receives useful answers? Furthermore, I haven't asked privately or whatever, but on a public mailing list so that the answer may be archived and profitable to others in the future; currently, I doubt people can learn much about Frama-C thanks to this thread, apart that one of its developers loves Feynman quotes. Thanks, Sylvain