Frama-C Bug Tracking System - Frama-C
View Issue Details
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

There are no notes attached to this issue.

Issue History
2009-12-24 16:27yegorNew Issue
2009-12-24 16:27yegorStatusnew => assigned
2009-12-24 16:27yegorAssigned To => cmarche
2009-12-25 17:38signolesAssigned Tocmarche => virgile
2010-01-29 17:59svn
2010-01-29 17:59svnStatusassigned => resolved
2010-01-29 17:59svnResolutionopen => fixed
2010-04-13 15:30signolesStatusresolved => new
2010-04-13 15:31signolesStatusnew => closed
2010-04-13 15:33signolesFixed in Version => Frama-C Boron