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.