--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on August 2015 ---
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