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
Reporterjessie_user 
Assigned Tocmarche 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
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 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?
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 - 2019 MantisBT Team
Powered by Mantis Bugtracker