--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on October 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Approach to compute if-else in Wp and Why



On 11.10.2012 16:44, Yannick Moy wrote:
> With Why2, you can pass the option --fast-wp to use a worst-case
> quadratic, linear in practice, weakest precondition similar to the one
> by Leino.
>
> With Why3, you do not have this option right now, but Jean-Christophe

What do Why2 without this option and Why3 do by default? Do you use 
another approach or the original wp-selection rule?
-- 
Best regards,
Boris