Frama-C-discuss mailing list archives

julien.signoles at cea.fr (Julien Signoles) · Tue, 19 May 2020 08:36:32 +0200

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

Frama-C-discuss mailing list archives

[Frama-c-discuss] [PROVENANCE INTERNET] Re: Frama-c support for dynamic memory