--- layout: fc_discuss_archives title: Message 42 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.



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