Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000358Frama-CKernel > ACSL implementationpublic2009-12-08 14:312010-04-13 15:33
Reportercmarche 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000358: redeclaration as different kind of symbol
DescriptionIn 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 !

TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000611)
yakobowski (manager)
2009-12-24 12:39

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

Corrected by revision 7219. The declarations
   type t;
   logic t t(integer n);
now cause an error.

- Issue History
Date Modified Username Field Change
2009-12-08 14:31 cmarche New Issue
2009-12-08 16:33 signoles Status new => assigned
2009-12-08 16:33 signoles Assigned To => virgile
2009-12-23 15:03 yakobowski Assigned To virgile => yakobowski
2009-12-24 12:39 yakobowski Note Added: 0000611
2009-12-24 12:41 yakobowski Note Added: 0000612
2009-12-24 12:41 yakobowski Status assigned => resolved
2009-12-24 12:41 yakobowski Resolution open => fixed
2010-02-05 09:44 signoles Category Kernel => Kernel > ACSL implementation
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 - 2018 MantisBT Team
Powered by Mantis Bugtracker