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