--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on May 2013 ---
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.html>