--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on May 2020 ---
[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