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
- Subject: [Frama-c-discuss] Frama-c support for dynamic memory
- From: Nicky.WILLIAMS at cea.fr (WILLIAMS Nicky)
- Date: Mon, 18 May 2020 07:11:58 +0000
- In-reply-to: <9a7e9bf4-e14e-0d39-6583-a7fbaceb62e9@inria.fr>
- References: <BD5124BD-33B8-438D-A0B4-D5E00815EED5@amazon.com>, <9a7e9bf4-e14e-0d39-6583-a7fbaceb62e9@inria.fr>
Hello everyone PathCrawler, the structural test generation plugin of Frama-C, treats dynamic allocation too. Best regards Nicky Williams ________________________________________ From: Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] on behalf of Claude Marche [Claude.Marche at inria.fr] Sent: 18 May 2020 09:09 To: frama-c-discuss at lists.gforge.inria.fr Subject: Re: [Frama-c-discuss] Frama-c support for dynamic memory Hello Mike, hello to all, Le 18/05/2020 à 03:21, Whalen, Mike a écrit : > 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. Interesting to learn that AWS aims at formally verifying C code. It is of course legitimate that you investigate on the existing tools to do so. Your analysis about capabilities of Frama-C and the WP plugin seems accurate to me. Let me add a few points that may make your analysis even more informed * verifying C code involving complex data-structures, including dynamic memory allocation, remains nowadays a complex task and a complex problem that is the subject of many on-going research in academia. It is not the case that you could find a perfect tool that would suit your needs off-the-shelf * Using techniques based on deductive verification is certainly promising, however for industrial needs I think it is important to have a broader vision and be ready to use several different techniques. For example regarding using Frama-C I was wondering if you investigated the Eva plug-in and how Eva and WP can be used in combination? * a less academic point : developing verification environment like Frama-C and make them reasonably usable from an industrial perspective costs a lot of human resources and money. Frama-C and WP are freely available, their development were and are supported in part by French public funding and in part by collaborations and contracts with industrial users. Is AWS considering a collaboration with the Frama-C developer team, with corresponding funding? [Disclaimer: I'm not member of Frama-C devteam, not a member of the CEA institute... yet I am paying taxes in France...] > 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. Being the main and almost only remaining maintainer of Jessie, I can say that they are current developments for porting it to recent Frama-C versions, but the development is now stopped due to absence of funding. Have a nice day, take care, - Claude _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
- References:
- [Frama-c-discuss] Frama-c support for dynamic memory
- From: mww at amazon.com (Whalen, Mike)
- [Frama-c-discuss] Frama-c support for dynamic memory
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Frama-c support for dynamic memory
- Prev by Date: [Frama-c-discuss] Frama-c support for dynamic memory
- Next by Date: [Frama-c-discuss] Frama-c support for dynamic memory
- Previous by thread: [Frama-c-discuss] Frama-c support for dynamic memory
- Next by thread: [Frama-c-discuss] Frama-c support for dynamic memory
- Index(es):