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

all of the warnings go away in frama-c if I use the parameters
in my ./Frama file (in the tgz).  It seems if I crank up the
slevel high enough, and use the val-split-return-auto
argument, it tries enough paths to know the relation between
the buffer and the sz in each analysis path. very brute force...

I did try a separate version where I fix the size with a define
and then use an external driver program to run frama once with
each size I care about.  Since I am varying over three parameters
(work factor, key size, input buffer size)
there is a big space to cover, and I never ran this analysis fully
to completion, but I suspect it might still be faster than the
13hrs to analyze with the brute force method..

What dead code are you seeing?  Everything in seq.c should
be important and useful.


On Thu, Aug 20, 2015 at 11:20 PM, David MENTRE <dmentre at linux-france.org>
wrote:

> 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
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>



-- 
Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150821/0ca487b1/attachment.html>