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] \fresh predicat in Oxygen

  • Subject: [Frama-c-discuss] \fresh predicat in Oxygen
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Tue, 5 Feb 2013 17:20:25 +0000
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