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 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