Frama-C Bug Tracking System - Frama-C
View Issue Details
0000364Frama-CPlug-in > jessiepublic2009-12-24 16:272010-04-13 15:33
yegor 
virgile 
normalminoralways
closedfixed 
Frama-C Beryllium-20090902 
Frama-C Boron-20100401 
0000364: complete/disjoint behaviors shouldn't accept undefined behaviors
Processing 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() {
}
No tags attached.
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:59svnCheckin
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

There are no notes attached to this issue.