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

Le 27/08/2015 08:26, David MENTRE a écrit :
> 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.

For the record, using exactly the same configuration as Tim (i.e. 
without your optimizations described in 
https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2015-August/004926.html) 
but without the option -val-slevel-merge-after-loop @all, the analysis 
with TIS Analyzer takes 5 hours, i.e. about two times faster than Tim 
analysis (and without warning).

Best regards,
david