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

I didn't "save" the analysis state, but I did keep the analysis
output.  It's very large, 4MB when compressed:

http://www.thenewsh.com/~newsham/frama/big-analysis.txt.gz


On Fri, Aug 21, 2015 at 6:41 AM, David MENTRE <dmentre at linux-france.org>
wrote:

> Hello Tim,
>
> Le 21/08/2015 18:01, Tim Newsham a écrit :
>
>> 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'm surprised that you have no warning using a value range for "sz"
> instead of a constant value, but if you say so.
>
> Next time, save the analysis log in a file.
>
> What dead code are you seeing?  Everything in seq.c should
>> be important and useful.
>>
>
> It appears that -lib-entry option triggers a different behaviour in
> open-source Frama-C and TIS Analyzer for fopen() result. Without this
> option, I found no warning on your code (sz == 256, verification took 1min)
> and the dead code disappeared (I did not make an exhaustive review though).
>
>
> DISCLAIMER²: I just wanted to compare very quickly the behaviour of TIS
> Analyzer on your code, so I haven't made a detailed review of the option
> used, the driver and analysis result. I might have missed points that
> invalidate my analysis result.
>
>
> There is still one of your assertion which is not proved (in
> frama-driver.c, just after the call to auth()). Interestingly, the
> postcondition of auth(), which is equivalent to this assert, is proved. I
> suspect WP (or Jessie) could be used to make the logical consequence in
> frama-driver.c and prove the assert but I did not try it. Or only use Value
> analysis and just proper re-writing of the logical expressions (I did some
> attempts, without much success).
>
> Nonetheless, TIS Analyzer produces results in short time (1min vs.
> 818min), which is encouraging. It would be interesting to see if one could
> gain some time using only the open-source version but I unfortunately don't
> have time for this (and already spent too much time in this use case ;-) ).
>
> I had a quick look at your proof.txt file and found no obvious missing.
> You'll probably need to detail *all* analysis parameters, as each one of
> them could influence the analysis (e.g. -lib-entry). But your Frama script
> gives the definitive answer, so probably better just to reference it.
>
>
> 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/b275aa93/attachment.html>