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.

On Fri, 2012-04-13 at 13:16 +0200, sylvain nahas wrote:
> 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?

unknown means just that. It's impossible that a program verification
tool is always able to decide if property holds or not.

In your case, the reason is that the value analysis can't handle
equality.
-- 
Best regards,
Boris