Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001033Frama-CPlug-in > jessiepublic2011-11-29 17:222011-11-29 17:22
Assigned Tocmarche 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0001033: Feature request (Jessie): \fresh (and \separated)
DescriptionIf 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?
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-11-29 17:22 jessie_user New Issue
2011-11-29 17:22 jessie_user Status new => assigned
2011-11-29 17:22 jessie_user Assigned To => cmarche

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker