--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on May 2020 ---
Thank you all for your help and pointers. This discussion has been very helpful (and much appreciated)!! I will look carefully and reach out to individual responders. Mike From: Frama-c-discuss <frama-c-discuss-bounces at lists.gforge.inria.fr> on behalf of CORRENSON Loic <loic.correnson at cea.fr> Reply-To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> Date: Monday, May 18, 2020 at 4:40 AM To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> Subject: RE: [EXTERNAL] [Frama-c-discuss] Frama-c support for dynamic memory CAUTION: This email originated from outside of the organization. Do not click links or open attachments unless you can confirm the sender and know the content is safe. Hi Mike, Thanks for your interest in Frama-C and its deductive verification plugins (WP & Jessie). Just to complement the excellent answer by Claude, I would like to point out the following items: - allocation is already part of the Frama-C/WP memory models, eg. we use it for handling the scope of local variables, validity and assigns (which is somehow related to validity); - however, ACSL allocation clauses (such as @allocates) are not _yet_ implemented; - ghost fields would also be easy to implement in the memory models; - ghost fields and variables can not have logical type, and implementing them in the Frama-C kernel would be a significant development â and also raises some tricky design choices! By the way, you can find an example for singly-linked lists in this paper [1]. Note that this case study would have benefited of the support of logic types in ghost code, and that some workarounds are used to deal with this limitation, as Claude told before, dealing with memory separation is still a hard task. Best regards, L. Correnson [1] https://allan-blanchard.fr/publis/bkl_sac_2019.pdf ________________________________ De : Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de Whalen, Mike [mww at amazon.com] Envoyé : lundi 18 mai 2020 03:21 à : Frama-C public discussion Objet : Re: [Frama-c-discuss] Frama-c support for dynamic memory Hello all, Apologies for perhaps an unfair criticism of the WP manual. It is really a nice document, and I have been able to prove some interesting things. However, if we wish to use frama-c for AWS-related projects, we must have support for dynamic memory. In looking at more of the plug-ins, it appears that Jessie is built on top of separation logic. It is still referenced in the frama-c web site, but is it still supported? The documentation was a bit sketchy. Thank you all and apologies for my many emails. Mike From: Frama-c-discuss <frama-c-discuss-bounces at lists.gforge.inria.fr> on behalf of "Whalen, Mike" <mww at amazon.com> Reply-To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> Date: Sunday, May 17, 2020 at 12:11 AM To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> Subject: [Frama-c-discuss] Frama-c support for dynamic memory I have made it to nearly the end of the WP tutorial. In chapter 8, it is mentioned that âWP cannot currently work with dynamic allocation. A function that would use it could not be proved.â I would move this to an earlier portion of the document, say, chapter 1. This is quite disappointing. Are there any frama-c tools that do work with dynamic allocation? Mike -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200518/922a826b/attachment-0001.html>