--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on August 2015 ---
Hello Boris, Le 26/08/2015 22:37, Boris Yakobowski a écrit : > With the open-source version, I obtain the same results as Tim (at least > until I get bored, and kill the analysis): no initialization warning. On > the other hand, I can reproduce your results, including the analysis > time, by activating option -val-slevel-merge-after-loop @all. Is this > option set by TrustInSoft Analyzer? Yes. > Given the way Tim's main function is written, this option completely > changes the number of separate paths that are analyzed: > - with the option set, only one analysis is performed, with an imprecise > value for sz, ksz, buf and kbuf. This is due to the merge that occurs at > the beginning of each loop, regardless of the number of states that > initially enters the loop. > - without this option, the two loops that initialize buf and kbuf > separate sz and ksz into all possible values, resulting in 64 * 256 > different analyses. Thank you for the explanation, very enlightening. Best regards, david