--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on February 2013 ---
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