Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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