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] Frama-c support for dynamic memory

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>