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

[Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated



-- Fran?ois Bobot (2013-10-18)
> 
> If you are using the plugin Jessie or the plugin WP, you can already prove your goal using why3. And why3 has a session mechanism through the commands why3ide, why3replayer and why3session. A session allow you the kind of cache David is referring.
> 
> In fact GNATprove also use why3 for that ;).


not only! :)
We use compiler-like dependencies plus semantic dependencies to completely avoid regenerating VCs that cannot be impacted by a source code change. And on top of that, we use Why3 session mechanism (with hashes computed for VCs) to avoid calling the prover on a VC already proved.
--
Yannick Moy, Senior Software Engineer, AdaCore