Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000364Frama-CPlug-in > jessiepublic2009-12-24 16:272010-04-13 15:33
Reporteryegor 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000364: complete/disjoint behaviors shouldn't accept undefined behaviors
DescriptionProcessing of following program by Jessie should not succeed. An error should be reported instead.

/*@
        behavior foo:
        behavior bar:
        
        complete behaviors foo, bar, foobar;
        disjoint behaviors foo, bar, foobar;
*/
void f() {
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-12-24 16:27 yegor New Issue
2009-12-24 16:27 yegor Status new => assigned
2009-12-24 16:27 yegor Assigned To => cmarche
2009-12-25 17:38 signoles Assigned To cmarche => virgile
2010-01-29 17:59 svn Checkin
2010-01-29 17:59 svn Status assigned => resolved
2010-01-29 17:59 svn Resolution open => fixed
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version => Frama-C Boron

Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker