--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] my first frama verification



Hello Tim,

Le 21/08/2015 09:46, David MENTRE a écrit :
> It found 6 warnings:
> bits.c:12:[kernel] warning: accessing uninitialized left-value: assert
> \initialized(&byte);
> sha2.c:377:[kernel] warning: accessing uninitialized left-value: assert
> \initialized(&tmp);
> auth.c:32:[kernel] warning: accessing uninitialized left-value: assert
> \initialized(x);

In fact there are the 3 above warnings. They disappear if I put a 
constant value for "sz" in your main, e.g. 256. Value analysis's domain 
is non-relational, so it does not keep track of relation ships between 
variables. This is a case where one should use the trick I told you 
previously (use a constant N, changing its value externally).

I also noticed a lot of dead code that seems suspicious, e.g. in 
checkSeq() and getSeq(). I'm not using the same version of frama-c as 
you and the same configuration options, so the issue might be on my 
side. But at least double check that you don't have unexpected 
dead-code: it is usually the sign of an analysis issue.

Best regards,
david