--- layout: fc_discuss_archives title: Message 17 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 10/11/2012 04:15 PM, Boris Hollas wrote:
> Hello,
>
> what approach do Wp or Why use to avoid the exponential growth of the
> VCs due to the computation of the selection (branching) rule? Do you use
> "passification" as proposed by Leino? Any references?

In Why, it depends which version you are using for VC generation. The 
page http://krakatoa.lri.fr/ summarizes which version of Why (2 or 3) is 
used in Frama-C by default, and if the other version is available on option.

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 
Filli?tre has started implementing it, and Johannes Kanig and I have 
agreed to contribute to this implementation. So coming in a few months.
-- 
Yannick Moy, Senior Software Engineer, AdaCore