--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on May 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c-discuss Digest, Vol 60, Issue 12



Hello Christiano,

my guess for the lack of support of \fresh in WP is that not all low level code need support for dynamic allocation.
To be more precise: many standards for safety critical software (e.g. IEC 61508 or EN 50128) 
highly recommend NOT to use dynamic memory allocation.

Nevertheless, it would be nice to see \fresh properly supported by WP.

Regards

Jens


> ----------------------------------------------------------------------
> 
> Message: 1
> Date: Sat, 18 May 2013 20:04:04 +0100
> From: Cristiano Sousa <cristiano.sousa126 at gmail.com>
> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
> Subject: [Frama-c-discuss] [WP Plugin] Fresh annotation
> Message-ID:
> 	<CAEt_dEonKaJvMB=32t9RMOxPo1XQC96UD-RfkCJ6_QzgRrh=-Q at mail.gmail.com>
> Content-Type: text/plain; charset="iso-8859-1"
> 
> Hi all,
> 
> As i understand it, the WP plugin was created to address more low level
> verification. With that in mind I question why the fresh predicate (and
> allocable, freeable, allocates, frees) has not been implemented yet.
> 
> I'm currently working on two frama-c projects that use the WP plugin, and
> too often I run into problems such as this:
> 
> http://pastebin.com/TkNUqLbL
> 
> Is there an alternative to avoid this problem? Or will I have to wait until
> the fresh predicate is implemented?
> 
> Thanks!
> 
> -- 
> Cumprimentos,
> Cristiano Sousa
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130518/d8a4876f/attachment-0001.html>
> 
> ------------------------------
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> 
> End of Frama-c-discuss Digest, Vol 60, Issue 12
> ***********************************************