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