--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on April 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Value analysis] Validating a function with behavior spec.



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