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