--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on February 2013 ---
Hi Jens, The predicate \fresh and the other clauses related to memory allocation (section 2.7.3 of ACSL 1.6) are not implemented in WP. And I'm afraid they will not be available in the upcoming release of WP... We are working on these features, but we need more work to release it. L. Le 5 f?vr. 2013 ? 18:20, Gerlach, Jens a ?crit : > Hello, > > I tried to play around with the "\fresh" pedicate described on page 58 in acsl-implementation-Oxygen-20120901.pdf. > Oxygen says > > - Warning: Ignored post-condition for function call > Reason: fresh not yet implemented > > I understand that it is an experimental feature band so I am wondering whether Frama-C has an option > to experiment with it. > > Regards > > Jens > > > > > _______________________________________________ > 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