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] 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