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] [PROVENANCE INTERNET] Re: Frama-c support for dynamic memory

  • Subject: [Frama-c-discuss] [PROVENANCE INTERNET] Re: Frama-c support for dynamic memory
  • From: julien.signoles at (Julien Signoles)
  • Date: Tue, 19 May 2020 08:36:32 +0200
  • In-reply-to: <>
  • References: <> <> <>

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 :-).


> ________________________________________
> From: Frama-c-discuss [frama-c-discuss-bounces at] on behalf of Claude Marche [Claude.Marche at]
> Sent: 18 May 2020 09:09
> To: frama-c-discuss at
> 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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at