--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on October 2012 ---
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