--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on May 2020 ---
Le 18/05/2020 à 09:11, WILLIAMS Nicky a écrit : > PathCrawler, the structural test generation plugin of Frama-C, treats dynamic allocation too. As well as E-ACSL, the runtime verification plug-in of Frama-C. Dynamic allocations are much easier to handle with dynamic analysis tools :-). Julien > ________________________________________ > 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 > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss