Frama-C Bug Tracking System - Frama-C
View Issue Details
0000358Frama-CKernel > ACSL implementationpublic2009-12-08 14:312010-04-13 15:33
cmarche 
yakobowski 
normalminoralways
closedfixed 
Frama-C Beryllium-20090902 
Frama-C Boron-20100401 
0000358: redeclaration as different kind of symbol
In C, the code typedef int t; t t(); fails with error: ‘t’ redeclared as different kind of symbol The logic parser should produce a similar error as in /*@ axiomatic A { logic type t; logic t t(integer n); } */ which do not produce any error, but if you do later //* lemma \forall integer n; t(n) == t(n); you get user error: syntax error while parsing annotation which is very difficult to understand !
No tags attached.
Issue History
2009-12-08 14:31cmarcheNew Issue
2009-12-08 16:33signolesStatusnew => assigned
2009-12-08 16:33signolesAssigned To => virgile
2009-12-23 15:03yakobowskiAssigned Tovirgile => yakobowski
2009-12-24 12:39yakobowskiNote Added: 0000611
2009-12-24 12:41yakobowskiNote Added: 0000612
2009-12-24 12:41yakobowskiStatusassigned => resolved
2009-12-24 12:41yakobowskiResolutionopen => fixed
2010-02-05 09:44signolesCategoryKernel => Kernel > ACSL implementation
2010-04-13 15:30signolesStatusresolved => new
2010-04-13 15:31signolesStatusnew => closed
2010-04-13 15:33signolesFixed in Version => Frama-C Boron

Notes
(0000611)
yakobowski   
2009-12-24 12:39   
Corrected by revision 7219. The declarations type t; logic t t(integer n); now cause an error.
(0000612)
yakobowski   
2009-12-24 12:41   
Corrected by revision 7219. The declarations type t; logic t t(integer n); now cause an error.