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-discuss Digest, Vol 60, Issue 12

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 60, Issue 12
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Sun, 19 May 2013 10:23:13 +0000
  • In-reply-to: <mailman.21.1368957673.15594.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.21.1368957673.15594.frama-c-discuss@lists.gforge.inria.fr>
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
> ***********************************************