Feature request (Jessie): \fresh (and \separated)
ID0001033: This issue was created automatically from Mantis Issue 1033. Further discussion may take place here.
|ID0001033||Frama-C||Plug-in > jessie||public||2011-11-29||2011-11-29|
|Product Version||Frama-C Nitrogen-20111001||Target Version||-||Fixed in Version||-|
If I use jessie on function contract with \fresh(..) I've got: State_builder.aborted because of unimplemented feature. Please send a feature request at http://bts.frama-c.com with: 'Interp.pred Pfresh'.
I have described the problem in http://bts.frama-c.com/view.php?id=1032
Is it possible to implement with this features or what features can I use instead?
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information