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
- Follow-Ups:
- [Frama-c-discuss] \fresh predicat in Oxygen
- From: loic.correnson at cea.fr (Loïc Correnson)
- [Frama-c-discuss] \fresh predicat in Oxygen
- Next by Date: [Frama-c-discuss] \fresh predicat in Oxygen
- Next by thread: [Frama-c-discuss] \fresh predicat in Oxygen
- Index(es):