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] Making frama-c-gui a read-only tool?

Thanks Yannick for the pointers on your memcached-based solution !
To complete your notes on using Why3, I would just mention that in Frama-C/WP (current version), using `-wp-prover why3ide` actually uses a why3-session to store and reuse proof results.
	L.

> Le 6 févr. 2017 à 11:39, Yannick Moy <moy at adacore.com> a écrit :
> 
> -- Loïc Correnson (2017-02-06)
>> 
>> For the SMT part, we have on ongoing task in VESSEDIA project for caching at a large scale proof obligation results, but we are just at the beginning of the project.
> 
> In case our experience can be useful for Frama-C, we have recently added support for memcached in SPARK, so that VCs proved across a team are available for any other member of the team. Or VCs proved by a remote server during a nightly run are available for your daily runs. The integration with memcached is really simple, so simple in fact that we originally had done it only internally for developers, to speed up local testing. But given the user interest, this is now an official feature. This is described here: http://www.spark-2014.org/entries/detail/hash-it-and-cache-it <http://www.spark-2014.org/entries/detail/hash-it-and-cache-it>
> 
>> For this new interactive prover, a complete journal of what have been proved (and how) is kept. We have actually distinguish between two interactive modes : one mode for upgrading, editing or tuning proofs or SMT parameters, and a replay-mode which is read-only.
> 
> AFAIU, Jens was interested in yet another mode, a "display" mode where nothing is recomputed, but simply results are displayed. That's also something we added to SPARK in the past year, distinguishing the "replay" mode that attempts to redo proofs following what is stored in the Why3 session file, and the "display" mode that just displays the stored results from the Why3 session file (tagging specially those results that may be obsolete). At some point we tried to display results based on previously displayed outputs (which were saved in files on disk) but that did not work well with the ability to call the analyzer at different levels of granularity: maybe your previous run was on a single subprogram, and now you want to display the results for the complete program. So we use now the Why3 session file instead, even if it's slightly slower.
> 
> --
> Yannick Moy, Senior Software Engineer, AdaCore
> 
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170206/1d53599e/attachment.html>