--- layout: fc_discuss_archives title: Message 53 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



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