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

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