Frama-C Bug Tracking System - Frama-C
View Issue Details
0001033Frama-CPlug-in > jessiepublic2011-11-29 17:222011-11-29 17:22
Frama-C Nitrogen-20111001 
0001033: Feature request (Jessie): \fresh (and \separated)
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 with: 'Interp.pred Pfresh'. I have described the problem in Is it possible to implement with this features or what features can I use instead?
No tags attached.
Issue History
2011-11-29 17:22jessie_userNew Issue
2011-11-29 17:22jessie_userStatusnew => assigned
2011-11-29 17:22jessie_userAssigned To => cmarche

There are no notes attached to this issue.