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

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