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

[Frama-c-discuss] \fresh predicat in Oxygen



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