Frama-C Bug Tracking System - Frama-C
View Issue Details
0001033Frama-CPlug-in > jessiepublic2011-11-29 17:222011-11-29 17:22
jessie_user 
cmarche 
normalfeaturealways
assignedopen 
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 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?
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.