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] [Value analysis] Validating a function with behavior spec.

  • Subject: [Frama-c-discuss] [Value analysis] Validating a function with behavior spec.
  • From: sylvain.nahas at googlemail.com (sylvain nahas)
  • Date: Fri, 13 Apr 2012 13:16:49 +0200
  • In-reply-to: <CAOH62JgyUC8+2cHf-bsPmVnWcL+JxyV88mnVo9gHc0j5Ym=JqQ@mail.gmail.com>
  • References: <CAFaEDLCHYJtescjnsqs6gE5q_Nx5+CWSg_3AD=f9pN_AHhq4=w@mail.gmail.com> <CAOH62JgyUC8+2cHf-bsPmVnWcL+JxyV88mnVo9gHc0j5Ym=JqQ@mail.gmail.com>
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