--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on April 2012 ---
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