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
- Subject: [Frama-c-discuss] my first frama verification
- From: dmentre at linux-france.org (David MENTRE)
- Date: Fri, 21 Aug 2015 11:20:57 +0200
- In-reply-to: <55D6D766.9000208@linux-france.org>
- References: <CAGSRWbgk8sbO4DKZ-ij8jbDALBgt8e7K4dAto-puDQZqbu+76Q@mail.gmail.com> <55D6CCA5.901@linux-france.org> <55D6D766.9000208@linux-france.org>
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
- Follow-Ups:
- [Frama-c-discuss] my first frama verification
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] my first frama verification
- References:
- [Frama-c-discuss] my first frama verification
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] my first frama verification
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] my first frama verification
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] my first frama verification
- Prev by Date: [Frama-c-discuss] my first frama verification
- Next by Date: [Frama-c-discuss] my first frama verification
- Previous by thread: [Frama-c-discuss] my first frama verification
- Next by thread: [Frama-c-discuss] my first frama verification
- Index(es):